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

Symbolic Model Checking without BDDs

Biere, A., Cimatti, A., Clarke, E. M., & Zhu, Y. (1999) · Lecture notes in computer science · doi:10.1007/3-540-49059-0_14 · Cited by 2,192

Design and validation of computer protocols

Holzmann, G. J. (1991) · Cited by 1,693

GRASP: a search algorithm for propositional satisfiability

Marques-Silva, J. P., & Sakallah, K. A. (1999) · IEEE Transactions on Computers · doi:10.1109/12.769433 · Cited by 1,378

Relationships between nondeterministic and deterministic tape complexities

Savitch, W. J. (1970) · Journal of Computer and System Sciences · doi:10.1016/s0022-0000(70)80006-x · Cited by 1,357

On the Complexity of Derivation in Propositional Calculus

Tseitin, G. S. (1983) · Springer eBooks · doi:10.1007/978-3-642-81955-1_28 · Cited by 1,211

A new method for solving hard satisfiability problems

Selman, B., Levesque, H. J., & Mitchell, D. G. M. (1992) · Cited by 1,179

An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits

Goel, . (1981) · IEEE Transactions on Computers · doi:10.1109/tc.1981.1675757 · Cited by 1,084

DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

Clarke, E. M., & Emerson, E. A. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-69850-0_12 · Cited by 1,080

Symbolic model checking: an approach to the state explosion problem

McMillan, K. L. (1992) · Defense Technical Information Center (DTIC) · Cited by 979

The S LAM project

Ball, T., & Rajamani, S. K. (2002) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/503272.503274 · Cited by 923

Interpolation and SAT-Based Model Checking

McMillan, K. L. (2003) · Lecture notes in computer science · doi:10.1007/978-3-540-45069-6_1 · Cited by 918

Word problems requiring exponential time(Preliminary Report)

Stockmeyer, L. J., & Meyer, A. R. (1973) · ACM Symposium on Theory of Computing (STOC) · doi:10.1145/800125.804029 · Cited by 874

On the Acceleration of Test Generation Algorithms

Fujiwara, & Shimono (1983) · IEEE Transactions on Computers · doi:10.1109/tc.1983.1676174 · Cited by 801

Computer-aided verification of coordinating processes: The automata-theoretic approach

(1995) · Computers & Mathematics with Applications · doi:10.1016/0898-1221(95)90267-8 · Cited by 786

Noise strategies for improving local search

Selman, B., Kautz, H., & Cohen, B. (1994) · Cited by 757

Symbolic model checking using SAT procedures instead of BDDs

Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., & Zhu, Y. (1999) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/309847.309942 · Cited by 752

Checking Safety Properties Using Induction and a SAT-Solver

Sheeran, M., Singh, S., & Stålmarck, G. (2000) · Lecture notes in computer science · doi:10.1007/3-540-40922-x_8 · Cited by 719

Bounded Model Checking Using Satisfiability Solving

Clarke, E. M., Biere, A., Raimi, R., & Zhu, Y. (2001) · Formal Methods in System Design · doi:10.1023/a:1011276507260 · Cited by 712

Test pattern generation using Boolean satisfiability

Larrabee, T. (1992) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/43.108614 · Cited by 690

Efficient Conflict Driven Learning in a Boolean Satisfiability Solver

Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001) · Cited by 682

Using CSP look-back techniques to solve real-world SAT instances

Bayardo, R. J., & Schrag, R. C. (1997) · Cited by 592

A Structure-preserving Clause Form Translation

Plaisted, D. A., & Greenbaum, S. (1986) · Journal of Symbolic Computation · doi:10.1016/s0747-7171(86)80028-1 · Cited by 582

Symbolic model checking for sequential circuit verification

Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. L., & Dill, D. L. (1994) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/43.275352 · Cited by 547

SATO: An efficient propositional prover

Zhang, H. (1997) · Lecture notes in computer science · doi:10.1007/3-540-63104-6_28 · Cited by 515

Timed Automata

Rajeev Alur, A. (1999) · Cited by 452

Computer-Aided Verification of Coordinating Processes

Kurshan, R. P. (1995) · Princeton University Press eBooks · doi:10.1515/9781400864041 · Cited by 440

Model Checking

Clarke, E. M., & Schlingloff, B. (2001) · Elsevier eBooks · doi:10.1016/b978-044450813-3/50026-6 · Cited by 391

Temporal Induction by Incremental SAT Solving

Eén, N., & Sörensson, N. (2003) · Electronic Notes in Theoretical Computer Science · doi:10.1016/s1571-0661(05)82542-3 · Cited by 376

BerkMin: A fast and robust SAT-solver

Goldberg, E. I., & Novikov, Y. (2003) · Design, Automation, and Test in Europe · doi:10.1109/date.2002.998262 · Cited by 363

Applying SAT Methods in Unbounded Symbolic Model Checking

McMillan, K. L. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_19 · Cited by 359

Robust Boolean reasoning for equivalence checking and functional property verification

Kuehlmann, A., Paruthi, V., Krohm, F., & Ganai, M. (2002) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2002.804386 · Cited by 333

Resolution for Quantified Boolean Formulas

Büning, H. K., Karpiński, M., & Flögel, A. (1995) · Information and Computation · doi:10.1006/inco.1995.1025 · Cited by 321

