A survey of recent advances in SAT-based formal verification

Untitled work

(1979) · Cited by 43,841

Graph-Based Algorithms for Boolean Function Manipulation

Bryant (1986) · IEEE Transactions on Computers · doi:10.1109/tc.1986.1676819 · Cited by 8,941

Model checking

Clarke, E. M., Grümberg, O., & Long, D. (1996) · Cited by 6,877

Model Checking

Clarke, E. M., & Schlingloff, B. (1999) · Cited by 4,237

Temporal and Modal Logic

Emerson, E. (1991) · Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics · doi:10.1016/b978-0-444-88074-1.50021-4 · Cited by 3,268

A machine program for theorem-proving

Davis, M. D., Logemann, G. W., & Loveland, D. W. (1962) · Communications of the ACM · doi:10.1145/368273.368557 · Cited by 3,240

Chaff

Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/378239.379017 · Cited by 2,954

Symbolic model checking

Clarke, E., McMillan, K. L., Campos, S., & Hartonas-Garmhausen, V. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61474-5_93 · Cited by 2,846

A Computing Procedure for Quantification Theory

Davis, M. D., & Putnam, H. (1960) · Journal of the ACM · doi:10.1145/321033.321034 · Cited by 2,657

Design and synthesis of synchronization skeletons using branching time temporal logic

Clarke, E. M., & Emerson, E. A. (2005) · Springer eBooks · doi:10.1007/bfb0025774 · Cited by 2,223

Verilog Transformation for an RTL SAT Solver in Formal Verification

Yang, X., Bian, J., Deng, S., & Zhao, Y. (2007) · International Conference on Communications, Circuits and Systems · doi:10.1109/icccas.2007.4348294 · Cited by 1

Improving generation method for test pattern based on BDD learning

Liu, X. (2011) · IEEE International Conference on Electronic Measurement & Instruments · doi:10.1109/icemi.2011.6037887 · Cited by 1

iPSL: An Environment for IP-Based PSL Specification

Jin, N., Zhou, J., & Ni, T. (2008) · IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) · doi:10.1109/iceccs.2008.13 · Cited by 1

Optimizations and Complexity Analysis on the Reversible Level

Abdessaied, N., & Drechsler, R. (2016) · Springer eBooks · doi:10.1007/978-3-319-31937-7_3 · Cited by 1

Optimization and Complexity Analysis on the Mapping Level

Abdessaied, N., & Drechsler, R. (2016) · Springer eBooks · doi:10.1007/978-3-319-31937-7_4 · Cited by 1

Tractable Classes in Exactly-One-SAT

Boumarafi, Y. M., & Salhi, Y. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-99344-7_18 · Cited by 1

BETWEEN PROOF CONSTRUCTION AND SAT-SOLVING

SCHUBERT, A., Urzyczyn, P., & ZDANOWSKI, K. (2025) · Journal of Symbolic Logic · doi:10.1017/jsl.2025.10090 · Cited by 1

Symmetries in Modal Logics

Areces, C., Hoffmann, G., & Orbe, E. (2013) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.113.6 · Cited by 1

Hardware/Firmware Verification of Graphic IP

Romain, K. (2007) · International Workshop on Rapid System Prototyping (RSP) · doi:10.1109/rsp.2007.25 · Cited by 1

Some advances in tools and algorithms for the construction and analysis of systems

Christel Baier, A., & Tinelli, C. (2017) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-017-0471-4 · Cited by 1

Simplified model for automatic QCA circuitry verification

Sardinha, L. H. B., Neto, O. P. V., Orlandi, V. B., & Campos, S. (2017) · Symposium on Integrated Circuits and Systems Design · doi:10.1145/3109984.3110011 · Cited by 1

Verification by Gambling on Program Slices

Akhundov, M. D., Mora, F., Feng, N., Hui, V., & Chećhik, M. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-88885-5_18 · Cited by 1

Background

Abdessaied, N., & Drechsler, R. (2016) · Springer eBooks · doi:10.1007/978-3-319-31937-7_2 · Cited by 1

Branching Strategy Selection Approach Based on Vivification Ratio

