Z3: An Efficient SMT Solver
Integrity signals
Registry
Cites
Statistics
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?
Type checking in Granule, if successful, outputs a predicate capturing theorems about grading, which is compiled to SMT-LIB and passed to a compatible solver (Z3).
“Type checking, if successful, outputs a predicate capturing theorems about grading, which is compiled to the SMT-LIB format [Barrett et al. 2010] and passed to any compatible solver (we use Z3 [De Moura and Bjørner 2008]).”
From Quantitative program reasoning with graded modal types (2019) · cites this paper as De Moura and Bjørner 2008
Cited by
Sorted by citations
Dafny: An Automatic Program Verifier for Functional Correctness
Leino, K. R. M. (2010) · Lecture Notes in Computer Science · doi:10.1007/978-3-642-17511-4_20 · Cited by 940 · see citing works
A survey of symbolic execution techniques
Baldoni, R., Coppa, E., D’elia, D. C., Demetrescu, C., & Finocchi, I. (2019) · ACM Computing Surveys · doi:10.1145/3182657 · Cited by 708 · see citing works
Solving olympiad geometry without human demonstrations
Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024) · Nature · doi:10.1038/s41586-023-06747-5 · Cited by 311 · see citing works
Mapping Quantum Circuits to IBM QX Architectures Using the Minimal Number of SWAP and H Operations
Wille, R., Burgholzer, L., & Zulehner, A. (2019) · Proceedings of the 56th Annual Design Automation Conference 2019 · doi:10.1145/3316781.3317859 · Cited by 207 · see citing works
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
Vandin, A., ter Beek, M. H., Legay, A., & Lluch Lafuente, A. (2018) · EasyChair Preprints · doi:10.29007/1mjd · Cited by 196 · see citing works
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Pan, L., Albalak, A., Wang, X., & Wang, W. Y. (2023) · arXiv · doi:10.48550/arxiv.2305.12295 · Cited by 144 · see citing works
“For solving SAT problems, we use the Z3 theorem prover (de Moura and Bjørner, 2008), a satisfiability modulo theories (SMT) solver developed by Microsoft 4 .”
BackgroundMethodFaith and Fate: Limits of Transformers on Compositionality
Dziri, N., Lu, X., Sclar, M., Li, X. (., Jiang, L., Lin, B. Y., Welleck, S., West, P., Bhagavatula, C., Bras, R. L., et al. (2023) · Advances in Neural Information Processing Systems 36 · doi:10.52202/075280-3081 · Cited by 124 · see citing works
“Graph Construction Algorithm To solve the complex compositional reasoning process for a logical grid puzzle, we use existing puzzle solvers [21] to generate the computation graph.”
MethodFaith and Fate: Limits of Transformers on Compositionality
Dziri, N., Lu, X., Sclar, M., Li, X. L., Jiang, L., Lin, B. Y., West, P., Bhagavatula, C., Bras, R. L., Hwang, J. D., et al. (2023) · arXiv · Cited by 124 · see citing works
A Formal Foundation for Secure Remote Execution of Enclaves
Subramanyan, P., Sinha, R., Lebedev, I., Devadas, S., & Seshia, S. A. (2017) · Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security · doi:10.1145/3133956.3134098 · Cited by 119 · see citing works
Program synthesis using conflict-driven learning
Feng, Y., Martins, R., Bastani, O., & Dillig, I. (2018) · Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/3192366.3192382 · Cited by 111 · see citing works
Optimal layout synthesis for quantum computing
Tan, B., & Cong, J. (2020) · Proceedings of the 39th International Conference on Computer-Aided Design · doi:10.1145/3400302.3415620 · Cited by 126 · see citing works
Semantic-based Automated Reasoning for AWS Access Policies using SMT
Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., & Varming, C. (2018) · 2018 Formal Methods in Computer Aided Design (FMCAD) · doi:10.23919/fmcad.2018.8602994 · Cited by 106 · see citing works
Semantic program alignment for equivalence checking
Churchill, B., Padon, O., Sharma, R., & Aiken, A. (2019) · Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/3314221.3314596 · Cited by 97
FairSquare: probabilistic verification of program fairness
Albarghouthi, A., D'Antoni, L., Drews, S., & Nori, A. V. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3133904 · Cited by 94 · see citing works
Quantitative program reasoning with graded modal types
Orchard, D., Liepelt, V.-B., & Eades III, H. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3341714 · Cited by 85 · see citing works
Reinforcement Quantum Annealing: A Hybrid Quantum Learning Automata
Ayanzadeh, R., Halem, M., & Finin, T. (2020) · Scientific Reports · doi:10.1038/s41598-020-64078-1 · Cited by 57 · see citing works
Constraint-Based Synthesis of Datalog Programs
Albarghouthi, A., Koutris, P., Naik, M., & Smith, C. (2017) · Lecture Notes in Computer Science · doi:10.1007/978-3-319-66158-2_44 · Cited by 40 · see citing works
Nye, M., Tessler, M. H., Tenenbaum, J. B., & Lake, B. M. (2021) · arXiv · doi:10.48550/arxiv.2107.02794 · Cited by 40 · see citing works
Towards AI-Assisted Synthesis of Verified Dafny Methods
Misu, M. R. H., Lopes, C. V., Ma, I., & Noble, J. (2024) · Proceedings of the ACM on Software Engineering · doi:10.1145/3643763 · Cited by 38 · see citing works
Synthesis of biological models from mutation experiments
Koksal, A. S., Pu, Y., Srivastava, S., Bodik, R., Fisher, J., & Piterman, N. (2013) · Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages · doi:10.1145/2429069.2429125 · Cited by 36 · see citing works
Ming, J., Zhang, F., Wu, D., Liu, P., & Zhu, S. (2016) · IEEE Transactions on Reliability · doi:10.1109/tr.2016.2570554 · Cited by 33 · see citing works
Dsc+Mock: a test case + mock class generator in support of coding against interfaces
Islam, M., & Csallner, C. (2010) · Proceedings of the Eighth International Workshop on Dynamic Analysis · doi:10.1145/1868321.1868326 · Cited by 30 · see citing works
Measuring code behavioral similarity for programming and software engineering education
Li, S., Xiao, X., Bassett, B., Xie, T., & Tillmann, N. (2016) · Proceedings of the 38th International Conference on Software Engineering Companion · doi:10.1145/2889160.2889204 · Cited by 30 · see citing works
Horus: Non-Intrusive Causal Analysis of Distributed Systems Logs
Neves, F., Machado, N., Vilaca, R., & Pereira, J. (2021) · 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) · doi:10.1109/dsn48987.2021.00035 · Cited by 8 · see citing works
Qualitative Analysis for Validating IEC 62443-4-2 Requirements in DevSecOps
Göttel, C., Kabir-Querrec, M., Kozhaya, D., Sivanthi, T., & Vuković, O. (2023) · 2023 IEEE 28th International Conference on Emerging Technologies and Factory Automation (ETFA) · doi:10.1109/etfa54631.2023.10275637 · Cited by 7 · see citing works
Iacobelli, A., Rinieri, L., Melis, A., Sadi, A. A., Prandini, M., & Callegati, F. (2024) · 2024 IEEE 7th International Conference on Industrial Cyber-Physical Systems (ICPS) · doi:10.1109/icps59941.2024.10639995 · Cited by 5 · see citing works
VERINA: Benchmarking Verifiable Code Generation
Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., & Song, D. (2025) · arXiv · doi:10.48550/arxiv.2505.23135 · Cited by 3 · see citing works
“Verification-oriented languages like Dafny [29] and Verus [30] leverage SMT solvers for automated theorem proving [31, 32] and consume only proof hints, such as loop invariants [33] and assertions [34].”
Progent: Securing AI Agents with Privilege Control
Shi, T., He, J., Wang, Z., Li, H., Wu, L., Guo, W., & Song, D. (2025) · arXiv · doi:10.48550/arxiv.2504.11703 · Cited by 3 · see citing works
Eilers, M., Schwerhoff, M., Summers, A. J., & Müller, P. (2025) · Lecture Notes in Computer Science · doi:10.1007/978-3-031-98668-0_5 · Cited by 2 · see citing works
Decentralized Self-Verifiable Cryptographic Image Provenance in Social Internet of Things
Akram, J., Akram, A., & Anaissi, A. (2026) · Future Internet · doi:10.3390/fi18080402
- Authors
- de Moura, L., & Bjørner, N.
- Affiliations
- Microsoft (United States) (US)
- ORCID
- Bjørner, Nikolaj
- Venue
- Lecture Notes in Computer Science
- Publisher
- Springer Berlin Heidelberg
- Published
- 2008
- Pages
- 337-340
- ISSN
- 0302-9743 (ISSN-L)
- 1611-3349
- OpenAlex
- W1480909796
- Cited by
- 6,595
- References
- 0
- Citations by year
- 2026: 402 · 2025: 492 · 2024: 465 · 2023: 423 · 2022: 407 · 2021: 553 · 2020: 516 · 2019: 465 · 2018: 407 · 2017: 418 · 2016: 362 · 2015: 368 · 2014: 358 · 2013: 312 · 2012: 214
- FWCI
- 114.54
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- Lecture notes in computer science (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- Z3, SMT solvers, satisfiability modulo theories, decision procedures, first-order logic, background theory, bit vectors, arrays, uninterpreted functions, software 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
