This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
State space, not proof
A subject the papers are about. The loosest grouping, and the one to reach for last.
Model checking: verification by searching a system's states rather than deriving its properties, from temporal logic through the explicit, BDD-based and SAT-based algorithms and the tools that run them. Membership: the method is model checking.
134 references
Complete SEU Vulnerable Register Enumeration using Property Directed Reachability
Félix Ridoux and others (2026)
SecIC3: Customizing IC3 for Hardware Security Verification
Qinhan Tan and others (2026) · Design, Automation and Test in Europe (DATE 2026)
Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
Nick Waddoups and others (2025) · Verification, Model Checking, and Abstract Interpretation (VMCAI 2026)
FRAIG-BMC: Functional Reduction to Speed Up Bounded Model Checking
Changyuan Yu and others (2025)
Hardware Model Checking Algorithms and Techniques
Gianpiero Cabodi and others (2024) · Algorithms · Multidisciplinary Digital Publishing Institute
Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking
Jiahui Xu and others (2023) · ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA)
GenMC: A Model Checker for Weak Memory Models
Michalis Kokologiannakis and others (2021) · Springer International Publishing
Pono: A Flexible and Extensible SMT-Based Model Checker
Makai Mann and others (2021) · Computer Aided Verification · Springer International Publishing
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
Riley Roberts and others (2021) · Formal Methods for Industrial Critical Systems (FMICS 2021)
Modular SMT-Based Verification of Rule-Based Hardware Designs
Andrew C. Wright (2021)
NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
Y. Yuan and others (2020) · 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)
Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction
Aman Goel and others (2019) · Lecture notes in computer science · Springer Science+Business Media
Model checking for weakly consistent libraries
Michalis Kokologiannakis and others (2019) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits
Aymane Bouzafour and others (2018) · 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC) · IEEE
Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking
Randal E. Bryant (2018) · Handbook of Model Checking · Springer International Publishing
Handbook of Model Checking
Edmund M. Clarke and others (2018) · Springer International Publishing
Explicit-State Model Checking
Gerard J. Holzmann (2018) · Springer Nature
Model Checking of C and C++ with DIVINE 4
Zuzana Baranová and others (2017) · Automated Technology for Verification and Analysis · Springer International Publishing
Effective stateless model checking for C/C++ concurrency
Michalis Kokologiannakis and others (2017) · Association for Computing Machinery (ACM)
Plasma Lab Statistical Model Checker: Architecture, Usage and Extension
Axel Legay and others (2017) · 43rd International Conference on Current Trends in Theory and Practice of Computer Science
WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction
A. Mangean and others (2017) · Springer International Publishing
Model Checking of Embedded Assembly Program Based on Simulation
Satoshi Yamane and others (2017) · Institute of Electronics, Information and Communications Engineers (IEICE)
Hardware Model Checking Competition 2014: An Analysis and Comparison of Model Checkers and Benchmarks
Gianpiero Cabodi and others (2016) · Journal on Satisfiability, Boolean Modeling and Computation
Model checking usage policies
Massimo Bartoletti and others (2015) · Cambridge University Press (CUP)
Dependable Horizontal Scaling Based on Probabilistic Model Checking
A. Naskos and others (2015) · IEEE
Combining Symbolic Execution and Model Checking for Data Flow Testing
Ting Su (2015) · IEEE
The nuXmv Symbolic Model Checker
Roberto Cavada and others (2014) · Lecture notes in computer science · Springer Science+Business Media
CBMC – C Bounded Model Checker
Daniel Kroening and others (2014) · Lecture notes in computer science · Springer Science+Business Media
Sequoll: A framework for model checking binaries
B. Blackham and others (2013) · IEEE
Model Checking and the State Explosion Problem
Edmund M. Clarke and others (2012) · Lecture notes in computer science · Springer Science+Business Media
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
Florian Merz and others (2012) · Lecture notes in computer science · Springer Science+Business Media
LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation
Carsten Sinz and others (2012) · Lecture notes in computer science · Springer Science+Business Media
SAT-Based Model Checking without Unrolling
Aaron R. Bradley (2011) · Verification, Model Checking, and Abstract Interpretation (VMCAI) · Springer Berlin Heidelberg
Efficient implementation of property directed reachability
Niklas Eén and others (2011) · Formal Methods in Computer-Aided Design (FMCAD) · FMCAD Inc.
Linear Completeness Thresholds for Bounded Model Checking
D. Kroening and others (2011) · Springer Berlin Heidelberg
Analog Circuit Verification by Statistical Model Checking
Ying-Chih Wang and others (2011) · 16th Asia and South Pacific Design Automation Conference (ASP-DAC 2011)
Metamoc: Modular execution time analysis using model checking
A. Dalsgaard and others (2010) · WCET
Proactive Detection of Computer Worms Using Model Checking
Johannes Kinder and others (2010) · IEEE Transactions on Dependable and Secure Computing · IEEE Computer Society
Statistical Model Checking: An Overview
Axel Legay and others (2010) · Runtime Verification · Springer Berlin Heidelberg
Software model checking takes off
Steven P. Miller and others (2010) · Association for Computing Machinery (ACM)
Linear Temporal Logic Symbolic Model Checking
Kristin Yvonne Rozier (2010) · Computer Science Review · Elsevier BV
Model checking: Algorithmic verification and debugging
Edmund M. Clarke and others (2009) · Communications of the ACM · Association for Computing Machinery
Interpolation-sequence based model checking
Yakir Vizel and others (2009) · 2009 Formal Methods in Computer-Aided Design · IEEE
Principles of Model Checking
Christel Baier and others (2008) · The MIT Press
The Beginning of Model Checking: A Personal Perspective
E. Allen Emerson (2008) · Lecture notes in computer science · Springer Science+Business Media
Symbolic Execution and Model Checking for Testing
Corina S. Păsăreanu and others (2008) · Springer Nature
Challenges in embedded model checking — a simulator for the [mc]square model checker
Thomas Reinbacher and others (2008) · International Symposium on Industrial Embedded Systems
Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis
Bernhard Rieder and others (2008)
Verifying Compiler Based Refinement of Bluespec TM Specifications Using the SPIN Model Checker
Gaurav Kumar Singh and others (2008) · Lecture notes in computer science · Springer Science+Business Media
Model Checking Bluespec Specified Hardware Designs
Gaurav Kumar Singh and others (2007)
Model checking restricted sets of timed paths
Nicolas Markey and others (2006) · Theoretical Computer Science · Elsevier BV
PSL Model Checking and Run-Time Verification Via Testers
A. Pnueli and others (2006) · Springer Berlin Heidelberg
[mc]square: A Model Checker for Microcontroller Code
Bastian Schlich and others (2006)
Verification System for Transient Response of Analog Circuits Using Model Checking
T.R. Dastidar and others (2005) · Verification System for Transient Response of Analog Circuits Using Model Checking, VLSID’05
Integration of a Software Model Checker into Isabelle
M. Daum and others (2005) · Springer Berlin Heidelberg
Model Checking Machine Code with the GNU Debugger
Eric Mercer and others (2005) · Springer Berlin Heidelberg
Bounded Model Checking of Concurrent Programs
Ishai Rabinovitz and others (2005) · Springer Berlin Heidelberg
The SPIN model checker: Primer and reference manual, volume 1003
Gerard J Holzmann (2004) · Addison-Wesley Reading
Why Model Checking Can Improve WCET Analysis
Alexander Metzner (2004) · Lecture notes in computer science · Springer Science+Business Media
Bounded Model Checking
Armin Biere and others (2003) · Advances in computers · Elsevier BV
Counterexample-guided abstraction refinement for symbolic model checking
Edmund Clarke and others (2003) · Journal of the ACM · Association for Computing Machinery (ACM)
Model Checking a Path
N. Markey and others (2003) · Springer Berlin Heidelberg
Interpolation and SAT-Based Model Checking
K. L. McMillan (2003) · Springer Berlin Heidelberg
Introduction to StEAM-an assembly-level software model checker
Tilman Mehler and others (2003)
Bounded Model Checking and Induction: From Refutation to Verification
Leonardo De Moura and others (2003) · Springer Berlin Heidelberg
Model Checking Programs
Willem Visser (2003) · Springer Science and Business Media LLC
Verification of Asynchronous Circuits using Timed Automata
Marius Bozga and others (2002) · Electronic Notes in Theoretical Computer Science: Theory and Practice of Timed Systems (TPTS 2002)
NuSMV 2: An OpenSource Tool for Symbolic Model Checking
A. Cimatti (2002) · Springer Berlin Heidelberg
Comparing Symbolic and Explicit Model Checking of a Software System
C. Eisner and others (2002) · Springer Berlin Heidelberg
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving
C. Jacobi (2002) · Springer Berlin Heidelberg
Systems and Software Verification: Model-Checking Techniques and Tools
B. Bérard and others (2001) · Springer Berlin Heidelberg
Bounded Model Checking Using Satisfiability Solving
Edmund Clarke and others (2001) · Springer Science and Business Media LLC
Progress on the State Explosion Problem in Model Checking
E. Clarke and others (2001) · Springer Berlin Heidelberg
Microarchitecture Verification by Compositional Model Checking
Ranjit Jhala and others (2001) · Lecture notes in computer science · Springer Science+Business Media
Model Checking of Safety Properties
O. Kupferman and others (2001) · Springer Science and Business Media LLC
Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability
M. Kwiatkowska and others (2000) · Kwiatkowska, N. Gethin, and J. Sproston, Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachab
Cadence smv
K. McMillan (2000) · Cadence Berkeley Labs, CA
A methodology for hardware verification using compositional model checking
Kenneth L. McMillan (2000) · Science of Computer Programming · Elsevier BV
Modeling and verification of embedded systems using Cadence SMV
A. Mir and others (2000) · IEEE
Checking Safety Properties Using Induction and a SAT-Solver
Mary Sheeran and others (2000) · Formal Methods in Computer-Aided Design (FMCAD 2000) · Springer Science+Business Media
Symbolic Model Checking without BDDs
Armin Biere and others (1999) · Tools and Algorithms for the Construction and Analysis of Systems (TACAS) · Springer Science+Business Media
Symbolic model checking using SAT procedures instead of BDDs
Armin Biere and others (1999) · ACM
Model Checking
Edmund M. Clarke and others (1999) · MIT Press
Model Checking TLA+ Specifications
Yuan Yu and others (1999) · Lecture notes in computer science · Springer Science+Business Media
Combining symbolic model checking with uninterpreted functions for out-of-order processor verification
S. Berezin and others (1998) · FMCAD ’98, LNCS 1522 · Springer
Verification of an implementation of Tomasulo's algorithm by compositional model checking
Kenneth L. McMillan (1998) · Lecture notes in computer science · Springer Science+Business Media
Compositional reasoning in model checking
Sergey Berezin and others (1997) · International Symposium on Compositionality · Springer
Model checking expands verification's scope
Richard Goering (1997)
The model checker SPIN
G. J. Holzmann (1997) · IEEE Transactions on Software Engineering · Institute of Electrical and Electronics Engineers (IEEE)
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking
Yirng-An Chen and others (1996) · Formal Methods in Computer-Aided Design (FMCAD '96)
Word Level Model Checking -- Avoiding the Pentium FDIV Error
E. M. Clarke and others (1996) · 33rd Design Automation Conference (DAC '96) · ACM
Experiments in theorem proving and model checking for protocol verification
Klaus Havelund and others (1996) · Lecture notes in computer science · Springer Science+Business Media
Combining partial order reductions with on-the-fly model-checking
Doron Peled (1996) · Springer Science and Business Media LLC
Model checking in practice: the T9000 virtual channel processor
G. Barrett (1995) · Institute of Electrical and Electronics Engineers (IEEE)
Model Checking in Industrial Hardware Design
Jörg Bormann (1995) · ACM/IEEE Design Automation Conference (DAC) · Association for Computing Machinery
An integration of model checking with automated proof checking
Sreeranga P. Rajan and others (1995) · Lecture notes in computer science · Springer Science+Business Media
Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock
A. W. Roscoe and others (1995) · Tools and Algorithms for the Construction and Analysis of Systems · Springer Berlin Heidelberg
Symbolic model checking for sequential circuit verification
J.R. Burch and others (1994) · Institute of Electrical and Electronics Engineers (IEEE)
Another look at LTL Model Checking
E. M. Clarke and others (1994) · CAV’94
Model checking and abstraction
Edmund M. Clarke and others (1994) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery
Symbolic Model Checking for Real-Time Systems
Thomas A. Henzinger and others (1994) · Information and Computation · Elsevier BV
Model checking for UNITY
M. Kaltenbach (1994) · Tech. Rep. TR94-31
Model-checking CSP
A. Roscoe (1994) · A Classical Mind: Essays in Honour of C.A.R. Hoare
Reasoning about Infinite Computations
Moshe Y. Vardi and others (1994) · Information and Computation · Elsevier BV
Exploiting symmetry in temporal logic model checking
E. M. Clarke and others (1993) · Springer Berlin Heidelberg
Generating BDDs for symbolic model checking in CCS
Reinhard Enders and others (1993) · Springer Science and Business Media LLC
BDD-Based debugging of designs using language containment and fair CTL
Ramin Hojati and others (1993) · Lecture notes in computer science · Springer Science+Business Media
Model checking, abstraction, and compositional reasoning
D. L. Long (1993) · Ph.D. Thesis
Model Checking, Abstraction, and Compositional Verification
David E. Long (1993)
Symbolic Model Checking
Kenneth L. McMillan (1993) · Kluwer Academic Publishers
Symbolic model checking: 10^20 States and beyond
J. R. Burch and others (1992) · Information and Computation · Elsevier BV
Model checking and abstraction
Edmund M. Clarke and others (1992) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Symbolic Model Checking: An Approach to the State Explosion Problem
Kenneth L. McMillan (1992)
Representing circuits more efficiently in symbolic model checking
Jerry R. Burch and others (1991)
Symbolic model checking with partitioned transition relations
J. R. Burch and others (1991) · Proceedings of the IFIP International Conference on Very Large Scale Integration (VLSI 91), Edinburgh
Symbolic model checking with partitioned transition relations
J. R. Burch and others (1991) · Technical Report CMU-CS-9 1-195
A partial approach to model checking
Patrice Godefroid and others (1991) · Proceedings - Symposium on Logic in Computer Science · Institute of Electrical and Electronics Engineers
Model checking and modular verification
Orna Grümberg and others (1991) · Lecture notes in computer science · Springer Science+Business Media
Model Checking vs. Theorem Proving: A Manifesto
Joseph Y Halpern and others (1991) · Elsevier
Using partial-order semantics to avoid the state explosion problem in asynchronous systems
D. K. Probst and others (1991) · American Mathematical Society
Testing language containment for omega-automata using BDDs
H. J. Touati and others (1991) · IMEC-IFIP International Workshop on Formal Methods in VLSI Design, Miami
Symbolic model checking: 10^20 states and beyond
Jerry R. Burch and others (1990) · Proceedings - Symposium on Logic in Computer Science · Institute of Electrical and Electronics Engineers
Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams
M. Fujita and others (1990) · 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers · IEEE Comput. Soc. Press
Implicit state enumeration of finite state machines using BDD's
H. J. Touati and others (1990) · IEEE Comput. Soc. Press
A stubborn attack on state explosion
Antti Valmari (1990) · Springer Nature
Compositional model checking
E. M. Clarke and others (1989)
Automatic Verification of Sequential Circuits Using Temporal Logic
Michael C. Browne and others (1986) · IEEE Transactions on Computers
Automatic verification of finite-state concurrent systems using temporal logic specifications
Edmund M. Clarke and others (1986) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery
Efficient model checking in fragments of the propositional mu-calculus
E. A. Emerson and others (1986) · Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) · IEEE Computer Society Press
An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)
Moshe Y. Vardi and others (1986) · Proceedings of the First Annual Symposium on Logic in Computer Science
Hierarchical Verification of Asynchronous Circuits Using Temporal Logic
Bud Mishra and others (1985) · Theoretical Computer Science · North-Holland
Specification and verification of concurrent systems in CESAR
J. P. Queille and others (1982) · 5th International Symposium on Programming · Springer
Design and synthesis of synchronization skeletons using branching time temporal logic
Edmund M. Clarke and others (1981) · Logic of Programs · Springer
The temporal logic of programs
Amir Pnueli (1977) · 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)