Luo, M., Li, C.-M., Wu, X., Li, S., & Lv, Z. (2022) · International Journal of Software and Informatics · doi:10.21655/ijsi.1673-7288.00278 · Cited by 1

The Verification Universe

Wagner, I., & Bertacco, V. (2010) · Springer eBooks · doi:10.1007/978-1-4419-8034-2_2 · Cited by 1

Conception et mise en oeuvre d'un outil déclaratif pour l'analyse des réseaux génétiques discrets

Corblin, F. (2008) · HAL · Cited by 1

A proposal for model-based automation of enterprise service change management processes

Latasa, F. C. (2009) · doi:10.20868/upm.thesis.4294 · Cited by 1

Modular Checking with Model Checking

Hashimoto, Y., & Nakajima, S. (2009) · Electronic Notes in Theoretical Computer Science · doi:10.1016/j.entcs.2009.09.062 · Cited by 1

Weak Functional Dependencies: Full Propositional Expressiveness for the Database Practitioner

Link, S., & Hartmann, S. (2020) · doi:10.3217/jucs-015-01-0112 · Cited by 1

Search-space Aware Learning Techniques for Unbounded Model Checking and Path Delay Testing

Chandrasekar, K. (2006) · VTechWorks (Virginia Tech) · Cited by 1

Sequential Equivalence Checking of Circuits with Different State Encodings by Pruning Simulation-based Multi-Node Invariants

Yuan, Z. (2015) · VTechWorks (Virginia Tech) · Cited by 1

Automated Generation of Directed Tests

Chen, M., Qin, X., Koo, H.-M., & Mishra, P. (2012) · Springer eBooks · doi:10.1007/978-1-4614-1359-2_3

Solving polynomial constraints for proving termination of rewriting

Navarro-Marset, R. (2011)

Strategia weryfikacji systemu na chipie oparta na mechaniźmie FDL

Pułka, A. (2010) · Elektronika : konstrukcje, technologie, zastosowania

A Review on Multicore Architecture and their Validation

Ramalakshmi., R., & Rajamunipriya., R. (2014)

ASERE: Assuring the Satisfiability of Sequential Extended Regular Expressions

Jin, N., & Zhu, H. (2008) · Communications in computer and information science · doi:10.1007/978-3-540-88479-8_17

From Total Assignment Enumeration to Modern SAT SolverPreprint

Dershowitz, N., & Nadel, A. (2011) · arXiv (Cornell University) · doi:10.48550/arxiv.1110.5867

Pourquoi les solveurs SAT modernes se piquent-ils contre des cactus ?

Audemard, G., Modeliar, M. S., & Simon, L. (2009) · HAL

Assisting Groupware Development with Model Checking - Case Studies from Cooperative Work in the WWW

Papadopoulos, C. (2007) · The Open Information Systems Journal · doi:10.2174/1874133900701010001

Verifying Absence of ∞ Loops in Parameterized Protocols

Saksena, M. (2008)

Achieving High Availability of Consistent Data in the Presence of Network Partitions

Tsuchiya, T. (2012) · Autonomic and Trusted Computing · doi:10.1109/uic-atc.2012.127

Implementing Symbolic Simulation Using SAT Solvers by Variables Partition

Yan, W., & Wu, J. (2009) · IEEE Circuits and Systems International Conference on Testing and Diagnosis (ICTD) · doi:10.1109/cas-ictd.2009.4960831

Using Bounded Model Checking with BOGOR

Lee, T., Cho, M., & Kwon, G. (2007) · IEEE/ACIS International Conference on Software Engineering Research, Management and Applications (SERA) · doi:10.1109/sera.2007.132

Invariant detection meets Random test case generation

Veloso, T. A. (2011) · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT)

Correct low power design transformations for hardware systems

Viswanath, V. (2013) · Texas ScholarWorks (Texas Digital Library)

Mining constraints for Testing and Verification

Wu, W. (2009)

Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving

Deng, S., Wu, W., & Bian, J. (2007) · Springer eBooks · doi:10.1007/978-3-540-72863-4_31

Test Generation Using Design and Property Decompositions

