NuSMV

NuSMV is a symbolic model checker developed as a joint project between: The Embedded Systems Unit in the Center for Information Technology at FBK-IRST The Model Checking group at Carnegie Mellon University , the Mechanized Reasoning Group at University of Genova The Mechanized Reasoning Group at University of Trento. NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas. NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model Checker, which can be connected to the Minisat SAT Solver and/or to the ZChaff SAT Solver. The University of Genova has contributed SIM, a state-of-the-art SAT solver used until version 2.5.0, and the RBC package use in the Bounded Model Checking algorithms.


References in zbMATH (referenced in 249 articles , 1 standard article )

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

1 2 3 ... 11 12 13 next

  1. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  2. Gheorghe, Marian; Ceterchi, Rodica; Ipate, Florentin; Konur, Savas: Kernel P systems modelling, testing and verification -- sorting case study (2017)
  3. Konnov, Igor; Veith, Helmut; Widder, Josef: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability (2017)
  4. Adzkiya, Dieky; Zhang, Yining; Abate, Alessandro: VeriSIMPL 2: an open-source software for the verification of max-plus-linear systems (2016)
  5. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiène: Formal dependability modeling and analysis: a survey (2016)
  6. Barnat, Jiří; Bauch, Petr; Beneš, Nikola; Brim, Luboš; Beran, Jan; Kratochvíla, Tomáš: Analysing sanity of requirements for avionics systems (2016)
  7. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  8. Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
  9. De Giacomo, Giuseppe; Gerevini, Alfonso Emilio; Patrizi, Fabio; Saetti, Alessandro; Sardina, Sebastian: Agent planning programs (2016)
  10. De Giacomo, Giuseppe; Lespérance, Yves; Patrizi, Fabio: Bounded situation calculus action theories (2016)
  11. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  12. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  13. Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
  14. Schuppan, Viktor: Extracting unsatisfiable cores for LTL via temporal resolution (2016)
  15. Schuppan, Viktor: Enhancing unsatisfiable cores for LTL with information on temporal relevance (2016)
  16. ter Beek, Maurice H.; Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints (2016)
  17. Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of $\mathrmEB^3$ specifications using CADP (2016)
  18. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  19. Barnat, Jiří: Quo vadis explicit-state model checking (2015)
  20. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano: HRELTL: a temporal logic for hybrid systems (2015)

1 2 3 ... 11 12 13 next