SIFT probabilistic verification papers presented at DIFTS Workshop
Robert Goldman presented two papers -- joint work with Mike Boldt and David Musliner -- at the International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS). These papers concerned our work on verifying systems modeled as probabilistic automata. The work was done as part of the "Quiksilver" project, funded by the Office of Naval Research, on which SIFT was a subcontractor to Carnegie-Mellon University (specifically Prof. Edmund Clarke's group). The papers are titled "Heuristic Search for Bounded Model Checking of Probabilistic Automata," and "Offline Monte Carlo Tree Search for Statistical Model Checking of Markov Decision Processes." Each describes a new method for model-checking systems of probabilistic automata, based on search, and on Monte Carlo tree search, respectively.