The Quest for Efficient Boolean Satisfiability Solvers

Zhang, L., & Malik, S. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_2 · Cited by 287

Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications

Zhang, L., & Malik, S. (2003) · doi:10.5555/789083.1022835 · Cited by 278

Resolve and Expand

Biere, A. (2005) · Lecture notes in computer science · doi:10.1007/11527695_5 · Cited by 251

Timed Automata

Rajeev Alur, A. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48683-6_3 · Cited by 235

Automatic Abstraction without Counterexamples

McMillan, K. L., & Amla, N. (2003) · Lecture notes in computer science · doi:10.1007/3-540-36577-x_2 · Cited by 232

Finding bugs with a constraint solver

Jackson, D. N., & Vaziri, M. (2000) · ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) · doi:10.1145/347324.383378 · Cited by 209

An Efficient Propositional Prover

Zhang, H. (1997) · Cited by 196

Propositional Logic: Deduction and Algorithms

Büning, H. K., & Letterman, T. (1999) · Cambridge University Press eBooks · Cited by 193

Benefits of Bounded Model Checking at an Industrial Setting

Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., & Vardi, M. Y. (2001) · Lecture notes in computer science · doi:10.1007/3-540-44585-4_43 · Cited by 189

SATIRE

Whittemore, J., Kim, J., & Sakallah, K. A. (2001) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac.2001.935567 · Cited by 188

Symbolic Reachability Analysis Based on SAT-Solvers

Abdulla, P. A., Bjesse, P., & Eén, N. (2000) · Lecture notes in computer science · doi:10.1007/3-540-46419-0_28 · Cited by 187

Tuning SAT Checkers for Bounded Model Checking

Shtrichman, O. (2000) · Lecture notes in computer science · doi:10.1007/10722167_36 · Cited by 167

The Impact of Branching Heuristics in Propositional Satisfiability Algorithms

Marques-Silva, J. P. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48159-1_5 · Cited by 163

SAT-Based Verification without State Space Traversal

Bjesse, P., & Claessen, K. (2000) · Lecture notes in computer science · doi:10.1007/3-540-40922-x_23 · Cited by 162

Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas

Letz, R. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45616-3_12 · Cited by 154

Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis

Chauhan, P., Clarke, E. M., Kukula, J. H., Sapra, S., Veith, H., & Wang, D. (2002) · Lecture notes in computer science · doi:10.1007/3-540-36126-x_3 · Cited by 153

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT

Barrett, C., Dill, D. L., & Stump, A. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_18 · Cited by 150

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques

Clarke, E. M., Gupta, A., Kukula, J. H., & Strichman, O. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_20 · Cited by 148

Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors

Velev, M. N., & Bryant, R. E. (2003) · Journal of Symbolic Computation · doi:10.1016/s0747-7171(02)00091-3 · Cited by 148

Verification of Proofs of Unsatisfiability for CNF Formulas

Goldberg, E. I., & Novikov, Y. (2003) · Cited by 143

Pruning Techniques for the SAT-Based Bounded Model Checking Problem

Shtrichman, O. (2001) · Lecture notes in computer science · doi:10.1007/3-540-44798-9_4 · Cited by 142

Using SAT for combinational equivalence checking

Goldberg, E. I., Prasad, M. R., & Brayton, R. K. (2001) · doi:10.5555/367072.367111 · Cited by 137

Verifying Safety Properties of a PowerPC− Microprocessor Using Symbolic Model Checking without BDDs

Biere, A., Clarke, E. M., Raimi, R., & Zhu, Y. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48683-6_8 · Cited by 130

An algorithm to evaluate quantified Boolean formulae

Cadoli, M., Giovanardi, A., & Schaerf, M. (1998) · Cited by 130

A Tutorial on Stålmarck's Proof Procedure for Propositional Logic

Sheeran, M., & Stålmarck, G. (2000) · Formal Methods in System Design · doi:10.1023/a:1008725524946 · Cited by 128

Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation

Zhang, L., & Malik, S. (2002) · Lecture notes in computer science · doi:10.1007/3-540-46135-3_14 · Cited by 121

Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers

Bjesse, P., Leonard, T., & Mokkedem, A. (2001) · Lecture notes in computer science · doi:10.1007/3-540-44585-4_44 · Cited by 114

Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver

Ganai, M., Ashar, P. N., Gupta, A., Zhang, L., & Malik, S. (2002) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/513918.514105 · Cited by 113

A Circuit SAT Solver With Signal Correlation Guided Learning

Lu, F., Wang, L.-C., Cheng, K.-T. T., & Huang, R. C.-Y. (2003) · doi:10.5555/789083.1022837 · Cited by 111

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

Williams, P. F., Biere, A., Clarke, E. M., & Gupta, A. (2000) · Lecture notes in computer science · doi:10.1007/10722167_13 · Cited by 107

Using SAT for combinational equivalence checking

Goldberg, E. I., Prasad, M. R., & Brayton, R. K. (2002) · Design, Automation, and Test in Europe · doi:10.1109/date.2001.915010 · Cited by 94

Verification of proofs of unsatisfiability for CNF formulas

Goldberg, E. I., & Novikov, Y. (2003) · Design, Automation, and Test in Europe · doi:10.1109/date.2003.1253718 · Cited by 89

A hybrid SAT-based decision procedure for separation logic with uninterpreted functions

Seshia, S. A., Lahiri, S. K., & Bryant, R. E. (2003) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/775832.775945 · Cited by 87

Efficient SAT-based unbounded symbolic model checking using circuit cofactoring

Ganai, M., Gupta, A., & Ashar, P. N. (2005) · doi:10.1109/iccad.2004.1382631 · Cited by 83

SAT-Based Image Computation with Application in Reachability Analysis

Gupta, A., Yang, Z., Ashar, P. N., & Gupta, A. (2000) · Lecture notes in computer science · doi:10.1007/3-540-40922-x_22 · Cited by 82

Sequential equivalence checking without state space traversal

van Eijk, C. A. J. (1998) · doi:10.5555/368058.368314 · Cited by 79

Iterative abstraction using SAT-based BMC with proof analysis

Gupta, A., Ganai, M., Yang, Z., & Ashar, P. N. (2004) · International Conference on Computer Aided Design · doi:10.1109/iccad.2003.1257811 · Cited by 78

Book Review: Design and Validation of Computer Protocols by Gerard J. Holzmann (Prentice Hall, 1991)

Fredlund, L. (1991) · ACM SIGCOMM Computer Communication Review · doi:10.1145/122419.1024051 · Cited by 69

Efficient reduction of finite state model checking to reachability analysis

Schuppan, V., & Biere, A. (2004) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-003-0121-x · Cited by 67

Boolean Expression Diagrams

Andersen, H. R., & Hulgaard, H. (2002) · Information and Computation · doi:10.1006/inco.2001.2948 · Cited by 66

Qubos: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers

Ayari, A., & Basin, D. (2002) · Lecture notes in computer science · doi:10.1007/3-540-36126-x_12 · Cited by 58

Learning for quantified boolean logic satisfiability

Giunchiglia, E., Narizzano, M., & Tacchella, A. (2002) · CINECA IRIS Institutial Research Information System (University of Genoa) · doi:10.5555/777092.777192 · Cited by 57

Learning from BDDs in SAT-based bounded model checking

Gupta, A., Ganai, M., Wang, C., Yang, Z., & Ashar, P. N. (2003) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac.2003.1219133 · Cited by 55

On Solving Presburger and Linear Arithmetic with SAT

Strichman, O. (2002) · Lecture notes in computer science · doi:10.1007/3-540-36126-x_10 · Cited by 54

CTL model checking based on forward state traversal

Iwashita, H., Nakata, T., & Hirose, F. (1996) · doi:10.5555/244522.244536 · Cited by 54

Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae

Rintanen, J. (2001) · Lecture notes in computer science · doi:10.1007/3-540-45653-8_25 · Cited by 52

Partition-Based Decision Heuristics for Image Computation using SAT and BDDs

Gupta, A., Yang, Z., Ashar, P. N., Zhang, L., & Malik, S. (2001) · Cited by 52

Property Checking via Structural Analysis

Baumgartner, J., Kuehlmann, A., & Abraham, J. A. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_12 · Cited by 51

Experimental Analysis of Different Techniques for Bounded Model Checking

Amla, N., Kurshan, R. P., McMillan, K. L., & Medel, R. (2003) · Lecture notes in computer science · doi:10.1007/3-540-36577-x_4 · Cited by 49

A Signal Correlation Guided ATPG solver and its applications for solving difficult industrial cases

Lu, F., Wang, L.-C., Cheng, K.-T. T., Moondanos, J., & Hanna, Z. (2003) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac.2003.1219041 · Cited by 49

A satisfiability procedure for quantified Boolean formulae

Plaisted, D. A., Biere, A., & Zhu, Y. (2003) · Discrete Applied Mathematics · doi:10.1016/s0166-218x(02)00409-2 · Cited by 48

Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals

Cabodi, G., Nocco, S., & Quer, S. (2003) · Design, Automation, and Test in Europe · doi:10.5555/789083.1022838 · Cited by 48

Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver

Ganai, M., Zhang, L., Ashar, P. N., Gupta, A., & Malik, S. (2002) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac.2002.1012722 · Cited by 47

Sequential equivalence checking without state space traversal

van Eijk, C. A. J. (2002) · Design, Automation, and Test in Europe · doi:10.1109/date.1998.655922 · Cited by 46

Model Checking Based on Sequential ATPG

Boppana, V., Rajan, S. P., Takayama, K., & Fujita, M. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48683-6_36 · Cited by 45

Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking

Huan, C.-Y., & Cheng, K.-T. T. (2001) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/43.913756 · Cited by 44

SATORI-a fast sequential SAT engine for circuits

Iyer, M. K., Parthasarathy, G., & Cheng, K.-T. T. (2003) · International Conference on Computer Aided Design · doi:10.1109/iccad.2003.159706 · Cited by 44

From pre-historic to post-modern symbolic model checking

Henzinger, T. A., Kupferman, O., & Qadeer, S. (1998) · Lecture notes in computer science · doi:10.1007/bfb0028745 · Cited by 43

Improving ariadne’s bundle by following multiple threads in abstraction refinement

