91 citations · 210 across the 30 of their papers we have counts for
8 papers · 1 filter
ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Eric Vin, Kyle A. Miller, Inigo Incer +2
Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. E…
Satisfiability and Synthesis Modulo Oracles
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification)…
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte +3
We revisit the symbolic verification of Markov chains with respect to finite horizon reachability properties. The prevalent approach iteratively computes step-bounded state reachab…
Runtime Monitoring for Markov Decision Processes
Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk,…
SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers
Elizabeth Polgreen, Sanjit A. Seshia
Program synthesis is the task of automatically generating expressions that satisfy a given specification. Program synthesis techniques have been used to automate the generation of…
Understanding and Extending Incremental Determinization for 2QBF
Markus N. Rabe, Leander Tentrup, Cameron Rasmussen +1
Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determ…