SMT-based model checking for recursive programs
From MaRDI portal
Publication:518396
DOI10.1007/s10703-016-0249-4zbMath1358.68072arXiv1405.4028OpenAlexW2571456046MaRDI QIDQ518396
Sagar Chaki, Arie Gurfinkel, Anvesh Komuravelli
Publication date: 28 March 2017
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1405.4028
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (33)
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ RustHorn: CHC-Based Verification for Rust Programs ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Programmable program synthesis ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Toward neural-network-guided program synthesis and verification ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Unnamed Item ⋮ Parameterized recursive refinement types for automated program verification ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ On higher-order reachability games vs may reachability ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ SMT sampling via model-guided approximation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Run-time complexity bounds using squeezers ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Unbounded procedure summaries from bounded environments ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ Copy complexity of Horn formulas with respect to unit read-once resolution ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ Refutation-based synthesis in SMT ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ On recursion-free Horn clauses and Craig interpolation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear quantifier elimination
- Program invariants as fixedpoints
- Generalized Property Directed Reachability
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- From Under-Approximations to Over-Approximations and Back
- SAT-Based Model Checking without Unrolling
- Applying Linear Quantifier Elimination
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Solving SAT and SAT Modulo Theories
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Precise interprocedural dataflow analysis with applications to constant propagation
- Lazy abstraction
- Compositional may-must program analysis
- Nested interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: SMT-based model checking for recursive programs
