Search results for "NuSMV"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
70	Marco Bozzano, Adolfo Villafiorita	The FSAP/NuSMV-SA Safety Analysis Platform.	Int. J. Softw. Tools Technol. Transf.	2007	DBLP DOI BibTeX RDF
70	Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella	NuSMV 2: An OpenSource Tool for Symbolic Model Checking.	CAV	2002	DBLP DOI BibTeX RDF
70	Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri	NUSMV: A New Symbolic Model Checker.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Tools for technology transfer, Temporal logics, Symbolic model checking, Automatic verification
70	Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri	NUSMV: A New Symbolic Model Verifier.	CAV	1999	DBLP DOI BibTeX RDF
69	Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila	Simple Is Better: Efficient Bounded Model Checking for Past LTL.	VMCAI	2005	DBLP DOI BibTeX RDF	Past LTL, Bounded Model Checking, NuSMV
67	Yunja Choi	From NuSMV to SPIN: Experiences with model checking flight guidance systems.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Flight guidance systems, Model checking, SPIN, NuSMV
55	Marco Bozzano, Adolfo Villafiorita	Improving System Reliability via Model Checking: The FSAP/NuSMV-SA Safety Analysis Platform.	SAFECOMP	2003	DBLP DOI BibTeX RDF
53	Orlando Ferrante, Luca Benvenuti, Leonardo Mangeruca, Christos Sofronis, Alberto Ferrari	Parallel NuSMV: A NuSMV Extension for the Verification of Complex Embedded Systems.	SAFECOMP Workshops	2012	DBLP DOI BibTeX RDF
43	Wendy Johnston, Kirsten Winter, Lionel van den Berg, Paul A. Strooper, Peter J. Robinson 0001	Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking.	FM	2006	DBLP DOI BibTeX RDF	partitioned transition relations, clustering, Binary Decision Diagrams, Symbolic model checking, image computation, railway interlockings
41	Tertia Hörne, John A. van der Poll	Planning as model checking: the performance of ProB vs NuSMV.	SAICSIT	2008	DBLP DOI BibTeX RDF	tableaux theorem proving, model checking, planning, satisfiability, BDDs, constraint logic programming
41	Wanwei Liu, Ji Wang 0001, Huowang Chen, Xiaodong Ma, Zhaofei Wang	Symbolic model checking APSL.	Frontiers Comput. Sci. China	2009	DBLP DOI BibTeX RDF	tableau approach, extended NuSMV, symbolic model checking, property specification language
41	Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala	Bounded Model Checking for Weak Alternating Büchi Automata.	CAV	2006	DBLP DOI BibTeX RDF	Weak Alternating Büchi Automata, Bounded Model Checking, PSL, NuSMV
41	Keijo Heljanko, Tommi A. Junttila, Timo Latvala	Incremental and Complete Bounded Model Checking for Full PLTL.	CAV	2005	DBLP DOI BibTeX RDF	PLTL, Complete, Bounded Model Checking, Incremental, NuSMV
41	Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila	Simple Bounded LTL Model Checking.	FMCAD	2004	DBLP DOI BibTeX RDF	linear translation, bounded model checking, LTL, NuSMV
29	Naoki Iwasaki, Katsumi Wasaki	A Meta Hardware Description Language Melasy for Model-Checking Systems.	ITNG	2008	DBLP DOI BibTeX RDF	Hardware/Software co-design and co-verification, Model Checking, Haskell, Design-for-test, Hardware Compilers
29	Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko	Symbolic Step Encodings for Object Based Communicating State Machines.	FMOODS	2008	DBLP DOI BibTeX RDF
29	Roberto Tiella, Adolfo Villafiorita, Silvia Tomasi	FSMC+, a tool for the generation of Java code from statecharts.	PPPJ	2007	DBLP DOI BibTeX RDF	evoting, model checking, code generation, statecharts
29	Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl	Proving the shalls.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF	Formal verification, Software requirements, Model-based development
29	Nikola Bogunovic, Edgar Pek	Model Checking Procedures for Infinite State Systems.	ECBS	2006	DBLP DOI BibTeX RDF
29	Charles Pecheur, Franco Raimondi	Symbolic Model Checking of Logics with Actions.	MoChArt	2006	DBLP DOI BibTeX RDF
29	Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya	Efficient Guided Symbolic Reachability Using Reachability Expressions.	TACAS	2006	DBLP DOI BibTeX RDF
29	Vitus S. W. Lam, Julian A. Padget	An integrated environment for communicating UML statechart diagrams.	AICCSA	2005	DBLP DOI BibTeX RDF
29	Vitus S. W. Lam, Julian A. Padget	Formal Specification and Verification of the SET/A Protocol with an Integrated Approach.	CEC	2004	DBLP DOI BibTeX RDF
29	Michael Huber, Steve King 0001	Towards an Integrated Model Checker for Railway Signalling Data.	FME	2002	DBLP DOI BibTeX RDF	Data verification, hidden formal methods, model checking
27	Ganesha	Simulink to NuSMV Model Translation Challenges.	ISEC	2022	DBLP DOI BibTeX RDF
27	Jonas Fritzsch, Tobias Schmid, Stefan Wagner 0001	Experiences from Large-Scale Model Checking: Verifying a Vehicle Control System with NuSMV.	ICST	2021	DBLP DOI BibTeX RDF
27	Miguel Carrillo, Vladimir Estivill-Castro, David A. Rosenblueth	Model-to-Model Transformations for Efficient Time-domain Verification of Concurrent Models by NuSMV Modules.	MODELSWARD	2020	DBLP DOI BibTeX RDF
27	Daniel Hausmann 0001, Tadeusz Litak, Christoph Rauch, Matthias Zinner	Cheap CTL Compassion in NuSMV.	VMCAI	2020	DBLP DOI BibTeX RDF
27	Daniel Ratiu, Marco Gario, Hannes Schoenhaar	FASTEN: an open extensible framework to experiment with formal specification approaches: using language engineering to develop a multi-paradigm specification environment for NuSMV.	FormaliSE@ICSE	2019	DBLP DOI BibTeX RDF
27	S. Sheerazuddin, S. Anand, R. S. Anish Badhri	A Scheme to Verify Services with Unboundedly many Clients using NuSMV.	CoRR	2018	DBLP BibTeX RDF
27	Ninglin Xu, Zhanyou Ma, Jiulei Jiang, Panqing Zhang	Model Checking Instance Based on NuSMV.	SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI	2018	DBLP DOI BibTeX RDF
27	Salma Ayari, Yousra Bendaly Hlaoui, Leila Jemni Ben Ayed	A Refinement based Verification Approach of BPMN Models using NuSMV.	ICSOFT	2018	DBLP DOI BibTeX RDF
27	Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene	NuSeen: A Tool Framework for the NuSMV Model Checker.	ICST	2017	DBLP DOI BibTeX RDF
27	Kazuya Nakahori, Shingo Yamaguchi	A support tool to design IoT services with NuSMV.	ICCE	2017	DBLP DOI BibTeX RDF
27	Yongho Kim, Jin-Woo Jung, John C. Gallagher, Eric T. Matson	An Adaptive Goal-Based Model for Autonomous Multi-Robot Using HARMS and NuSMV.	Int. J. Fuzzy Log. Intell. Syst.	2016	DBLP DOI BibTeX RDF
27	Jingyue Li, Altin Qeriqi, Martin Steffen, Ingrid Chieh Yu	Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems.	NIK	2016	DBLP BibTeX RDF
27	Pawel Gluchowski	NuSMV Model Verification of an Airport Traffic Control System with Deontic Rules.	DepCoS-RELCOMEX	2016	DBLP DOI BibTeX RDF
27	Georgiana Caltais, Florian Leitner-Fischer, Stefan Leue, Jannis Weiser	SysML to NuSMV Model Transformation via Object-Orientation.	CyPhy	2016	DBLP DOI BibTeX RDF
27	Piotr Szwed	Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV.	ISM/AITM	2015	DBLP DOI BibTeX RDF
27	Piotr Szwed	Efficiency of formal verification of ArchiMate business processes with NuSMV model checker.	FedCSIS	2015	DBLP DOI BibTeX RDF
27	Yongho Kim, Jin-Woo Jung, Eric T. Matson	An Adaptive Task-Based Model for Autonomous Multi-Robot Using HARMS and NuSMV.	FNC/MobiSPC	2015	DBLP DOI BibTeX RDF
27	Yongho Kim, Mauricio Gomez, James Goppert, Eric T. Matson	Model Checking of a Training System Using NuSMV for Humanoid Robot Soccer.	RiTA	2014	DBLP DOI BibTeX RDF
27	Marcin Szpyrka, Agnieszka Biernacka, Jerzy Biernacki	Methods of Translation of Petri Nets to NuSMV Language.	CS&P	2014	DBLP BibTeX RDF
27	Takashi Kitamura 0001, Keishi Okamoto	Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker.	IEICE Trans. Inf. Syst.	2013	DBLP DOI BibTeX RDF
27	Arne-Michael Törsel	A Testing Tool for Web Applications Using a Domain-Specific Modelling Language and the NuSMV Model Checker.	ICST	2013	DBLP DOI BibTeX RDF
27	Simon Busard, Charles Pecheur	PyNuSMV: NuSMV as a Python Library.	NASA Formal Methods	2013	DBLP DOI BibTeX RDF
27	Supriya D'Souza, Abhishek Rao, Amit Sharma, Sanjay Singh	Modeling and Verification of a Multi-Agent Argumentation System using NuSMV	CoRR	2012	DBLP BibTeX RDF
27	Yong Jiang, Zongyan Qiu	S2N: Model Transformation from SPIN to NuSMV - (Tool Paper).	SPIN	2012	DBLP DOI BibTeX RDF
27	Aditya Sinha, Ajay Ry, Sanjay Singh 0002	Modeling & verification of Sliding Window Protocol with data loss and intruder detection using NuSMV.	CCSEIT	2012	DBLP DOI BibTeX RDF
27	Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene	A model advisor for NuSMV specifications.	Innov. Syst. Softw. Eng.	2011	DBLP DOI BibTeX RDF
27	Yan Cao, Qiuzi Lu, Tianhua Xu, Tao Tang 0004, Haifeng Wang, Yongcheng Xu	Integrating DSL-CBI and NuSMV for Modeling and Verifiying Interlocking Systems.	SSIRI (Companion)	2011	DBLP DOI BibTeX RDF
27	Vikram Saralaya, J. K. Kishore, Sateesh Reddy, Radhika M. Pai, Sanjay Singh 0002	Modeling and Verification of Chess Game Using NuSMV.	ACC (2)	2011	DBLP DOI BibTeX RDF
27	Vitus S. W. Lam	Formal Analysis of BPMN Models: a NuSMV-Based Approach.	Int. J. Softw. Eng. Knowl. Eng.	2010	DBLP DOI BibTeX RDF
27	Alessandro Ferrante, Maurizio Memoli, Margherita Napoli, Mimmo Parente, Francesco Sorrentino 0002	A NuSMV Extension for Graded-CTL Model Checking.	CAV	2010	DBLP DOI BibTeX RDF
27	Giuseppe Di Guglielmo, Franco Fummi, Graziano Pravadelli, Stefano Soffia, Marco Roveri	Semi-formal functional verification by EFSM traversing via NuSMV.	HLDVT	2010	DBLP DOI BibTeX RDF
27	Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene	AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications.	ASM	2010	DBLP DOI BibTeX RDF
27	Yefei Zhao, Zongyuan Yang, Jinkui Xie, Qiang Liu	Formal Model and Analysis of Sliding Window Protocol Based on NuSMV.	J. Comput.	2009	DBLP BibTeX RDF
27	Melissa Kova, Jamal Bentahar, Zakaria Maamar, Hamdi Yahyaoui	A Formal Verification Approach of Conversations in Composite Web Services Using NuSMV.	SoMeT	2009	DBLP DOI BibTeX RDF
27	Masaya Kadono, Tatsuhiro Tsuchiya, Tohru Kikuno	Using the NuSMV Model Checker for Test Generation from Statecharts.	PRDC	2009	DBLP DOI BibTeX RDF
27	Amin Ansari	Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV	CoRR	2008	DBLP BibTeX RDF
27	Alessio Lomuscio, Charles Pecheur, Franco Raimondi	Automatic Verification of Knowledge and Time with NuSMV.	IJCAI	2007	DBLP BibTeX RDF
27	Grygoriy Bunin, Axel Schneider, Christian Haubelt, Jan Langer, Ulrich Heinkel	Automatic Test Case Generation with NuSMV.	GI Jahrestagung (2)	2006	DBLP BibTeX RDF
26	Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila	Efficient Model Checking of PSL Safety Properties.	ACSD	2010	DBLP DOI BibTeX RDF	model checking, safety properties, PSL, NuSMV
26	Nalini Vasudevan, Olivier Tardieu, Julian Dolby, Stephen A. Edwards	Compile-Time Analysis and Specialization of Clocks in Concurrent Programs.	CC	2009	DBLP DOI BibTeX RDF	Concurrency, Synchronization, Static Analysis, Clocks, X10, NuSMV
14	Alessandro Ferrante, Margherita Napoli, Mimmo Parente	Graded-CTL: Satisfiability and Symbolic Model Checking.	ICFEM	2009	DBLP DOI BibTeX RDF
14	Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li	Model Checking Coalition Nash Equilibria in MAD Distributed Systems.	SSS	2009	DBLP DOI BibTeX RDF
14	Kenichi Yajima, Shoichi Morimoto, Daisuke Horie, Noor Sheila Azreen, Yuichi Goto, Jingde Cheng	FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408.	ARES	2009	DBLP DOI BibTeX RDF
14	Hrishikesh Karmarkar, Supratik Chakraborty	On Minimal Odd Rankings for Büchi Complementation.	ATVA	2009	DBLP DOI BibTeX RDF
14	Ram Krishnan, Ravi S. Sandhu, Jianwei Niu 0001, William H. Winsborough	Foundations for group-centric secure information sharing models.	SACMAT	2009	DBLP DOI BibTeX RDF	groups, linear temporal logic, security properties
14	Baolin Shao, Nalini Vasudevan, Stephen A. Edwards	Compositional deadlock detection for rendezvous communication.	EMSOFT	2009	DBLP DOI BibTeX RDF	SHIM, concurrency, static analysis, deadlock, divide-and-conquer
14	Wei Chen 0018, Wenhui Zhang	Bounded Model Checking of ACTL Formulae.	TASE	2009	DBLP DOI BibTeX RDF
14	Wonhong Nam, P. Madhusudan, Rajeev Alur	Automatic symbolic compositional verification by learning assumptions.	Formal Methods Syst. Des.	2008	DBLP DOI BibTeX RDF	Regular language learning, Formal verification, Symbolic model checking, Compositional verification, Assume-guarantee reasoning, Hypergraph partitioning
14	Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya	Efficient guided symbolic reachability using reachability expressions.	Int. J. Softw. Tools Technol. Transf.	2008	DBLP DOI BibTeX RDF
14	Nan Guan, Zonghua Gu 0001, Mingsong Lv, Qingxu Deng, Ge Yu 0001	Schedulability Analysis of Global Fixed-Priority or EDF Multiprocessor Scheduling with Symbolic Model-Checking.	ISORC	2008	DBLP DOI BibTeX RDF	Schedulability, real-time scheduling, symbolic model-checking
14	Kais Klai, Denis Poitrenaud	MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs.	Petri Nets	2008	DBLP DOI BibTeX RDF
14	Moonzoo Kim, Yunja Choi, Yunho Kim, Hotae Kim	Formal Verification of a Flash Memory Device Driver - An Experience Report.	SPIN	2008	DBLP DOI BibTeX RDF
14	Ralf Huuck, Ansgar Fehnker, Sean Seefried, Jörg Brauer	Goanna: Syntactic Software Model Checking.	ATVA	2008	DBLP DOI BibTeX RDF
14	Moonzoo Kim, Yunja Choi, Yunho Kim, Hotae Kim	Pre-testing Flash Device Driver through Model Checking Techniques.	ICST	2008	DBLP DOI BibTeX RDF	Model Checking, Testing, Embedded Software
14	Yanyan Gao 0001, Xi Li 0003	Formal Verification of Bypassed Processor Pipelines.	ICYCS	2008	DBLP DOI BibTeX RDF
14	Ronald Toegl, Georg Hofferek, Karin Greimel, Adrian Leung, Raphael Chung-Wei Phan, Roderick Bloem	Formal Analysis of a TPM-Based Secrets Distribution and Storage Scheme.	ICYCS	2008	DBLP DOI BibTeX RDF
14	Konstantinos Aisopos, Chien-Chun Chou, Li-Shiuan Peh	Extending open core protocol to support system-level cache coherence.	CODES+ISSS	2008	DBLP DOI BibTeX RDF	coherence extensions, ocp, open core protocol, specification, mpsocs
14	Eyad Alkassar, Peter Böhm, Steffen Knapp	Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level.	DIPES	2008	DBLP DOI BibTeX RDF
14	Junhua Ding, Mohammad H. N. Tabrizi	Modeling and Model Checking of a Clinical Diagnostic Algorithm.	ICNSC	2008	DBLP DOI BibTeX RDF
14	Radu Siminiceanu, Gianfranco Ciardo	Formal verification of the NASA runway safety monitor.	Int. J. Softw. Tools Technol. Transf.	2007	DBLP DOI BibTeX RDF	Model checkinga, Aviation safetya, Collision avoidance protocols, Formal verification
14	Susanne Kandl, Raimund Kirner, Peter P. Puschner	Automated Formal Verification and Testing of C Programs for Embedded Systems.	ISORC	2007	DBLP DOI BibTeX RDF
14	Ka Lok Man, Andrea Fedeli, Michele Mercaldi, Menouer Boubekeur, Michel P. Schellekens	SC2SCFL: Automated SystemC to SystemCFL Translation.	SAMOS	2007	DBLP DOI BibTeX RDF
14	Cheng-Hong Li, Rebecca L. Collins, Sampada Sonalkar, Luca P. Carloni	Design, Implementation, and Validation of a New Class of Interface Circuits for Latency-Insensitive Design.	MEMOCODE	2007	DBLP DOI BibTeX RDF
14	Kristin Y. Rozier, Moshe Y. Vardi	LTL Satisfiability Checking.	SPIN	2007	DBLP DOI BibTeX RDF
14	Gordon J. Pace, Cristian Prisacariu, Gerardo Schneider	Model Checking Contracts - A Case Study.	ATVA	2007	DBLP DOI BibTeX RDF
14	Yongyan Zheng, Jiong Zhou, Paul Krause	A Model Checking based Test Case Generation Framework forWeb Services.	ITNG	2007	DBLP DOI BibTeX RDF
14	Lionel van den Berg, Paul A. Strooper, Kirsten Winter	Introducing Time in an Industrial Application of Model-Checking.	FMICS	2007	DBLP DOI BibTeX RDF	real-time system, model checking, railway interlockings
14	Zoë R. Stephenson, John A. McDermid	Using Model Checking to Validate Style-Specific Architectural Refactoring Patterns.	SEW	2007	DBLP DOI BibTeX RDF
14	Zonghua Gu 0001, Mingxuan Yuan, Nan Guan, Mingsong Lv, Xiuqiang He 0001, Qingxu Deng, Ge Yu 0001	Static Scheduling and Software Synthesis for Dataflow Graphs with Symbolic Model-Checking.	RTSS	2007	DBLP DOI BibTeX RDF
14	Mihaela Gheorghiu, Arie Gurfinkel, Marsha Chechik	Finding State Solutions to Temporal Logic Queries.	IFM	2007	DBLP DOI BibTeX RDF
14	Frederic Doucet, R. K. Shyamasundar, Ingolf H. Krüger, Saurabh Joshi 0001, Rajesh K. Gupta 0001	Reactivity in SystemC Transaction-Level Models.	Haifa Verification Conference	2007	DBLP DOI BibTeX RDF
14	Yongyan Zheng, Jiong Zhou, Paul Krause	Analysis of BPEL Data Dependencies.	EUROMICRO-SEAA	2007	DBLP DOI BibTeX RDF
14	Julien Schmaltz	A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware.	FMCAD	2007	DBLP DOI BibTeX RDF
14	Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch	Model Checking Software at Compile Time.	TASE	2007	DBLP DOI BibTeX RDF
14	Rik Eshuis	Symbolic model checking of UML activity diagrams.	ACM Trans. Softw. Eng. Methodol.	2006	DBLP DOI BibTeX RDF	Model checking, Unified Modeling Language, activity diagrams
14	Gabor Karsai, Anantha Narayanan	On the Correctness of Model Transformations in the Development of Embedded Systems.	Monterey Workshop	2006	DBLP DOI BibTeX RDF