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

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

1 2 3 ... 14 15 16 next

  1. Bennour, Imed Eddine: Formal verification of timed synchronous dataflow graphs using lustre (2021)
  2. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian: Model-based safety assessment of a triple modular generator with xSAP (2021)
  3. Gheorghe, Marian; Lefticaru, Raluca; Konur, Savas; Niculescu, Ionuţ Mihai; Adorna, Henry N.: Spiking neural P systems: matrix representation and formal verification (2021)
  4. Ho, Hsi-Ming; Zhou, Ruoyu; Jones, Timothy M.: Timed hyperproperties (2021)
  5. 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
  6. Menghi, Claudio; Rizzi, Alessandro Maria; Bernasconi, Anna; Spoletini, Paola: TOrPEDO : witnessing model correctness with topological proofs (2021)
  7. Rubio, Rubén; Martí-Oliet, Narciso; Pita, Isabel; Verdejo, Alberto: Strategies, model checking and branching-time properties in Maude (2021)
  8. Baresi, L.; Bersani, M. M.; Marconi, F.; Quattrocchi, G.; Rossi, M.: Using formal verification to evaluate the execution time of Spark applications (2020)
  9. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)
  10. Firman, Elizabeth; Maoz, Shahar; Ringert, Jan Oliver: Performance heuristics for GR(1) synthesis and related algorithms (2020)
  11. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  12. Hajnal, Matej; Pastva, Samuel: Toward model selection by formal methods (2020)
  13. Hustadt, Ullrich; Ozaki, Ana; Dixon, Clare: Theorem proving for pointwise metric temporal logic over the naturals via translations (2020)
  14. Mirzaie, Nahal; Faghih, Fathiyeh; Jacobs, Swen; Bonakdarpour, Borzoo: Parameterized synthesis of self-stabilizing protocols in symmetric networks (2020)
  15. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
  16. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  17. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  18. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  19. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  20. Ramasubramanian, Bhaskar; Niu, Luyao; Clark, Andrew; Bushnell, Linda; Poovendran, Radha: Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates (2019)

1 2 3 ... 14 15 16 next