MCMT: a model checker modulo theories

DOI10.1007/978-3-642-14203-1_3MaRDI QIDQ5747748zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Towards SMT Model Checking of Array-Based Systems
• Light-weight SMT-based model checking
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• SMT-based verification of data-aware processes: a model-theoretic approach
• Satisfiability modulo theories

Cites work

• scientific article; zbMATH DE number 1361123 (Why is no real title available?)
• Goal-directed invariant synthesis for model checking modulo theories
• Light-weight SMT-based model checking
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Predicate abstraction for software verification
• Predicate abstraction with indexed predicates
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Towards SMT Model Checking of Array-Based Systems

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
• An extension of lazy abstraction with interpolation for programs with arrays
• Search-space partitioning for parallelizing SMT solvers
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Formal specification and verification of dynamic parametrized architectures
• Parameterized model checking on the TSO weak memory model
• Towards SMT Model Checking of Array-Based Systems
• Combined covers and Beth definability
• Tasks in modular proofs of concurrent algorithms
• scientific article; zbMATH DE number 7566058 (Why is no real title available?)
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Finite reasons for safety. Parameterized verification by finite model finding
• Satisfiability modulo theories
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• αCheck: A mechanized metatheory model checker
• Analysis of a clock synchronization protocol for wireless sensor networks
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Rewriting modulo SMT and open system analysis
• Model completeness, covers and superposition
• Rewriting modulo SMT and open system analysis
• Abduction of trap invariants in parameterized systems
• Tasks in modular proofs of concurrent algorithms
• SMT-based model checking for recursive programs
• Light-weight SMT-based model checking
• Combination of uniform interpolants via Beth definability

Describes a project that uses

Uses Software

• Mcmt

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)