Article

NUSMV: A New Symbolic Model Verifier

Authors:

Alessandro Cimatti,

Edmund M. Clarke,

Fausto Giunchiglia,

Marco RoveriAuthors Info & Claims

CAV '99: Proceedings of the 11th International Conference on Computer Aided Verification

Pages 495 - 499

Published: 06 July 1999 Publication History

Abstract

No abstract available.

References

[1]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. In Proc. TACAS'99, March 1999. To appear.

Crossref

Google Scholar

[2]

R. K. Brayton et al. VIS: A system for Verification and Synthesis. In Proc. of CAV'96. LNCS 1102, Springer-Verlag.

Crossref

Google Scholar

[3]

J. Burch, E. Clarke, and D. Long. Representing Circuits More Efficiently in Symbolic Model Checking. In Proc. of the 28th ACM/IEEE Design Automation Conference, pages 403-407, Los Alamitos, CA, June 1991. IEEE Computer Society Press.

Crossref

Google Scholar

[4]

A. Cimatti, M. Roveri, and P. Traverso. Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains. In Proc. of the 15th National Conference on Artificial Intelligence (AAAI-98), Madison, Wisconsin, 1998. AAAI-Press.

Crossref

Google Scholar

[5]

O. Grumberg E. Clarke and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10(1):57-71, February 1997.

Crossref

Google Scholar

[6]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.

Crossref

Google Scholar

[7]

R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

Google Scholar

[8]

F. Somenzi. CUDD: CU Decision Diagram package -- release 2.1.2. Department of Electrical and Computer Engineering -- University of Colorado at Boulder, April 1997. ftp://vlsi.colorado.edu/pub/

Google Scholar

Cited By

View all

Tietz VFrey CSchoepf JAnnighoefer BKühn TSousa V(2022)Why the use of domain-specific modeling in airworthy software requires new methods and how these might look like?Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3561536(627-632)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3561536
Liang XBurns JSanchez JDantu KZiarek LLiu Y(2021)Understanding Bounding Functions in Safety-Critical UAV SoftwareProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00119(1311-1322)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00119
Yousefi FAbhashkumar ASubramanian KHans KGhorbani SAkella ABhagwan RPorter G(2020)Liveness verification of stateful network functionsProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388260(257-272)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388260
Show More Cited By

Recommendations

NuSMV 2: An OpenSource Tool for Symbolic Model Checking
CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification
Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems
SAFECOMP'12: Proceedings of the 2012 international conference on Computer Safety, Reliability, and Security

In this paper we present Parallel NuSMV, a tool based on the NuSMV model checker that integrates the ManySAT parallel SAT solver. The PNuSMV is part of the FormalSpecs Verifier framework for the formal verification of Simulink/Stateflow models. The ...
A model advisor for NuSMV specifications

Among possible model validation techniques able to identify defects early in the system development, model review aims also at determining if a model is of sufficient quality, where quality is measured as the absence of certain faults. In this paper, we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV '99: Proceedings of the 11th International Conference on Computer Aided Verification

July 1999

483 pages

ISBN:3540662022

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 July 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

125
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Tietz VFrey CSchoepf JAnnighoefer BKühn TSousa V(2022)Why the use of domain-specific modeling in airworthy software requires new methods and how these might look like?Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3550356.3561536(627-632)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550356.3561536
Liang XBurns JSanchez JDantu KZiarek LLiu Y(2021)Understanding Bounding Functions in Safety-Critical UAV SoftwareProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00119(1311-1322)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00119
Yousefi FAbhashkumar ASubramanian KHans KGhorbani SAkella ABhagwan RPorter G(2020)Liveness verification of stateful network functionsProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388260(257-272)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388260
Tran N(2019)A Specification-Based Approach to Model Checking Event-Driven SystemsProceedings of the 10th International Symposium on Information and Communication Technology10.1145/3368926.3369703(449-456)Online publication date: 4-Dec-2019
https://dl.acm.org/doi/10.1145/3368926.3369703
García SPelliccione PMenghi CBerger TBures TNierstrasz OGray JOliveira B(2019)High-level mission specification for multiple robotsProceedings of the 12th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3357766.3359535(127-140)Online publication date: 20-Oct-2019
https://dl.acm.org/doi/10.1145/3357766.3359535
Menghi CTsigkanos CBerger TPelliccione PMussbacher GAtlee JBultan T(2019)PsALMProceedings of the 41st International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion.2019.00048(99-102)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICSE-Companion.2019.00048
Bahrami ADe Maria EFelty A(2018)Modelling and Verifying Dynamic Properties of Biological Neural Networks in CoqProceedings of the 9th International Conference on Computational Systems-Biology and Bioinformatics10.1145/3291757.3291771(1-11)Online publication date: 10-Dec-2018
https://dl.acm.org/doi/10.1145/3291757.3291771
Shrestha RMehrpouyan HXu DZhao ZAhn GKrishnan RGhinita G(2018)Model Checking of Security Properties in Industrial Control Systems (ICS)Proceedings of the Eighth ACM Conference on Data and Application Security and Privacy10.1145/3176258.3176949(164-166)Online publication date: 13-Mar-2018
https://dl.acm.org/doi/10.1145/3176258.3176949
Kong JLomuscio A(2017)Model checking multi-agent systems against LDLK specificationsProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171642.3171804(1138-1144)Online publication date: 19-Aug-2017
https://dl.acm.org/doi/10.5555/3171642.3171804
Sardinha LNeto OOrlandi VCampos SSilveira J(2017)Simplified model for automatic QCA circuitry verificationProceedings of the 30th Symposium on Integrated Circuits and Systems Design: Chip on the Sands10.1145/3109984.3110011(204-209)Online publication date: 28-Aug-2017
https://dl.acm.org/doi/10.1145/3109984.3110011
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Recommendations

NuSMV 2: An OpenSource Tool for Symbolic Model Checking

Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems

A model advisor for NuSMV specifications

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations