Cited by 279Formal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques

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

Prasad, Mukul R., Biere, Armin, Gupta, Aarti·2005·International Journal on Software Tools for Technology Transfer

DOI 10.1007/s10009-004-0183-4

Open this paper in CoChat — free account

Integrity signals

Registry

Crossref · 10.1007/s10009-004-0183-4

Cites

123 of 123 references verified0 citation errors · 0 not checkable

Statistics

Recomputing p-values needs the paper’s full text.

Claims the paper makes

We couldn’t retrieve this paper’s full text, so its claims and self-check weren’t run. The registry and citation checks still apply.

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?

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

Flagged first, then by citations

Show all 131 references

8 of the 131 references couldn’t be matched to a known paper.

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

Sorted by citations

Items 101–200 of 278

Guiding Formal Verification Orchestration Using Machine Learning Methods
Mandouh, E. E., & Wassal, A. G. (2018) · ACM Transactions on Design Automation of Electronic Systems · doi:10.1145/3224206 · Cited by 13
Sequential equivalence checking between system level and RTL descriptions
Vasudevan, S., Viswanath, V., Abraham, J. A., & Tu, J. (2008) · Design Automation for Embedded Systems · doi:10.1007/s10617-008-9033-z · Cited by 13
Model-driven allocation engineering: specifying and solving constraints based on the example of automotive systems
Pohlmann, U., & Hüwe, M. (2018) · Automated Software Engineering · doi:10.1007/s10515-018-0248-3 · Cited by 13
Continuous Search in Constraint Programming
Arbeláez, A., Hamadi, Y., & Sébag, M. (2011) · Springer eBooks · doi:10.1007/978-3-642-21434-9_9 · Cited by 13
Pattern QUBOs: Algorithmic Construction of 3SAT-to-QUBO Transformations
Zielinski, S., Nüßlein, J., Stein, J., Gabor, T., Linnhoff–Popien, C., & Feld, S. (2023) · Electronics · doi:10.3390/electronics12163492 · Cited by 12
On designing and testing distributed virtual environments
Valadares, A., Gabrielova, E., & Lopes, C. V. (2016) · Concurrency and Computation Practice and Experience · doi:10.1002/cpe.3803 · Cited by 12
SAT-Based Verification of LTL Formulas
Zhang, W. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-70952-7_18 · Cited by 12
Efficient modeling and verification of analog/mixed-signal circuits using labeled hybrid petri nets
Little, S. (2008) · Cited by 12
Combining Abstraction Refinement and SAT-Based Model Checking
Amla, N., & McMillan, K. L. (2007) · Springer eBooks · doi:10.1007/978-3-540-71209-1_31 · Cited by 11
More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
Fröhlich, A., Kovásznai, G., & Biere, A. (2013) · Lecture notes in computer science · doi:10.1007/978-3-642-38536-0_33 · Cited by 11
Self-citation
Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches
Lierler, Y. (2021) · Theory and Practice of Logic Programming · doi:10.1017/s1471068421000478 · Cited by 11
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) · doi:10.5555/1266366.1266653 · Cited by 11
Bounded semantics
Zhang, W. (2014) · Theoretical Computer Science · doi:10.1016/j.tcs.2014.10.026 · Cited by 11
RTL VERIFICATION: FROM SAT TO SMT(BV)
Cimatti, A., & Sebastiani, R. (2008) · Cited by 11
Automated Extraction of Inductive Invariants to Aid Model Checking
Case, M. L., Mishchenko, A., & Brayton, R. K. (2007) · Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2007.9 · Cited by 10
A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis
Bertoli, P., Bozzano, M., & Cimatti, A. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-74128-2_1 · Cited by 10
Obtaining Microprocessor Vulnerability Factor Using Formal Methods
Shazli, S. Z., & Tahoori, M. B. (2008) · Proceedings · doi:10.1109/dft.2008.52 · Cited by 10
Assertion Recommendation for Formal Program Verification
Wang, C., He, F., Xiaoyu Song, B., Jiang, Y., Gu, M., & Sun, J. (2017) · IEEE Annual International Computer Software and Applications Conference (COMPSAC) · doi:10.1109/compsac.2017.66 · Cited by 10
Slicing ATL model transformations for scalable deductive verification and fault localization
Cheng, Z., & Tisi, M. (2018) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-018-0491-8 · Cited by 10
B-PERFect
Halchin, A., Feliachi, A., Singh, N. K., Aït‐Ameur, Y., & Ordioni, J. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-68499-4_11 · Cited by 10
Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings
Domshlak, C., Hoffmann, J., & Sabharwal, A. (2009) · Journal of Artificial Intelligence Research · doi:10.1613/jair.2817 · Cited by 10
A Decision-Making Procedure for Resolution-Based SAT-Solvers
Goldberg, E. (2008) · Springer eBooks · doi:10.1007/978-3-540-79719-7_11 · Cited by 10
Satisfiability-based program reasoning and program synthesis
Foster, J. S., & Srivastava, S. (2010) · Cited by 10
Liveness checking as safety checking to find shortest counterexamples to linear time properties
Schuppan, V. (2006) · Repository for Publications and Research Data (ETH Zurich) · doi:10.3929/ethz-a-005170555 · Cited by 10
A New Cryptographic Scheme Utilizing the Difficulty of Big Boolean Satisfiability
Ahmad, W., & Rushdi, A. M. A. (2018) · International Journal of Mathematical Engineering and Management Sciences · doi:10.33889/ijmems.2018.3.1-005 · Cited by 9
Amplitude amplification-inspired QAOA: improving the success probability for solving 3SAT
Mandl, A., Barzen, J., Bechtold, M., Leymann, F., & Wild, K. (2023) · Quantum Science and Technology · doi:10.1088/2058-9565/ad141d · Cited by 11
Debugging reversible circuits
Wille, R., Grosse, D. J., Frehse, S., Dueck, G. W., & Drechsler, R. (2010) · Integration · doi:10.1016/j.vlsi.2010.08.002 · Cited by 9
Automated Extraction of Inductive Invariants to Aid Model Checking
Case, M. L., Mishchenko, A., & Brayton, R. K. (2007) · Formal Methods in Computer-Aided Design · doi:10.1109/famcad.2007.12 · Cited by 9
A Framework for the Specification of Random SAT and QSAT Formulas
Creignou, N., Egly, U., & Seidl, M. (2012) · Lecture notes in computer science · doi:10.1007/978-3-642-30473-6_14 · Cited by 8
VEST - An intelligent tool for timing SoCs verification using UML timing diagrams
Pułka, A., & Milik, A. (2008) · Forum on specification and Design Languages · doi:10.1109/fdl.2008.4641432 · Cited by 8
EHSAT
Deng, S., Bian, J., Wu, W., Yang, X., & Zhao, Y. (2007) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/1278480.1278629 · Cited by 8
Exploiting Unexploited Computing Resources for Computational Logics.
Palù, A. D., Agostino Dovier, A., Formisano, A., & Pontelli, E. (2012) · Institutional Research Information System (University of Udine) · Cited by 7
Quantifier Reordering for QBF
Slivovsky, F., & Szeider, S. (2015) · Journal of Automated Reasoning · doi:10.1007/s10817-015-9353-1 · Cited by 7
Tutorial on Model Checking: Modelling and Verification in Computer Science
Biere, A. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-85101-1_2 · Cited by 7
Self-citation
Using routers to build logic circuits: How powerful is BGP?
Chiesa, M., Cittadini, L., Battista, G. D., Vanbever, L., & Vissicchio, S. (2013) · IEEE International Conference on Network Protocols (ICNP) · doi:10.1109/icnp.2013.6733584 · Cited by 7
Towards accelerating irregular EDA applications with GPUs
Qian, H., Deng, Y. S., Wang, B., & Mu, S. (2011) · Integration · doi:10.1016/j.vlsi.2011.05.004 · Cited by 7
Enhancing bug hunting using high-level symbolic simulation
Chou, H.-Z., Lin, I.-H., Yang, C.-S., Chang, K.-H., & Kuo, S. (2009) · ACM Great Lakes Symposium on VLSI (GLSVLSI) · doi:10.1145/1531542.1531637 · Cited by 7
Formal modeling and verification of software‐defined networks: A survey
Shukla, N., Pandey, M., & Srivastava, S. (2019) · International Journal of Network Management · doi:10.1002/nem.2082 · Cited by 7
Scalable Constraint-based Virtual Data Center Allocation
Bayless, S., Kodirov, N., Beschastnikh, I., Hoos, H. H., & Hu, A. J. (2017) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2017/77 · Cited by 7
On Formal Methods for Large-Scale Product Configuration
Voronov, A. (2013) · Chalmers Research (Chalmers University of Technology) · Cited by 7
Model Checking with SAT-Based Characterization of ACTL Formulas
Zhang, W. (2007) · Lecture notes in computer science · doi:10.1007/978-3-540-76650-6_12 · Cited by 7
Emerging verification methods for complex hardware in avionics
Karlsson, K., & Forsberg, H. (2006) · IEEE/AIAA Digital Avionics Systems Conference (DASC) · doi:10.1109/dasc.2005.1563385 · Cited by 7
Bounded Model Checking for Partial Kripke Structures
Wehrheim, H. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-85762-4_26 · Cited by 6
Datamining techniques and swarm intelligence for problem solving: Application to SAT
Drias, H., Hirèche, C., & Douib, A. (2013) · World Congress on Nature and Biologically Inspired Computing (NaBIC) · doi:10.1109/nabic.2013.6617862 · Cited by 6
Constraint programming heuristics for configuring optimal products in multi product lines
Ochoa, L., González-Rojas, O., Cardozo, N., González, A. N., Chavarriaga, J., Casallas, R., & Díaz, J. F. (2018) · Information Sciences · doi:10.1016/j.ins.2018.09.042 · Cited by 6
Formal Verification and Synthesis for Quality-of- Service in On-Chip Networks
Holcomb, D. E. (2013) · eScholarship (California Digital Library) · Cited by 6
Transistor Sizing for Parameter Obfuscation of Analog Circuits Using Satisfiability Modulo Theory
Rao, V. V., & Savidis, I. (2018) · IEEE Asia Pacific Conference on Circuits and Systems (APCCAS) · doi:10.1109/apccas.2018.8605710 · Cited by 5
Model Learning and Test Generation Using Cover Automata
Ipate, F., Ştefănescu, A., & Dinca, I. (2014) · The Computer Journal · doi:10.1093/comjnl/bxu032 · Cited by 5
Automated conflict resolution between multiple clinical pathways: a technology report
Litchfield, I. J., Turner, A. M., Backman, R., Filho, J. B. F., Weber, P., & Lee, M. G. (2018) · BMJ Health & Care Informatics · doi:10.14236/jhi.v25i3.986 · Cited by 5
Supervisory control using satisfiability solvers
Voronov, A., & Åkesson, K. (2008) · International Workshop on Discrete Event Systems · doi:10.1109/wodes.2008.4605926 · Cited by 5
Survey on Formal Verification Methods for Digital IC
Wang, J., Shao, J., Li, Y., & Ding, J. (2009) · International Conference on Internet Computing for Science and Engineering · doi:10.1109/icicse.2009.46 · Cited by 4
Efficient software product-line model checking using induction and a SAT solver
He, F., Gao, Y., & Yin, L. (2018) · Frontiers of Computer Science · doi:10.1007/s11704-016-6048-7 · Cited by 4
A Model-Driven Engineering Approach for Business Process Based SaaS Services Composition
Fattouch, N., Rekik, M., Wakrime, A. A., & Boukadi, K. (2019) · IEEE/ACS International Conference on Computer Systems and Applications (AICCSA) · doi:10.1109/aiccsa47632.2019.9035348 · Cited by 4
Reasoning with Propositional Logic: From SAT Solvers to Knowledge Compilation
Simon, L. (2020) · Springer eBooks · doi:10.1007/978-3-030-06167-8_5 · Cited by 4
Certified Embedding of B Models in an Integrated Verification Framework
Halchin, A., Aït‐Ameur, Y., Singh, N. K., Feliachi, A., & Ordioni, J. (2019) · International Symposium on Theoretical Aspects of Software Engineering (TASE) · doi:10.1109/tase.2019.000-4 · Cited by 4
Handling B models in the PERF integrated verification framework: Formalised and certified embedding
Halchin, A., Aït‐Ameur, Y., Singh, N. K., Ordioni, J., & Feliachi, A. (2020) · Science of Computer Programming · doi:10.1016/j.scico.2020.102477 · Cited by 4
Using Alloy in Introductory Courses of Formal Methods
Nakajima, S. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-17404-4_7 · Cited by 4
From Hardware Verification to Software Verification: Re-use and Re-learn
Gupta, A. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-77966-7_3 · Cited by 4
Self-citation
High level static analysis of system descriptions for taming verification complexity
Abraham, J. A., & Vasudevan, S. (2007) · Cited by 4
On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification
Case, M. L. (2009) · UC Berkeley · Cited by 4
Mathematical and Computer Modelling of Dynamical Systems: Methods, Tools and Applications in Engineering and Related Sciences
Rocha, C., Mendonça, T., Silva, M. E., & Frías, R. (2013) · Cited by 3
Single-Solver Algorithms for 2QBF
Bayless, S., & Hu, A. J. (2012) · Lecture notes in computer science · doi:10.1007/978-3-642-31612-8_48 · Cited by 3
Unlocking the Potential of Quantum Computing: A Comprehensive Review
-, P. S., -, S. C., & -, S. T. (2023) · International Journal For Multidisciplinary Research · doi:10.36948/ijfmr.2023.v05i06.9440 · Cited by 3
Hardened Flow-Sensitive Trace Formula for Fault Localization
Lamraoui, S.-M., Nakajima, S., & Hosobe, H. (2015) · IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) · doi:10.1109/iceccs.2015.16 · Cited by 3
Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers
Bauer, A., Leucker, M., Schallhart, C., & Tautschnig, M. (2009) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-009-0133-2 · Cited by 3
A Model-Based Autonomous Engine for Application Runtime Environment Configuration and Deployment in PaaS Cloud
Lan, X., Liu, Y., Chen, X., Huang, Y., Lin, B., & Guo, W. (2014) · IEEE International Conference on Cloud Computing Technology and Science · doi:10.1109/cloudcom.2014.80 · Cited by 3
Deductive temporal reasoning with constraints
Dixon, C., Konev, B. Y., Fisher, M., & Nietiadi, S. (2012) · Journal of Applied Logic · doi:10.1016/j.jal.2012.07.001 · Cited by 3
SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse
Andrade, F. V., Oliveira, M. C. M., Fernandes, A. O., & Coelho, C. (2007) · IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS) · doi:10.1109/ddecs.2007.4295319 · Cited by 3
SAT-based Unbounded Model Checking of Timed Automata
Penczek, W., & Szreter, M. (2008) · Fundamenta Informaticae · doi:10.3233/fun-2008-851-429 · Cited by 3
Satisfiability Advancements Enabled by State Machines
Weaver, S. (2012) · OhioLink ETD Center (Ohio Library and Information Network) · Cited by 3
Bias in algorithm portfolio performance evaluation
Cameron, C., Hoos, H. H., & Leyton‐Brown, K. (2016) · International Joint Conference on Artificial Intelligence · Cited by 3
Teaching and Practice Innovation of Embedded System Design Course Based on Proteus and Keil-electronic Stopwatch as an Example
Dan, L., Erhu, H., Yanrong, Z., & Yu, Z. (2015) · International Journal of Smart Home · doi:10.14257/ijsh.2015.9.4.13 · Cited by 3
Parameterized Graph Separation Problems: New Techniques and Algorithms
Ramanujan, M. S. (2013) · INFLIBNET · Cited by 3
Contributions to model-based diagnosis of discrete-event systems
Boussif, A. (2016) · doi:10.70675/925a979aza256z435fz8ac6z9a9f618d664c · Cited by 3
Impact of Variability Compensation on the Performance of an RRAM-based 3-SAT Solver
Heittmann, A., Hizzani, M., & Strachan, J. P. (2025) · IEEE International Symposium on Circuits and Systems proceedings · doi:10.1109/iscas56072.2025.11043674 · Cited by 2
A 28nm Mode-Reconfigurable CAM-CIM Hybrid Complete 3-SAT Solver Supporting Conflict-Driven Clause Learning with 100% Solvability
Wu, Z., Tang, X., Lin, L., Yang, Y., Luo, H., Xu, B., Liang, Y., Bo, X., & Wang, Y. (2026) · Digest of technical papers/Digest of technical papers - IEEE International Solid-State Circuits Conference · doi:10.1109/isscc49663.2026.11409109 · Cited by 2
Modular Checking of C Programs Using SAT-Based Bounded Model Checker
Hashimoto, Y., & Nakajima, S. (2009) · Asia-Pacific Software Engineering Conference (APSEC) · doi:10.1109/apsec.2009.24 · Cited by 2
Automated conflict resolution for patients with multiple morbidity being treated using more than one set of single condition clinical guidance: A case study
Litchfield, I. J., Turner, A. M., Filho, J. B. F., Lee, M. G., & Weber, P. (2022) · Computers in Biology and Medicine · doi:10.1016/j.compbiomed.2022.105381 · Cited by 2
A Variation-Tolerant Continuous-Time Ising Machine With eDRAM-Based Spin Interaction and Leaked Negative Feedback Annealing
Wu, Z., Song, J., Tang, X., Xu, B., Luo, H., Yang, Y., Wang, R., Bo, X., & Wang, Y. (2024) · IEEE Journal of Solid-State Circuits · doi:10.1109/jssc.2024.3461769 · Cited by 2
Context Petri Nets Definition and Manipulation
Cardozo, N., González, S., & Mens, K. (2012) · Cited by 2
Models for the Consistent Interaction of Adaptations in Self-Adaptive Systems
Cardozo, N., Mens, K., & Clarke, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-74183-3_11 · Cited by 2
Guiding CNF-SAT Search by Analyzing Constraint-Variable Dependencies and Clause Lengths
Durairaj, V., & Kalla, P. (2006) · Proceedings · doi:10.1109/hldvt.2006.319983 · Cited by 2
SAT-based Unbounded Model Checking of Timed Automata
Penczek, W., & Szreter, M. (2007) · International Conference on Application of Concurrency to System Design (ACSD) · doi:10.1109/acsd.2007.63 · Cited by 2
Building a Symbolic Model Checker from Formal Language Description
Bóbeda, E. L., Colange, M., & Buchs, D. (2015) · International Conference on Application of Concurrency to System Design (ACSD) · doi:10.1109/acsd.2015.10 · Cited by 2
A Formal Verification Environment for Use in the Certification of Safety-Related C Programs
Walter, D. (2010) · State and University Library Bremen · Cited by 2
Optimizations and Complexity Analysis on the Quantum Level
Abdessaied, N., & Drechsler, R. (2016) · Springer eBooks · doi:10.1007/978-3-319-31937-7_5 · Cited by 2
Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
Navarro-López, E. M., & O'Toole, M. D. (2017) · Mathematical and Computer Modelling of Dynamical Systems · doi:10.1080/13873954.2017.1369437 · Cited by 2
Sparkle: Toward Accessible Meta-Algorithmics for Improving the State of the Art in Solving Challenging Problems
van der Blom, K., Hoos, H. H., Luo, C. W., & Rook, J. (2022) · IEEE Transactions on Evolutionary Computation · doi:10.1109/tevc.2022.3215013 · Cited by 2
Boolean Satisfiability Solvers: Techniques, Implementations and Analysis
Lima, J. F. (2010) · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · Cited by 2
System on chip verification strategy based on FDL mechanism
Pułka, A. (2010) · ICSES 2010 International Conference on Signals and Electronic Circuits · Cited by 2
On the Configuration of SAT Formulae
Vallati, M., & Marco Maratea, A. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-35166-3_19 · Cited by 2
Data Driven Relational Constraint Programming
Valdron, M., & Pu, K. Q. (2020) · IEEE International Conference on Information Reuse and Integration (IRI) · doi:10.1109/iri49571.2020.00030 · Cited by 2
Self-diagnosis in Network-on-Chips
Dalirsani, A. (2015) · OPUS Publication Server of the University of Stuttgart (University of Stuttgart) · doi:10.18419/opus-3585 · Cited by 2
Modelling and Analysis of Real Time Systems with Logic Programming and Constraints
Banda, G. (2010) · University of Southern Denmark Research Portal (University of Southern Denmark) · Cited by 2
Planning with preferences using maximum satisfiability
Russell, R. A. (2021) · CL Technical Reports · doi:10.48456/tr-822 · Cited by 2
Learning during search
Rodriguez, A. A. (2011) · doi:10.70675/37ac3f0fzf87ez4642zab6ez000b386a7a0e · Cited by 2
Formal Verification of Complex Data Paths: An Industrial Experience
Seger, C.-J. H. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-90870-6_38 · Cited by 1
Polynomial formal verification parameterized by cutwidth properties of a circuit using Boolean satisfiability
Müller, L., & Drechsler, R. (2025) · Microprocessors and Microsystems · doi:10.1016/j.micpro.2025.105199 · Cited by 1
Advancing stochastic 3-SAT solvers by dissipating oversatisfied constraints
Schwardt, J., & Budich, J. C. (2025) · Proceedings of the National Academy of Sciences · doi:10.1073/pnas.2517297122 · Cited by 1
SAT, SMT and Applications
Biere, A. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-04238-6_1 · Cited by 1
Self-citation

Authors: Prasad, M. R., Biere, A., & Gupta, A.
Affiliations: Fujitsu (United States) (US)
Johannes Kepler University of Linz (AT)
Corresponding author: Biere, Armin
ORCID: Biere, Armin
Gupta, Aarti
Venue: International Journal on Software Tools for Technology Transfer
Publisher: Springer Science and Business Media LLC
Published: 2005-01-25
Volume: 7
Issue: 2
Pages: 156-173
ISSN: 1433-2779 (ISSN-L)
1433-2787
DOI: 10.1007/s10009-004-0183-4
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

A survey of recent advances in SAT-based formal verification

Overview

Integrity signals

Verification

Claims the paper makes

Claims other papers make about this one

Citations

Cites

Cited by

Related

Metadata

Record

About these checks