48 citations · 64 across the 4 of their papers we have counts for
5 papers
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel +1
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely…
SMT-based Model Checking for Recursive Programs
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other…
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…