Wang, C., Li, B., Jin, H., Hachtel, G. D., & Somenzi, F. (2003) · Cited by 42

Dynamic detection and removal of inactive clauses in SAT with application in image computation

Gupta, A., Gupta, A., Yang, Z., & Ashar, P. N. (2001) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/378239.379018 · Cited by 42

Record and play: a structural fixed point iteration for sequential circuit verification

Stoffel, & Kunz (1997) · International Conference on Computer Aided Design · doi:10.1109/iccad.1997.643566 · Cited by 42

Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers

Berre, D. L., Simon, L., & Tacchella, A. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-24605-3_35 · Cited by 40

Improving SAT-based bounded model checking by means of BDD-based approximate traversals

Cabodi, G., Nocco, S., & Quer, S. (2003) · Design, Automation, and Test in Europe · doi:10.1109/date.2003.1253720 · Cited by 38

Forward model checking techniques oriented to buggy designs

Iwashita, H., & Nakata, T. (1997) · doi:10.5555/266388.266515 · Cited by 35

Abstraction and BDDs Complement SAT-Based BMC in DiVer

Gupta, A., Ganai, M., Wang, C., Yang, Z., & Ashar, P. N. (2003) · Lecture notes in computer science · doi:10.1007/978-3-540-45069-6_20 · Cited by 33

Bounded Model Construction for Monadic Second-Order Logics

Ayari, A., & Basin, D. (2000) · Lecture notes in computer science · doi:10.1007/10722167_11 · Cited by 32

Tuning the VSIDS decision heuristic for bounded model checking

Shacham, O., & Zarpas, E. (2004) · International Workshop on Microprocessor Test and Verification (MTV) · doi:10.1109/mtv.2003.1250266 · Cited by 32

Forward model checking techniques oriented to buggy designs

Iwashita, & Nakata (1997) · International Conference on Computer Aided Design · doi:10.1109/iccad.1997.643567 · Cited by 32

Verifying properties using sequential ATPG [IC design]

Abraham, J. A., & Vedula, V. M. (2003) · IEEE International Test Conference (ITC) · doi:10.1109/test.2002.1041761 · Cited by 30

SAT-based sequential depth computation

Mneimneh, M. N., & Sakallah, K. A. (2003) · Asia and South Pacific Design Automation Conference (ASP-DAC) · doi:10.1109/aspdac.2003.1194998 · Cited by 30

Partition-based decision heuristics for image computation using SAT and BDDs

Gupta, A., Yang, Z., Ashar, P., Zhang, L., & Malik, S. (2002) · International Conference on Computer Aided Design · doi:10.1109/iccad.2001.968635 · Cited by 30

Improved SAT-based bounded reachability analysis

Ganai, M., & Aziz, A. (2003) · Asia and South Pacific Design Automation Conference (ASP-DAC) · doi:10.1109/aspdac.2002.995020 · Cited by 28

CTL model checking based on forward state traversal

Iwashita, H., Nakata, T., & Hirose, F. (2002) · International Conference on Computer Aided Design · doi:10.1109/iccad.1996.569084 · Cited by 26

Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking

Biere, A., Zhu, Y., & Clarke, E. M. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48092-7_8 · Cited by 21

An analysis of ATPG and SAT algorithms for formal verification

Parthasarathy, G., Huang, C.-Y. R., & Cheng, K.-T. T. (2002) · Proceedings · doi:10.1109/hldvt.2001.972826 · Cited by 21

A Satisfiability-Based Approach to Abstraction Refinement in Model Checking

Li, B., Wang, C., & Somenzi, F. (2003) · Electronic Notes in Theoretical Computer Science · doi:10.1016/s1571-0661(05)82546-0 · Cited by 20

Effective safety property checking using simulation-based sequential ATPG

Sheng, S., Takayama, K., & Hsiao, M. S. (2002) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/513918.514120 · Cited by 14

On solving stack-based incremental satisfiability problems

Kim, J., Whittemore, J., & Sakallah, K. A. (2002) · IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD) · doi:10.1109/iccd.2000.878311 · Cited by 11

A hybrid SAT-based decision procedure for separation logic with uninterpreted functions

Seshia, S. A., Lahiri, S. K., & Bryant, R. E. (2004) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac.2003.1219039 · Cited by 11

Binary time-frame expansion

Fallah, F. (2002) · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · doi:10.1145/774572.774639 · Cited by 10

A Practical Approach to Cycle Bound Estimation for Property Checking.

Yen, C.-C., Chen, K.-C., & Jou, J.-Y. (2002) · Cited by 6

Quantum algorithms: an overview

Montanaro, A. (2016) · npj Quantum Information · doi:10.1038/npjqi.2015.23 · Cited by 1,071

Predicting learnt clauses quality in modern SAT solvers

Audemard, G., & Simon, L. (2009) · Cited by 498

Algorithm runtime prediction: Methods & evaluation

Hutter, F., Xu, L., Hoos, H. H., & Leyton‐Brown, K. (2013) · Artificial Intelligence · doi:10.1016/j.artint.2013.10.003 · Cited by 424

Combinatorial Optimization and Reasoning with Graph Neural Networks

Cappart, Q., Chételat, D., Khalil, E. B., Lodi, A., Morris, C., & Veličković, P. (2021) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2021/595 · Cited by 306

