MCMT: A Model Checker Modulo Theories

DOI10.1007/978-3-642-14203-1_3zbMath1291.68257OpenAlexW1516900991MaRDI QIDQ5747748

Silvio Ranise, Silvio Ghilardi

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)

Related Items

Decision procedures for flat array properties, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, Search-Space Partitioning for Parallelizing SMT Solvers, Satisfiability Modulo Theories, Rewriting modulo SMT and open system analysis, Tasks in modular proofs of concurrent algorithms, A New Acceleration-Based Combination Framework for Array Properties, Parameterized model checking on the TSO weak memory model, Symbolic backward reachability with effectively propositional logic. Application to security policy analysis, SMT-based verification of data-aware processes: a model-theoretic approach, An extension of lazy abstraction with interpolation for programs with arrays, Formal specification and verification of dynamic parametrized architectures, Unnamed Item, Higher-order quantifier elimination, counter simulations and fault-tolerant systems, Generalized rewrite theories, coherence completion, and symbolic methods, Counterexample-guided prophecy for model checking modulo the theory of arrays, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Model completeness, covers and superposition, Analysis of a clock synchronization protocol for wireless sensor networks, Combination of uniform interpolants via Beth definability, Combined covers and Beth definability, Finite reasons for safety

Uses Software

• Mcmt

Cites Work

• Towards SMT Model Checking of Array-Based Systems
• Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
• Predicate abstraction for software verification
• Light-Weight SMT-based Model Checking
• Predicate abstraction with indexed predicates
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Unnamed Item