Chen, M., Qin, X., Koo, H.-M., & Mishra, P. (2012) · Springer eBooks · doi:10.1007/978-1-4614-1359-2_8

SAT-Based ATPG for Digital Integrated Circuits Based on Multiple Observations

Leung, D. (2007) · MacSphere (McMaster University) · doi:10.71548/6377

Sequential Equivalence Checking with Efficient Filtering Strategies for Inductive Invariants

Nguyễn, H. L. (2011) · VTechWorks (Virginia Tech)

GuidingCNF-SAT SearchbyAnalyzing Constraint-Variable Dependencies andClauseLengths

Durairaj, V. (2006)

Automatic program analysis using Max-SMT

Larraz, D. (2015) · doi:10.5821/dissertation-2117-95760

Automated compositional analysis for checking component substitutability

Clarke, E. M., & Sinha, N. (2007)

Efficient approaches for functional validation of soc designs using high-level specifications

Mishra, P., & Chen, M. (2010) · University of Florida Digital Collections (University of Florida)

Search State Extensibility based Learning Framework for Model Checking and Test Generation

Chandrasekar, M. (2010) · VTechWorks (Virginia Tech)

Complexity and structural heuristics for propositional and quantified satisfiability

Vardi, M. Y., & Pan, G. (2007) · Rice Research Repository (Rice University)

Generation of Minimum-Consistent DFA Using SAT Solver

Inui, N., & Aizawa, A. (2012) · Transactions of the Japanese Society for Artificial Intelligence · doi:10.1527/tjsai.27.151

Embedded System Design Course simulation platform Based on Proteus and Keil

Dan, L., Yanrong, Z., Yu, Z., Zhang, L., & Erhu, H. (2014) · Advanced science and technology letters · doi:10.14257/astl.2014.77.12

Root-Cause Analysis for Memory-Locked Errors

Adler, J., Maksimovic, D., & Veneris, A. G. (2016) · Design, Automation, and Test in Europe · doi:10.3850/9783981537079_0465

Single-Solver Algorithms for 2QBF (Poster Presentation)

Bayless, S., & Hu, A. J. (2012) · Theory and Applications of Satisfiability Testing

Basic Technology for Formal Verification

Fujita, M., Ghosh, I., & Prasad, M. R. (2008) · Elsevier eBooks · doi:10.1016/b978-012370616-4.50004-5

Verification of large industrial circuits using sat based reparameterization and automated abstraction-refinement

Clarke, E. M., & Chauhan, P. (2007)

Extending SAT solver with parity constraints

Laitinen, T. (2010) · Aaltodoc (Aalto University)

JumpSAT Based System Verification Scenarios

Pułka, A. (2018) · International Conference on Signals and Electronic Systems · doi:10.1109/icses.2018.8507290

Symbolic Simulation via SAT Solver with Variable Partition

Yang, X., & He, A. (2011) · Energy Procedia · doi:10.1016/j.egypro.2011.12.354

Design Automation Methods for Conventional Systems

Zulehner, A., & Wille, R. (2020) · Springer eBooks · doi:10.1007/978-3-030-41753-6_3

Interval-based Counterexample Analysis for Error Explanation

Toda, T., & Inoue, T. (2021) · Journal of Information Processing · doi:10.2197/ipsjjip.29.630

References

Fisher, M. (2011) · Wiley eBooks · doi:10.1002/9781119991472.refs

Preliminaries

Wille, R., & Drechsler, R. (2010) · Springer eBooks · doi:10.1007/978-90-481-9579-4_2

Propositional Logic

Almeida, J. B., Frade, M. J., Pinto, J. S., & de Sousa, S. M. (2011) · Undergraduate topics in computer science · doi:10.1007/978-0-85729-018-2_3

Introduction

Chen, M., Qin, X., Koo, H.-M., & Mishra, P. (2012) · Springer eBooks · doi:10.1007/978-1-4614-1359-2_1

Analyzing Multiple Conflicts in SAT: An Experimental Evaluation

Oliveras, A., Rodríguez-Carbonell, E., & Zhao, R. (2023) · EPiC series in computing · doi:10.29007/fj74

Learning-Based Testing Using SAL (Symbolic Analysis Laboratory) Model Checker