Linear Encodings of Bounded LTL Model Checking

Biere, A., Heljanko, K., Junttila, T. A., Latvala, T., & Schuppan, V. (2006) · Logical Methods in Computer Science · doi:10.2168/lmcs-2(5:5)2006 · Cited by 224

ASlib: A benchmark library for algorithm selection

Bischl, B., Kerschke, P., Kotthoff, L., Lindauer, M., Malitsky, Y., Fréchette, A., Hoos, H. H., Hutter, F., Leyton‐Brown, K., Tierney, K., et al. (2016) · Artificial Intelligence · doi:10.1016/j.artint.2016.04.003 · Cited by 215

Automated Algorithm Configuration and Parameter Tuning

Hoos, H. H. (2011) · Springer eBooks · doi:10.1007/978-3-642-21434-9_3 · Cited by 215

Challenges and opportunities in quantum optimization

Abbas, A., Ambainis, A., Augustino, B., Bärtschi, A., Buhrman, H., Coffrin, C., Cortiana, G., Dunjko, V., Egger, D. J., Elmegreen, B. G., et al. (2024) · Nature Reviews Physics · doi:10.1038/s42254-024-00770-9 · Cited by 201

Exact Multiple-Control Toffoli Network Synthesis With SAT Techniques

Grosse, D. J., Wille, R., Dueck, G. W., & Drechsler, R. (2009) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2009.2017215 · Cited by 178

Boolean Satisfiability Solvers and Their Applications in Model Checking

Vizel, Y., Weißenbacher, G., & Malik, S. (2015) · Proceedings of the IEEE · doi:10.1109/jproc.2015.2455034 · Cited by 120

Formal verification approaches and standards in the cloud computing: A comprehensive and systematic review

Souri, A., Navimipour, N. J., & Rahmani, A. M. (2017) · Computer Standards & Interfaces · doi:10.1016/j.csi.2017.11.007 · Cited by 110

Propositional Satisfiability and Constraint Programming

Bordeaux, L., Hamadi, Y., & Zhang, L. (2006) · ACM Computing Surveys · doi:10.1145/1177352.1177354 · Cited by 107

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment

Amla, N., Du, X., Kuehlmann, A., Kurshan, R. P., & McMillan, K. L. (2005) · Lecture notes in computer science · doi:10.1007/11560548_20 · Cited by 104

Efficient SAT-based bounded model checking for software verification

Ivančić, F., Yang, Z., Ganai, M., Gupta, A., & Ashar, P. N. (2008) · Theoretical Computer Science · doi:10.1016/j.tcs.2008.03.013 · Cited by 98

Boosting Verification by Automatic Tuning of Decision Procedures

Hutter, F., Babić, D., Hoos, H. H., & Hu, A. J. (2007) · doi:10.1109/fmcad.2007.13 · Cited by 95

Fixed-Parameter Algorithms For Artificial Intelligence, Constraint Satisfaction and Database Problems

Gottlob, G., & Szeider, S. (2007) · The Computer Journal · doi:10.1093/comjnl/bxm056 · Cited by 93

Logical Formalizations of Commonsense Reasoning: A Survey

Davis, E. (2017) · Journal of Artificial Intelligence Research · doi:10.1613/jair.5339 · Cited by 97

Model checking C programs using F-Soft

Ivančić, F., Shlyakhter, I. A., Gupta, A., Ganai, M., Kahlon, V., Wang, C., & Yang, Z. (2006) · IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD) · doi:10.1109/iccd.2005.77 · Cited by 90

Boosting Verification by Automatic Tuning of Decision Procedures

Hutter, F., Babić, D., Hoos, H. H., & Hu, A. J. (2007) · Formal Methods in Computer-Aided Design · doi:10.1109/famcad.2007.9 · Cited by 79

Backdoors to Satisfaction

Gaspers, S., & Szeider, S. (2012) · Lecture notes in computer science · doi:10.1007/978-3-642-30891-8_15 · Cited by 76

Applying quantum algorithms to constraint satisfaction problems

Campbell, E. T., Khurana, A., & Montanaro, A. (2019) · Quantum · doi:10.22331/q-2019-07-18-167 · Cited by 89

The Configurable SAT Solver Challenge (CSSC)

Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H. H., & Leyton‐Brown, K. (2016) · Artificial Intelligence · doi:10.1016/j.artint.2016.09.006 · Cited by 69

Accelerating high-level bounded model checking

Ganai, M., & Gupta, A. (2006) · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · doi:10.1145/1233501.1233664 · Cited by 65

Quantum Optimization: Potential, Challenges, and the Path Forward

Abbas, A., (NNSA), U. N. N. S. A., Ambainis, A., Augustino, B., Bärtschi, A., Buhrman, H., Coffrin, C., Cortiana, G., Dunjko, V., Egger, D., et al. (2023) · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · doi:10.2172/2229681 · Cited by 65

Bit-Exact ECC Recovery (BEER): Determining DRAM On-Die ECC Functions by Exploiting DRAM Data Retention Characteristics

Patel, M., Kim, J. S., Shahroodi, T., Hassan, H., & Mutlu, O. (2020) · IEEE/ACM International Symposium on Microarchitecture (MICRO) · doi:10.1109/micro50266.2020.00034 · Cited by 58

