Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2012: Automated Reasoning pp 1–8Cite as

Taking Satisfiability to the Next Level with Z3

(Abstract)

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7364))

Abstract

Several applications from program analysis, design and testing rely critically on solving SMT problems. Many applications build on top of SMT solvers in sophisticated ways by carefully crafting the solver interaction.We illustrate partial correctness checking as an SMT problem and we introduce a procedure for model finding of recursive Horn clauses with arithmetic.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009)

    Google Scholar 

  2. de Moura, L., Bjørner, N.: Satisfiability Modulo Theories: Introduction & Applications. Comm. ACM (2011)

    Google Scholar 

  3. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Beyer, D.: Competition on Software Verification - (SV-COMP). In: [33], pp. 504–524

    Google Scholar 

  5. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)

    Google Scholar 

  6. Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp. 266–278. ACM (2011)

    Google Scholar 

  7. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 302–314. ACM (2009)

    Google Scholar 

  9. Rustan, K., Leino, M.: Developing Verified Programs with Dafny. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, p. 82. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory Safety for Systems-Level Code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Lahiri, S., Hawblitzel, C., Kawaguchi, M., Rebelo, H.: SymDiff: A language-agnostic semantic diff tool for imperative programs, (Tool description) (2012)

    Google Scholar 

  12. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. SIGPLAN Not. 37, 1–3 (2002)

    Article  Google Scholar 

  13. Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Lal, A., Qadeer, S., Lahiri, S.: Corral: A Solver for Reachability Modulo Theories (2012)

    Google Scholar 

  15. Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi Project: Software Property Checking via Static Analysis and Testing. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 178–181. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Godefroid, P., de Halleux, J., Nori, A.V., Rajamani, S.K., Schulte, W., Tillmann, N., Levin, M.Y.: Automating Software Testing Using Program Analysis. IEEE Software 25, 30–37 (2008)

    Article  Google Scholar 

  17. Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., Wurden, F.L.: Model-Based Quality Assurance of Windows Protocol Documentation. In: ICST, pp. 502–506. IEEE Computer Society (2008)

    Google Scholar 

  18. Jackson, E.K., Kang, E., Dahlweid, M., Seifert, D., Santen, T.: Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT, pp. 39–48 (2010)

    Google Scholar 

  19. Veanes, M., Bjørner, N.: Symbolic Automata: The Toolkit. In: [33], pp. 472–477

    Google Scholar 

  20. Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 313–326. ACM (2010)

    Google Scholar 

  21. Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 99–110. ACM (2010)

    Google Scholar 

  22. Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: [34], pp. 85–96

    Google Scholar 

  23. Köksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: [34], pp. 151–164

    Google Scholar 

  24. Chugh, R., Rondon, P.M., Jhala, R.: Nested refinements: a logic for duck typing. In: [34], pp. 231–244

    Google Scholar 

  25. Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: [34], pp. 123–136

    Google Scholar 

  26. Bjørner, N., Browne, A., Manna, Z.: Automatic Generation of Invariants and Assertions. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, pp. 589–623. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  27. Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  28. Hoder, K., Bjørner, N.: Generalized Property Directed Reachability. In: SAT (2012)

    Google Scholar 

  29. Silva, J.P.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48, 506–521 (1999)

    Article  Google Scholar 

  30. McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD (2011)

    Google Scholar 

  31. Gupta, A., Popeea, C., Rybalchenko, A.: Solving Recursion-Free Horn Clauses over LI+UIF. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 188–203. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: [33], pp. 157–172

    Google Scholar 

  33. Flanagan, C., König, B. (eds.): TACAS 2012. LNCS, vol. 7214. Springer, Heidelberg (2012)

    MATH  Google Scholar 

  34. Field, J., Hicks, M. (eds.): Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28. ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, USA

    Nikolaj Bjørner

Authors
  1. Nikolaj Bjørner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bjørner, N. (2012). Taking Satisfiability to the Next Level with Z3. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31365-3_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31364-6

  • Online ISBN: 978-3-642-31365-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation