Mcmt

Mcmt: a model checker modulo theories. We describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state systems whose state variables are arrays. Theories specify the properties of the indexes and the elements of the arrays. Sets of states and transitions of a system are described by quantified first-order formulae. The core of the system is a backward reachability procedure which symbolically computes pre-images of the set of unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart of the system. mcmt has been successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems.


References in zbMATH (referenced in 24 articles )

Showing results 1 to 20 of 24.
Sorted by year (citations)

1 2 next

  1. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (2021)
  2. Ghilardi, Silvio; Pagani, Elena: Higher-order quantifier elimination, counter simulations and fault-tolerant systems (2021)
  3. Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark Barrett: Pono: A Flexible and Extensible SMT-Based Model Checker (2021) not zbMATH
  4. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
  5. Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha: Parameterized model checking on the TSO weak memory model (2020)
  6. Meseguer, José: Generalized rewrite theories, coherence completion, and symbolic methods (2020)
  7. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: From model completeness to verification of data aware processes (2019)
  8. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: Model completeness, covers and superposition (2019)
  9. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  10. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  11. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: A new acceleration-based combination framework for array properties (2015)
  12. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
  13. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  14. Karbyshev, A.; Bjørner, N.; Itzhaky, S.; Rinetzky, N.; Shoham, S.: Property-directed inference of universal invariants or proving their absence (2015)
  15. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  16. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Definability of accelerated relations in a theory of arrays and its applications (2013)
  17. Bertolissi, Clara; Ranise, Silvio: Verification of composed array-based systems with applications to security-aware workflows (2013)
  18. Lisitsa, Alexei: Finite reasons for safety (2013)
  19. Ranise, Silvio: Symbolic backward reachability with effectively propositional logic. Application to security policy analysis (2013)
  20. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: Lazy abstraction with interpolants for arrays (2012)

1 2 next