Shah, A. A., & Sindhu, M. A. (2023) · NUML International Journal of Engineering and Computing · doi:10.52015/nijec.v2i1.32

On Solving MAX-SAT Using Sum of Squares

Sinjorgo, L., & Sotirov, R. (2023) · INFORMS journal on computing · doi:10.1287/ijoc.2023.0036

Entwurfsautomatisierungsmethoden für konventionelle Systeme

Zulehner, A., & Wille, R. (2023) · Springer eBooks · doi:10.1007/978-3-031-36751-9_3

OpenMP Program Verification Based on Bounded Model Checking

Sun, L., Lu, B., Yin, L., 阿部, 哲., & Jin, W. (2023) · IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C) · doi:10.1109/qrs-c60940.2023.00107

An improved method for a set-pair routing problem by SAT

Nagakura, K., & Fujiyoshi, K. (2024) · IEEE Asia Pacific Conference on Circuits and Systems (APCCAS) · doi:10.1109/apccas62602.2024.10808676

Theoretical analysis of practical heuristics for satisfiability

Skvortsov, E. (2009) · Summit (Simon Fraser University)

LLM-Driven Automated Generation of Formal Specifications for C Programs

He, L., Zhang, Y., Guo, W., Yao, R., Yang, X., & Sun, H. (2025) · International Conference on Blockchain Technology and Information Security (ICBCTIS) · doi:10.1109/icbctis66509.2025.11387183

Improving SAT and pseudo-boolean solving technology

Zhao, R. (2026) · doi:10.5821/dissertation-2117-456957

Vulnerability management for safe configurations in autonomic networks and systems

Barrère, M. (2014) · doi:10.70675/bc64e831z082ez45e9z81dazf5db6bf6719d

Etude des Mécanismes de Transformation de Modèles CSP/SAT

Gaete, C. A. V. (2020) · doi:10.70675/a52c999az4bc6z429eza297z0a41883df006

Development of a Formal Verification Methodology for B Specifications using PERF formal toolkit. Application to safety requirements of railway systems.

Halchin, A. (2021) · theses.fr (ABES) · doi:10.70675/265f2784zde83z4c73za062ze8d03780113c

Contributions to SAT Solving

Saouli, S. (2024) · doi:10.70675/e9194529z1a88z456cz8da5z000c1ce8594d

Taxonomy of AI Methods

Schmid, T., Hildesheim, W., & Holoyad, T. (2026) · Springer eBooks · doi:10.1007/978-3-032-00533-5_7

Bounded model checking for asynchronous concurrent systems

Rakotoarisoa, M. J. (2014) · doi:10.5821/dissertation-2117-95294

Verification Algorithms for FSM Models

Fujita, M., Ghosh, I., & Prasad, M. R. (2008) · Elsevier eBooks · doi:10.1016/b978-012370616-4.50005-7

Synchronized Generation of Directed Tests

Chen, M., Qin, X., Koo, H.-M., & Mishra, P. (2012) · Springer eBooks · doi:10.1007/978-1-4614-1359-2_7

SAT-based Verification -- From Core Algorithms to Novel Application Domains

Herbstritt, M. (2008) · FreiDok plus (Universitätsbibliothek Freiburg)

A comprehensive study and analysis on SAT-solvers: advances, usages and achievements

Alouneh, S., Abed, S., Alshayeji, M. H., & Mesleh, R. (2018) · Artificial Intelligence Review · doi:10.1007/s10462-018-9628-0 · Cited by 28

Tuning SAT for Formal Verification and Testing.

Velev, M. N. (2004) · Zenodo (CERN European Organization for Nuclear Research) · doi:10.3217/jucs-010-12 · Cited by 1

SAT-Based Verification Methods and Applications in Hardware Verification

Gupta, A., Ganai, M., & Wang, C. (2006) · Lecture notes in computer science · doi:10.1007/11757283_5 · Cited by 40

Editor’s Introduction to the Special Volume on Application of Constraints to Formal Verification

Velev, M. N. (2008) · Journal on Satisfiability Boolean Modeling and Computation · doi:10.3233/sat190049