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 288 articles , 1 standard article )

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

1 2 3 ... 13 14 15 next

  1. Firman, Elizabeth; Maoz, Shahar; Ringert, Jan Oliver: Performance heuristics for GR(1) synthesis and related algorithms (2020)
  2. Mirzaie, Nahal; Faghih, Fathiyeh; Jacobs, Swen; Bonakdarpour, Borzoo: Parameterized synthesis of self-stabilizing protocols in symmetric networks (2020)
  3. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
  4. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  5. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  6. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  7. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  8. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  9. Chaki, Sagar; Gurfinkel, Arie: BDD-based symbolic model checking (2018)
  10. Gheorghe, Marian; Ceterchi, Rodica; Ipate, Florentin; Konur, Savas; Lefticaru, Raluca: Kernel P systems: from modelling to verification and testing (2018)
  11. Kupferman, Orna: Automata theory and model checking (2018)
  12. Li, Jianwen; Zhang, Lijun; Zhu, Shufang; Pu, Geguang; Vardi, Moshe Y.; He, Jifeng: An explicit transition system construction approach to LTL satisfiability checking (2018)
  13. Wu, Yi-Chin; Raman, Vasumathi; Rawlings, Blake C.; Lafortune, Stéphane; Seshia, Sanjit A.: Synthesis of obfuscation policies to ensure privacy and utility (2018)
  14. Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan: A compiler for MSVL and its applications (2018)
  15. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  16. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  17. Gheorghe, Marian; Ceterchi, Rodica; Ipate, Florentin; Konur, Savas: Kernel P systems modelling, testing and verification -- sorting case study (2017)
  18. Konnov, Igor; Veith, Helmut; Widder, Josef: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability (2017)
  19. Rawlings, Blake C.; Ydstie, B. Erik: Falsification of combined invariance and reachability specifications in hybrid control systems (2017)
  20. Szpyrka, Marcin; Jasiul, Bartosz: Evaluation of cyber security and modelling of risk propagation with Petri nets (2017)

1 2 3 ... 13 14 15 next