MCMT: a model checker modulo theories
From MaRDI portal
Publication:5747748
DOI10.1007/978-3-642-14203-1_3zbMATH Open1291.68257OpenAlexW1516900991MaRDI QIDQ5747748FDOQ5747748
Authors: Silvio Ghilardi, Silvio Ranise 
Publication date: 14 September 2010
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_3
Recommendations
Cites Work
- Towards SMT Model Checking of Array-Based Systems
- Predicate abstraction for software verification
- Parameterized Verification of Infinite-State Processes with Global Conditions
- Light-weight SMT-based model checking
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
- Goal-directed invariant synthesis for model checking modulo theories
- Title not available (Why is that?)
- Predicate abstraction with indexed predicates
Cited In (30)
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
- SMT-based verification of data-aware processes: a model-theoretic approach
- Decision procedures for flat array properties
- A new acceleration-based combination framework for array properties
- Search-space partitioning for parallelizing SMT solvers
- An extension of lazy abstraction with interpolation for programs with arrays
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Formal specification and verification of dynamic parametrized architectures
- Towards SMT Model Checking of Array-Based Systems
- Parameterized model checking on the TSO weak memory model
- Tasks in modular proofs of concurrent algorithms
- Combined covers and Beth definability
- Title not available (Why is that?)
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Satisfiability modulo theories
- Finite reasons for safety. Parameterized verification by finite model finding
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- αCheck: A mechanized metatheory model checker
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Analysis of a clock synchronization protocol for wireless sensor networks
- Abduction of trap invariants in parameterized systems
- Rewriting modulo SMT and open system analysis
- Rewriting modulo SMT and open system analysis
- Model completeness, covers and superposition
- Tasks in modular proofs of concurrent algorithms
- Light-weight SMT-based model checking
- SMT-based model checking for recursive programs
- Combination of uniform interpolants via Beth definability
Uses Software
This page was built for publication: MCMT: a model checker modulo theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747748)
