Search results for "NuSMV"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Yunja Choi	From NuSMV to SPIN: Experiences with model checking flight guidance systems.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Flight guidance systems, Model checking, SPIN, NuSMV
2	Wanwei Liu, Ji Wang, Huowang Chen, Xiaodong Ma, Zhaofei Wang	Symbolic model checking APSL.	Frontiers of Computer Science in China	2009	DBLP DOI BibTeX RDF	tableau approach, extended NuSMV, symbolic model checking, property specification language
2	Tertia Hörne, John A. van der Poll	Planning as model checking: the performance of ProB vs NuSMV.	SAICSIT Conf.	2008	DBLP DOI BibTeX RDF	tableaux theorem proving, model checking, planning, satisfiability, BDDs, constraint logic programming
2	Marco Bozzano, Adolfo Villafiorita	The FSAP/NuSMV-SA Safety Analysis Platform.	STTT	2007	DBLP DOI BibTeX RDF
2	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
2	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
2	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
2	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
2	Marco Bozzano, Adolfo Villafiorita	Improving System Reliability via Model Checking: The FSAP/NuSMV-SA Safety Analysis Platform.	SAFECOMP	2003	DBLP DOI BibTeX RDF
2	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
2	Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri	NUSMV: A New Symbolic Model Checker.	STTT	2000	DBLP DOI BibTeX RDF	Tools for technology transfer, Temporal logics, Symbolic model checking, Automatic verification
2	Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri	NUSMV: A New Symbolic Model Verifier.	CAV	1999	DBLP DOI BibTeX RDF
1	Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene	A model advisor for NuSMV specifications.	ISSE	2011	DBLP DOI BibTeX RDF
1	Vikram Saralaya, J. K. Kishore, Sateesh Reddy, Radhika M. Pai, Sanjay Singh	Modeling and Verification of Chess Game Using NuSMV.	ACC	2011	DBLP DOI BibTeX RDF
1	Vitus S. W. Lam	Formal Analysis of BPMN Models: a NuSMV-Based Approach.	International Journal of Software Engineering and Knowledge Engineering	2010	DBLP DOI BibTeX RDF
1	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
1	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
1	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
1	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
1	Yefei Zhao, Zongyuan Yang, Jinkui Xie, Qiang Liu	Formal Model and Analysis of Sliding Window Protocol Based on NuSMV.	JCP	2009	DBLP DOI BibTeX RDF
1	Masaya Kadono, Tatsuhiro Tsuchiya, Tohru Kikuno	Using the NuSMV Model Checker for Test Generation from Statecharts.	PRDC	2009	DBLP DOI BibTeX RDF
1	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
1	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
1	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
1	Ram Krishnan, Ravi S. Sandhu, Jianwei Niu, William H. Winsborough	Foundations for group-centric secure information sharing models.	SACMAT	2009	DBLP DOI BibTeX RDF	groups, linear temporal logic, security properties
1	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
1	Wei Chen 0018, Wenhui Zhang	Bounded Model Checking of ACTL Formulae.	TASE	2009	DBLP DOI BibTeX RDF
1	Hrishikesh Karmarkar, Supratik Chakraborty	On Minimal Odd Rankings for Büchi Complementation.	ATVA	2009	DBLP DOI BibTeX RDF
1	Alessandro Ferrante, Margherita Napoli, Mimmo Parente	Graded-CTL: Satisfiability and Symbolic Model Checking.	ICFEM	2009	DBLP DOI BibTeX RDF
1	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
1	Amin Ansari	Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV	CoRR	2008	DBLP BibTeX RDF
1	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
1	Junhua Ding, Mohammad N. H. Tabrizi	Modeling and Model Checking of a Clinical Diagnostic Algorithm.	ICNSC	2008	DBLP DOI BibTeX RDF
1	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
1	Yanyan Gao, Xi Li	Formal Verification of Bypassed Processor Pipelines.	ICYCS	2008	DBLP DOI BibTeX RDF
1	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
1	Nan Guan, Zonghua Gu, Mingsong Lv, Qingxu Deng, Ge Yu	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
1	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
1	Kais Klai, Denis Poitrenaud	MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs.	Petri Nets	2008	DBLP DOI BibTeX RDF
1	Ralf Huuck, Ansgar Fehnker, Sean Seefried, Jörg Brauer	Goanna: Syntactic Software Model Checking.	ATVA	2008	DBLP DOI BibTeX RDF
1	Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko	Symbolic Step Encodings for Object Based Communicating State Machines.	FMOODS	2008	DBLP DOI BibTeX RDF
1	Eyad Alkassar, Peter Böhm, Steffen Knapp	Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level.	DIPES	2008	DBLP DOI BibTeX RDF
1	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
1	Wonhong Nam, P. Madhusudan, Rajeev Alur	Automatic symbolic compositional verification by learning assumptions.	Formal Methods in System Design	2008	DBLP DOI BibTeX RDF	Regular language learning, Formal verification, Symbolic model checking, Compositional verification, Assume-guarantee reasoning, Hypergraph partitioning
1	Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya	Efficient guided symbolic reachability using reachability expressions.	STTT	2008	DBLP DOI BibTeX RDF
1	Alessio Lomuscio, Charles Pecheur, Franco Raimondi	Automatic Verification of Knowledge and Time with NuSMV.	IJCAI	2007	DBLP BibTeX RDF
1	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
1	Yongyan Zheng, Jiong Zhou, Paul Krause	Analysis of BPEL Data Dependencies.	EUROMICRO-SEAA	2007	DBLP DOI BibTeX RDF
1	Julien Schmaltz	A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware.	FMCAD	2007	DBLP DOI BibTeX RDF
1	Susanne Kandl, Raimund Kirner, Peter P. Puschner	Automated Formal Verification and Testing of C Programs for Embedded Systems.	ISORC	2007	DBLP DOI BibTeX RDF
1	Yongyan Zheng, Jiong Zhou, Paul Krause	A Model Checking based Test Case Generation Framework forWeb Services.	ITNG	2007	DBLP DOI BibTeX RDF
1	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
1	Zonghua Gu, Mingxuan Yuan, Nan Guan, Mingsong Lv, Xiuqiang He, Qingxu Deng, Ge Yu	Static Scheduling and Software Synthesis for Dataflow Graphs with Symbolic Model-Checking.	RTSS	2007	DBLP DOI BibTeX RDF
1	Zoë R. Stephenson, John A. McDermid	Using Model Checking to Validate Style-Specific Architectural Refactoring Patterns.	SEW	2007	DBLP DOI BibTeX RDF
1	Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch	Model Checking Software at Compile Time.	TASE	2007	DBLP DOI BibTeX RDF
1	Gordon J. Pace, Cristian Prisacariu, Gerardo Schneider	Model Checking Contracts - A Case Study.	ATVA	2007	DBLP DOI BibTeX RDF
1	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
1	Frederic Doucet, R. K. Shyamasundar, Ingolf H. Krüger, Saurabh Joshi, Rajesh K. Gupta	Reactivity in SystemC Transaction-Level Models.	Haifa Verification Conference	2007	DBLP DOI BibTeX RDF
1	Mihaela Gheorghiu, Arie Gurfinkel, Marsha Chechik	Finding State Solutions to Temporal Logic Queries.	IFM	2007	DBLP DOI BibTeX RDF
1	Ka Lok Man, Andrea Fedeli, Michele Mercaldi, Menouer Boubekeur, Michel P. Schellekens	SC2SCFL: Automated SystemC to SystemCFL Translation.	SAMOS	2007	DBLP DOI BibTeX RDF
1	Kristin Y. Rozier, Moshe Y. Vardi	LTL Satisfiability Checking.	SPIN	2007	DBLP DOI BibTeX RDF
1	Radu Siminiceanu, Gianfranco Ciardo	Formal verification of the NASA runway safety monitor.	STTT	2007	DBLP DOI BibTeX RDF	Model checkinga, Aviation safetya, Collision avoidance protocols, Formal verification
1	Grygoriy Bunin, Axel Schneider, Christian Haubelt, Jan Langer, Ulrich Heinkel	Automatic Test Case Generation with NuSMV.	GI Jahrestagung	2006	DBLP BibTeX RDF
1	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
1	Nikola Bogunovi, Edgar Pek	Model Checking Procedures for Infinite State Systems.	ECBS	2006	DBLP DOI BibTeX RDF
1	Wonhong Nam, Rajeev Alur	Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition.	ATVA	2006	DBLP DOI BibTeX RDF
1	Wendy Johnston, Kirsten Winter, Lionel van den Berg, Paul A. Strooper, Peter Robinson	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
1	Charles Pecheur, Franco Raimondi	Symbolic Model Checking of Logics with Actions.	MoChArt	2006	DBLP DOI BibTeX RDF
1	Gabor Karsai, Anantha Narayanan	On the Correctness of Model Transformations in the Development of Embedded Systems.	Monterey Workshop	2006	DBLP DOI BibTeX RDF
1	Dina Thomas, Supratik Chakraborty, Paritosh K. Pandya	Efficient Guided Symbolic Reachability Using Reachability Expressions.	TACAS	2006	DBLP DOI BibTeX RDF
1	Steven P. Miller, Alan C. Tribble, Michael W. Whalen, Mats Per Erik Heimdahl	Proving the shalls.	STTT	2006	DBLP DOI BibTeX RDF	Formal verification, Software requirements, Model-based development
1	Vitus S. W. Lam, Julian A. Padget	An integrated environment for communicating UML statechart diagrams.	AICCSA	2005	DBLP DOI BibTeX RDF
1	Rajeev Alur, P. Madhusudan, Wonhong Nam	Symbolic Compositional Verification by Learning Assumptions.	CAV	2005	DBLP DOI BibTeX RDF
1	Toni Jussila, Keijo Heljanko, Ilkka Niemelä	BMC via on-the-fly determinization.	STTT	2005	DBLP DOI BibTeX RDF	Verification, Labeled transition system, Bounded model checking
1	Vitus S. W. Lam, Julian A. Padget	Symbolic Model Checking of UML Statechart Diagrams with an Integrated Approach.	ECBS	2004	DBLP DOI BibTeX RDF
1	Nicolas Markey, Ph. Schnoebelen	TSMV: A Symbolic Model Checker for Quantitative Analysis of Systems.	QEST	2004	DBLP DOI BibTeX RDF
1	Loredana Afanasiev, Massimo Franceschet, Maarten Marx, Maarten de Rijke	CTL Model Checking for Processing Simple XPath Queries.	TIME	2004	DBLP DOI BibTeX RDF
1	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
1	Edmund M. Clarke, Anubhav Gupta, Ofer Strichman	SAT-based counterexample-guided abstraction refinement.	IEEE Trans. on CAD of Integrated Circuits and Systems	2004	DBLP DOI BibTeX RDF
1	Gihwon Kwon, Taehoon Lee	Solving Box-Pushing Games via Model Checking with Optimizations.	ATVA	2004	DBLP DOI BibTeX RDF
1	Nicolas Markey, Ph. Schnoebelen	Symbolic Model Checking for Simply-Timed Systems.	FORMATS/FTRTFT	2004	DBLP DOI BibTeX RDF
1	Richard Banach, R. Cross	Safety Requirements and Fault Trees Using Retrenchment.	SAFECOMP	2004	DBLP DOI BibTeX RDF
1	Marco Benedetti, Sara Bernardini	Incremental Compilation-to-SAT Procedures.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
1	Paul Jackson, Daniel Sheridan	Clause Form Conversions for Boolean Circuits.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
1	Kairong Qian, Albert Nymeyer	Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases.	TACAS	2004	DBLP DOI BibTeX RDF
1	Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, Fabio Martinelli, Simone Tini, Enrico Tronci	Automated analysis of timed security: a case study on web privacy.	Int. J. Inf. Sec.	2004	DBLP DOI BibTeX RDF	Web privacy, Model checking tools, Timed behavior
1	Ariel Fuxman, Lin Liu, John Mylopoulos, Marco Roveri, Paolo Traverso	Specifying and analyzing early requirements in Tropos.	Requir. Eng.	2004	DBLP DOI BibTeX RDF	Early requirements specifications, Model checking, Formal methods
1	Alessio Lomuscio, Franco Raimondi, Marek J. Sergot	Towards model checking interpreted systems.	AAMAS	2003	DBLP DOI BibTeX RDF	model checking, epistemic logic, deontic logic, interpreted systems
1	Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith	Counterexample-guided abstraction refinement for symbolic model checking.	J. ACM	2003	DBLP DOI BibTeX RDF	temporal logic, Abstraction, symbolic model checking, hardware verification
1	Eugenio Di Sciascio, Francesco M. Donini, Marina Mongiello, Giacomo Piscitelli	Web Applications Design and Maintenance Using Symbolic Model Checking.	CSMR	2003	DBLP DOI BibTeX RDF
1	Yunja Choi, Mats Per Erik Heimdahl	Model Checking Software Requirement Specifications using Domain Reduction Abstraction.	ASE	2003	DBLP DOI BibTeX RDF
1	Ariel Fuxman, Lin Liu, Marco Pistore, Marco Roveri, John Mylopoulos	Specifying and Analyzing Early Requirements: Some Experimental Results.	RE	2003	DBLP DOI BibTeX RDF
1	Gianfranco Ciardo, Radu Siminiceanu	Structural Symbolic CTL Model Checking of Asynchronous Systems.	CAV	2003	DBLP DOI BibTeX RDF
1	Nathalie Chabrier, François Fages	Symbolic Model Checking of Biochemical Networks.	CMSB	2003	DBLP DOI BibTeX RDF
1	Mats Per Erik Heimdahl, Sanjai Rayadurgam, Willem Visser, George Devaraj, Jimin Gao	Auto-generating Test Sequences Using Model Checkers: A Case Study.	FATES	2003	DBLP DOI BibTeX RDF
1	Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl	Proving the Shalls.	FME	2003	DBLP DOI BibTeX RDF
1	Marco Benedetti, Alessandro Cimatti	Bounded Model Checking for Past LTL.	TACAS	2003	DBLP DOI BibTeX RDF
1	Paul Ammann, Duminda Wijesekera, Saket Kaushik	Scalable, graph-based network vulnerability analysis.	ACM Conference on Computer and Communications Security	2002	DBLP DOI BibTeX RDF	monotonic analysis, model checking, scalability, network security, vulnerability, exploit
1	Gianpiero Cabodi, Paolo Camurati, Stefano Quer	Can BDDs compete with SAT solvers on bounded model checking?	DAC	2002	DBLP DOI BibTeX RDF	model checking, formal verification, SAT, BDDs
1	Yunja Choi, Mats Per Erik Heimdahl	Model Checking RSML-e Requirements.	HASE	2002	DBLP DOI BibTeX RDF