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

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

1 2 3 ... 13 14 15 next

  1. Baresi, L.; Bersani, M. M.; Marconi, F.; Quattrocchi, G.; Rossi, M.: Using formal verification to evaluate the execution time of spark applications (2020)
  2. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)
  3. Firman, Elizabeth; Maoz, Shahar; Ringert, Jan Oliver: Performance heuristics for GR(1) synthesis and related algorithms (2020)
  4. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  5. Mirzaie, Nahal; Faghih, Fathiyeh; Jacobs, Swen; Bonakdarpour, Borzoo: Parameterized synthesis of self-stabilizing protocols in symmetric networks (2020)
  6. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
  7. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  8. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  9. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  10. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  11. Ramasubramanian, Bhaskar; Niu, Luyao; Clark, Andrew; Bushnell, Linda; Poovendran, Radha: Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates (2019)
  12. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  13. Chaki, Sagar; Gurfinkel, Arie: BDD-based symbolic model checking (2018)
  14. Gheorghe, Marian; Ceterchi, Rodica; Ipate, Florentin; Konur, Savas; Lefticaru, Raluca: Kernel P systems: from modelling to verification and testing (2018)
  15. Kupferman, Orna: Automata theory and model checking (2018)
  16. Li, Jianwen; Zhang, Lijun; Zhu, Shufang; Pu, Geguang; Vardi, Moshe Y.; He, Jifeng: An explicit transition system construction approach to LTL satisfiability checking (2018)
  17. Wu, Yi-Chin; Raman, Vasumathi; Rawlings, Blake C.; Lafortune, Stéphane; Seshia, Sanjit A.: Synthesis of obfuscation policies to ensure privacy and utility (2018)
  18. Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan: A compiler for MSVL and its applications (2018)
  19. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  20. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)

1 2 3 ... 13 14 15 next