A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges

Li, Y., Yin, X., Wang, Z., Yao, J., Shi, X., Wu, J., Zhang, H., & Wang, Q. (2018) · IEEE Communications Surveys & Tutorials · doi:10.1109/comst.2018.2868050 · Cited by 54

A Restriction of Extended Resolution for Clause Learning SAT Solvers

Audemard, G., Katsirelos, G., & Simon, L. (2010) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v24i1.7553 · Cited by 53

Functional Test Generation Using Efficient Property Clustering and Learning Techniques

Chen, M., & Mishra, P. (2010) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2010.2041846 · Cited by 53

1 Applying Formal Methods to Networking: Theory, Techniques and ApplicationsPreprint

Qadir, J., & Hasan, O. (2016) · Cited by 51

Understanding the empirical hardness of NP-complete problems

Leyton-Brown, K., Hoos, H., Hutter, F., & Xu, L. (2014) · CACM · doi:10.1145/2594413.2594424 · Cited by 54

Applying Formal Methods to Networking: Theory, Techniques, and Applications

Qadir, J., & Hasan, O. (2014) · IEEE Communications Surveys & Tutorials · doi:10.1109/comst.2014.2345792 · Cited by 48

Temporal Representation and Reasoning.

Fisher, M. (2008) · Cited by 45

Relational Hidden Variables and Non-Locality

Abramsky, S. (2013) · Studia Logica · doi:10.1007/s11225-013-9477-4 · Cited by 43

Using Boolean satisfiability for computing soft error rates in early design stages

Shazli, S. Z., & Tahoori, M. B. (2009) · Microelectronics Reliability · doi:10.1016/j.microrel.2009.08.006 · Cited by 42

The AI Methods, Capabilities and Criticality Grid

Schmid, T., Hildesheim, W., Holoyad, T., & Schumacher, K. (2021) · Künstliche Intell. · doi:10.1007/s13218-021-00736-4 · Cited by 46

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation

Grümberg, O., Heyman, T., Ifergan, N., & Schuster, A. (2005) · Lecture notes in computer science · doi:10.1007/11560548_12 · Cited by 41

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

Protecting analog circuits with parameter biasing obfuscation

Rao, V. V., & Savidis, I. (2017) · IEEE Latin American Test Symposium (LATS) · doi:10.1109/latw.2017.7906739 · Cited by 40

Finding Efficient Circuits Using SAT-Solvers

Kojevnikov, A., Kulikov, A. S., & Yaroslavtsev, G. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-02777-2_5 · Cited by 39

SAT-Based Model Checking

Biere, A., & Kroening, D. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_10 · Cited by 39

Building a Knowledge Base System for an Integration of Logic Programming and Classical Logic

Denecker, M., & Vennekens, J. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-89982-2_12 · Cited by 38

A Formula-based Approach for Automatic Fault Localization of Multi-fault Programs

Lamraoui, S.-M., & Nakajima, S. (2016) · Journal of Information Processing · doi:10.2197/ipsjjip.24.88 · Cited by 38

Continuous Search in Constraint Programming

Arbeláez, A., Hamadi, Y., & Sébag, M. (2010) · IEEE International Conference on Tools with Artificial Intelligence (ICTAI) · doi:10.1109/ictai.2010.17 · Cited by 37

Functional test generation using design and property decomposition techniques

Koo, H.-M., & Mishra, P. (2009) · ACM Transactions on Embedded Computing Systems · doi:10.1145/1550987.1550995 · Cited by 35

SAT-solving in practice

Claessen, K., Eén, N., Sheeran, M., & Sörensson, N. (2008) · International Workshop on Discrete Event Systems · doi:10.1109/wodes.2008.4605923 · Cited by 33

Test generation using SAT-based bounded model checking for validation of pipelined processors

Koo, H.-M., & Mishra, P. (2006) · ACM Great Lakes Symposium on VLSI (GLSVLSI) · doi:10.1145/1127908.1127991 · Cited by 33

Towards a notion of unsatisfiable and unrealizable cores for LTL

Schuppan, V. (2010) · Science of Computer Programming · doi:10.1016/j.scico.2010.11.004 · Cited by 33

Complexity of Fixed-Size Bit-Vector Logics

Kovásznai, G., Fröhlich, A., & Biere, A. (2015) · Theory of Computing Systems · doi:10.1007/s00224-015-9653-1 · Cited by 33

Soundness of Q-resolution with dependency schemes

Slivovsky, F., & Szeider, S. (2015) · Theoretical Computer Science · doi:10.1016/j.tcs.2015.10.020 · Cited by 32

On Approaches to Explaining Infeasibility of Sets of Boolean Clauses

Grégoire, É., Mazure, B., & Piette, C. (2008) · IEEE International Conference on Tools with Artificial Intelligence (ICTAI) · doi:10.1109/ictai.2008.39 · Cited by 31

SAT-Solving in Practice, with a Tutorial Example from Supervisory Control

Claessen, K., Eén, N., Sheeran, M., Sörensson, N., Voronov, A., & Åkesson, K. (2009) · Discrete Event Dynamic Systems · doi:10.1007/s10626-009-0081-8 · Cited by 30

