scientific article; zbMATH DE number 7453201
From MaRDI portal
Publication:5020662
Publication date: 6 January 2022
Full work available at URL: https://arxiv.org/abs/2008.02939
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Synthesizing history and prophecy variables for symbolic model checking, Counterexample-guided prophecy for model checking modulo the theory of arrays
Uses Software
Cites Work
- Unnamed Item
- SMT-based model checking for recursive programs
- A cooperative parallelization approach for property-directed \(k\)-induction
- Efficient interpolation for the theory of arrays
- Global guidance for local generalization in model checking
- Infinite-state invariant checking with IC3 and predicate abstraction
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
- Horn Clause Solvers for Program Verification
- SAT-Based Model Checking without Unrolling
- SMTS: Distributed, Visualized Constraint Solving
- The MathSAT5 SMT Solver
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Decomposing Farkas Interpolants
