Towards SMT Model Checking of Array-Based Systems
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- A logical reconstruction of reachability
- Efficient theory combination via Boolean search
- Lazy satisfiability modulo theories
- On Local Reasoning in Verification
- Parameterized Verification of Infinite-State Processes with Global Conditions
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
- Rewriting Systems with Data
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Symbolic model checking with rich assertional languages
- Towards SMT Model Checking of Array-Based Systems
- Verification, Model Checking, and Abstract Interpretation
Cited in
(22)- Generalized rewrite theories, coherence completion, and symbolic methods
- Scaling bounded model checking by transforming programs with arrays
- SMT-based verification of data-aware processes: a model-theoretic approach
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- A new acceleration-based combination framework for array properties
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Towards SMT Model Checking of Array-Based Systems
- Communicating Sequential Processes. The First 25 Years
- On model checking data-independent systems with arrays without reset
- Verification of composed array-based systems with applications to security-aware workflows
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Definability of accelerated relations in a theory of arrays and its applications
- MCMT: a model checker modulo theories
- Finite reasons for safety. Parameterized verification by finite model finding
- Satisfiability modulo theories
- Invariant checking for SMT-based systems with quantifiers
- Rewriting modulo SMT and open system analysis
- Taming past LTL and flat counter systems
- SMT-based generation of symbolic automata
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Light-weight SMT-based model checking
This page was built for publication: Towards SMT Model Checking of Array-Based Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3541687)
