150 citations · 341 across the 17 of their papers we have counts for
9 papers · 1 filter
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva +1
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive…
Proof Generation from Delta-Decisions
Sicun Gao, Soonho Kong, Edmund Clarke
We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem…
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions
Bing Liu, Soonho Kong, Sicun Gao +2
A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (\eg, time series). In this paper we focus o…
Satisfiability Modulo ODEs
Sicun Gao, Soonho Kong, Edmund Clarke
We study SMT problems over the reals containing ordinary differential equations. They are important for formal verification of realistic hybrid systems and embedded software. We de…
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki +1
Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "con…
Learning Probabilistic Systems from Tree Samples
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
We consider the problem of learning a non-deterministic probabilistic system consistent with a given finite set of positive and negative tree samples. Consistency is defined with r…
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probab…
Delta-Decidability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence φcontaining only bounded quantifiers, and any pos…
Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including t…