Deep Learning for Autonomous Vehicle Control: Algorithms, State-of-the-Art, and Future Prospects

Kuutti, S., Fallah, S., Bowden, R., & Barber, P. (2019) · Synthesis lectures on advances in automotive technology · doi:10.2200/s00932ed1v01y201906aat008 · Cited by 29

A Clause-Based Heuristic for SAT Solvers

Dershowitz, N., Hanna, Z., & Nadel, A. (2005) · Lecture notes in computer science · doi:10.1007/11499107_4 · Cited by 29

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

First steps towards SAT-based formal analog verification

Tiwary, S. K., Gupta, A., Phillips, J. R., Pinello, C., & Zlatanovici, R. (2009) · doi:10.1145/1687399.1687401 · Cited by 28

Efficient test case generation for validation of UML activity diagrams

Chen, M., Mishra, P., & Kalita, D. (2010) · Design Automation for Embedded Systems · doi:10.1007/s10617-010-9052-4 · Cited by 26

Survey on automated symbolic verification and its application for synthesising cyber‐physical systems

Cordeiro, L. C., Filho, E. B. L., & de Bessa, I. V. (2019) · IET Cyber-Physical Systems Theory & Applications · doi:10.1049/iet-cps.2018.5006 · Cited by 26

Model Checking: Software and Beyond

Clarke, E. M., & Lerda, F. (2020) · doi:10.3217/jucs-013-05-0639 · Cited by 26

Mesh Based Obfuscation of Analog Circuit Properties

Rao, V. V., & Savidis, I. (2019) · IEEE International Symposium on Circuits and Systems proceedings · doi:10.1109/iscas.2019.8702671 · Cited by 26

Accelerating High-level Bounded Model Checking

Ganai, M., & Gupta, A. (2006) · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · doi:10.1109/iccad.2006.320122 · Cited by 26

Automatic decomposition for sequential equivalence checking of system level and RTL descriptions

Vasudevan, S., Abraham, J. A., Viswanath, V., & Tu, J. (2006) · ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE) · doi:10.1109/memcod.2006.1695903 · Cited by 25

Improving platform-based system synthesis by satisfiability modulo theories solving

Reimann, F., Glaß, M., Haubelt, C. D., Eberl, M., & Teich, J. (2010) · International Conference on Hardware/Software Codesign and System Synthesis · doi:10.1145/1878961.1878986 · Cited by 25

SAT-Based Compositional Verification Using Lazy Learning

Sinha, N., & Clarke, E. M. (2007) · Springer eBooks · doi:10.1007/978-3-540-73368-3_8 · Cited by 25

Automatic Generation of Model Checking Scripts Based on Environment Modeling

Yatake, K., & Aoki, T. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-16164-3_5 · Cited by 23

A systematic literature review on counterexample explanation

Kaleeswaran, A. P., Nordmann, A., Vogel, T., & Grunske, L. (2021) · Information and Software Technology · doi:10.1016/j.infsof.2021.106800 · Cited by 23

Computing high-degree polynomial gradients in memory

Bhattacharya, T., Hutchinson, G. H., Pedretti, G., Sheng, X., Ignowski, J., Vaerenbergh, T. V., Beausoleil, R. G., Strachan, J. P., & Strukov, D. B. (2024) · Nature Communications · doi:10.1038/s41467-024-52488-y · Cited by 27

Symbolic quick error detection using symbolic initial state for pre-silicon verification

Fadiheh, M. R., Urdahl, J., Nuthakki, S. S., Mitra, S., Barrett, C., Stoffel, D., & Kunz, W. (2018) · Design, Automation, and Test in Europe · doi:10.23919/date.2018.8341979 · Cited by 23

Efficient Techniques for Directed Test Generation Using Incremental Satisfiability

Mishra, P., & Chen, M. (2009) · International Conference on VLSI Design · doi:10.1109/vlsi.design.2009.72 · Cited by 22

Towards a Notion of Unsatisfiable Cores for LTL

Schuppan, V. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-11623-0_7 · Cited by 22

Model-Based Testing for Verification Back-Ends

Artho, C. V., Biere, A., & Seidl, M. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-38916-0_3 · Cited by 22

A Formula-Based Approach for Automatic Fault Localization of Imperative Programs

Lamraoui, S.-M., & Nakajima, S. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-11737-9_17 · Cited by 22

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

Navarro-Pérez, J. A., & Воронков, А. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-73595-3_24 · Cited by 22

Answer Set versus Integer Linear Programming for Automatic Synthesis of Multiprocessor Systems from Real‐Time Parallel Programs

Ishebabi, H., Mahr, P., Bobda, C., Gebser, M., & Schaub, T. H. (2009) · International Journal of Reconfigurable Computing · doi:10.1155/2009/863630 · Cited by 21

FPGA acceleration of enhanced boolean constraint propagation for SAT solvers

Thong, J., & Nicolici, N. (2013) · International Conference on Computer Aided Design · doi:10.1109/iccad.2013.6691124 · Cited by 21

Better Decision Heuristics in CDCL through Local Search and Target Phases

Cai, S., Zhang, X., Fleury, M., & Biere, A. (2022) · Journal of Artificial Intelligence Research · doi:10.1613/jair.1.13666 · Cited by 20

