nuXmv

The nuXmv Symbolic Model Checker. This paper describes the nuXmv symbolic model checker for finite- and infinite-state synchronous transition systems. nuXmv is the evolution of the nuXmv open source model checker. It builds on and extends nuXmv along two main directions. For finite-state systems it complements the basic verification techniques of nuXmv with state-of-the-art verification algorithms. For infinite-state systems, it extends the nuXmv language with new data types, namely Integers and Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv has been optimized in terms of performance to be competitive with the state of the art. nuXmv has been used in several industrial projects as verification back-end, and it is the basis for several extensions to cope with requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software model checking.


References in zbMATH (referenced in 28 articles )

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

1 2 next

  1. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian: Model-based safety assessment of a triple modular generator with xSAP (2021)
  2. Ghilardi, Silvio; Pagani, Elena: Higher-order quantifier elimination, counter simulations and fault-tolerant systems (2021)
  3. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano: Certifying proofs for SAT-based model checking (2021)
  4. 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
  5. Bohlender, Dimitri; Kowalewski, Stefan: Leveraging Horn clause solving for compositional verification of PLC software (2020)
  6. Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano: SMT-based satisfiability of first-order LTL with event freezing functions and metric operators (2020)
  7. Li, Jianwen; Pu, Geguang; Zhang, Yueling; Vardi, Moshe Y.; Rozier, Kristin Y.: SAT-based explicit (\mathsfLTL_f) satisfiability checking (2020)
  8. Luttenberger, Michael; Meyer, Philipp J.; Sickert, Salomon: Practical synthesis of reactive systems from LTL specifications via parity games (2020)
  9. Qin, Xudong; Bliudze, Simon; Madelaine, Eric; Hou, Zechen; Deng, Yuxin; Zhang, Min: SMT-based generation of symbolic automata (2020)
  10. Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian: Formal reliability analysis of redundancy architectures (2019)
  11. Geatti, Luca; Gigante, Nicola; Montanari, Angelo: A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL (2019)
  12. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  13. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theory of floating-point numbers (2019)
  14. Bendík, Jaroslav; Černá, Ivana: Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets (2018)
  15. Cimatti, Alessandro; Demasi, Ramiro; Tonetta, Stefano: Tightening the contract refinements of a system architecture (2018)
  16. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions (2018)
  17. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  18. Cabodi, G.; Camurati, P. E.; Mishchenko, A.; Palena, M.; Pasini, P.: SAT solver management strategies in IC3: an experimental approach (2017)
  19. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF (2017)
  20. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: (\textPara^2): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (2017)

1 2 next