The DOI matches its Crossref record; 123 of the 131 references it cites were found in a registry or an index.
A survey of recent advances in SAT-based formal verification
Overview
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
In the citing paper
“Algorithms for Circuit SAT can be used to solve a plethora of problems related to electronic circuits; examples include design automation, circuit equivalence and model checking. 20”
From Quantum algorithms: an overview (2016) · cites this paper as [20]
Citations
Cites
(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
Clarke, E. M., Grümberg, O., & Long, D. (1996) · Cited by 6,877
Clarke, E. M., & Schlingloff, B. (1999) · Cited by 4,237
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
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
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
Research works printed but not linked: 6
- Donini FM, Liberatore P, Massacci F, Schaerf M (2002) Solving QBF with SMV. In: Proceedings of the 8th international conference on principles of knowledge representation and reasoning (KR), pp 578–589
- Gupta A, Yang Z, Ashar P, Gupta A (2000) SAT based state reachability analysis and model checking. In: Hunt WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD), November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 354–371
- Sheng S, Takayama K, Hsiao MS (2002) Effective static property checking using simulation-based ATPG. In: Proceedings of the 39th conference on design automation (DAC), June 2002, pp 813–818
- Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time. In: Proceedings of the 5th annual ACM symposium on the theory of computing (STOC), pp 1–9
- Whittemore JP, Kim J, Sakallah KA (2001) SATIRE: A new incremental satisfiability engine. In: Proceedings of the 38th conference on design automation (DAC), June 2001, pp 542–545 · DOI
- Zhang L, Malik S (2002) Towards symmetric treatment of conflicts and satisfaction in quantified Boolean satisfiability solvers. In: Van Hentenryck P (ed) Proceedings of the 8th international conference on principles and practice of constraint programming (CP). Lecture notes in computer science, vol 2470. Springer, Berlin Heidelberg New York, pp 200–215
Cited by
Sorted by citations
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 315
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
Self-citation
Metadata
- Authors
- Prasad, M. R., Biere, A., & Gupta, A.
- Affiliations
- Fujitsu (United States) (US)
- Johannes Kepler University of Linz (AT)
- Corresponding author
- Biere, Armin
- Venue
- International Journal on Software Tools for Technology Transfer
- Published
- 2005-01-25
- Volume
- 7
- Issue
- 2
- Pages
- 156-173
- ISSN
- 1433-2779 (ISSN-L)
- 1433-2787
- OpenAlex
- W2001859357
- Cited by
- 279
- References
- 131
- Citations by year
- 2026: 2 · 2025: 5 · 2024: 5 · 2023: 9 · 2022: 4 · 2021: 10 · 2020: 10 · 2019: 11 · 2018: 17 · 2017: 10 · 2016: 14 · 2015: 11 · 2014: 12 · 2013: 15 · 2012: 14
- FWCI
- 22.59
- Type
- journal article
- Language
- en
- Open access
- closed
- Licence
- www.springer.com/tdm (tdm)
- Locations
- International Journal on Software Tools for Technology Transfer (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- bounded model checking, model checking, SAT solvers, design verification
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