Simultaneous SAT-Based Model Checking of Safety Properties

Khasidashvili, Z. O., Nadel, A., Palti, A., & Hanna, Z. (2006) · Lecture notes in computer science · doi:10.1007/11678779_5 · Cited by 20

Merging nodes under sequential observability

Case, M. L., Kravets, V. N., Mishchenko, A., & Brayton, R. K. (2008) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/1391469.1391605 · Cited by 20

Guided Merging of Sequence Diagrams

Widl, M., Biere, A., Brosch, P., Egly, U., Heule, M. J. H., Kappel, G., Seidl, M., & Tompits, H. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-36089-3_10 · Cited by 19

A SAT-based approach to decipher Gene Regulatory Networks

Corblin, F., Hamadi, Y., Fanchon, É., & Trilling, L. (2007) · Cited by 19

Verification Techniques for System-Level Design

Fujita, M., Ghosh, I., & Prasad, M. R. (2008) · Elsevier eBooks · doi:10.1016/b978-0-12-370616-4.x5001-0 · Cited by 18

How to Implement a Theory of Correctness in the Area of Business Processes and Services

Lohmann, N., & Wolf, K. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-15618-2_7 · Cited by 18

Parallel Combinational Equivalence Checking

Possani, V. N., Mishchenko, A., Ribas, R. P., & Reis, A. I. (2019) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2019.2946254 · Cited by 17

Backdoors to q-Horn

Gaspers, S., Ordyniak, S., Ramanujan, M. S., Saurabh, S., & Szeider, S. (2014) · Algorithmica · doi:10.1007/s00453-014-9958-5 · Cited by 17

Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems

Semenov, A., Otpuschennikov, I. V., Gribanova, I., Заикин, О. С., & Kochemazov, S. (2020) · Logical Methods in Computer Science · doi:10.23638/lmcs-16(1:29)2020 · Cited by 17

Bosphorus: Bridging ANF and CNF Solvers

Choo, D., Soos, M., Chai, K. M. A., & Meel, K. S. (2019) · Design, Automation, and Test in Europe · doi:10.23919/date.2019.8715061 · Cited by 17

Advancements in Applications of Quantum Entanglement

Yu, Y. (2021) · Journal of Physics Conference Series · doi:10.1088/1742-6596/2012/1/012113 · Cited by 18

Learning finite cover automata from queries

Ipate, F. (2011) · Journal of Computer and System Sciences · doi:10.1016/j.jcss.2011.04.002 · Cited by 16

What is answer set programming to propositional satisfiability

Lierler, Y. (2016) · Constraints · doi:10.1007/s10601-016-9257-7 · Cited by 16

A SAT-based autonomous strategy for security vulnerability management

Barrère, M., Badonnel, R., & Festor, O. (2014) · IEEE/IFIP Network Operations and Management Symposium (NOMS) · doi:10.1109/noms.2014.6838309 · Cited by 16

Bounded Semantics of CTL and SAT-Based Verification

Zhang, W. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-10373-5_15 · Cited by 15

An Autonomous Engine for Services Configuration and Deployment

Cuadrado, F., Dueñas, J. C., & García-Carmona, R. (2011) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2011.24 · Cited by 15

Bounded sequence testing from deterministic finite state machines

Ipate, F. (2010) · Theoretical Computer Science · doi:10.1016/j.tcs.2010.01.030 · Cited by 15

Online over time processing of combinatorial problems

Duque, R., Arbeláez, A., & Díaz, J. F. (2018) · Constraints · doi:10.1007/s10601-018-9287-4 · Cited by 14

Automatic Constraint Based Test Generation for Behavioral HDL Models

Hari, S. K. S., Konda, V. V. R., Kamakoti, V., Vedula, V. M., & Maneperambil, K. S. (2008) · IEEE Transactions on Very Large Scale Integration (VLSI) Systems · doi:10.1109/tvlsi.2008.917424 · Cited by 14

Scalable constraint-based virtual data center allocation

Bayless, S., Kodirov, N., Iqbal, S. M., Beschastnikh, I., Hoos, H. H., & Hu, A. J. (2019) · Artificial Intelligence · doi:10.1016/j.artint.2019.103196 · Cited by 14

Verification and refutation of C programs based on k-induction and invariant inference

Alhawi, O. M. K., Rocha, H. O., Gadelha, M. R., Cordeiro, L. C., & Batista, E. (2020) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-020-00564-1 · Cited by 14

Chapter 12 Temporal Representation and Reasoning

(2008) · Foundations of artificial intelligence · doi:10.1016/s1574-6526(07)03012-x · Cited by 14

Ant Colony Optimization with Adaptive Fitness Function for Satisfiability Testing

Villagra, M., & Barán, B. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-73445-1_26 · Cited by 14

QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure

Wu, C.-A. R., Lin, T.-H., Lee, C.-C., & Huang, C.-Y. R. (2007) · Design, Automation, and Test in Europe · doi:10.1109/date.2007.364479 · Cited by 14

qbf2epr: A Tool for Generating EPR Formulas from QBF

Seidl, M., Lonsing, F., & Biere, A. (2018) · EPiC series in computing · doi:10.29007/2b5d · Cited by 13

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