Skip to main content
SpringerLink
Log in

Automatic Verification of TLA +  Proof Obligations with SMT Solvers

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7180))

Abstract

TLA +  is a formal specification language that is based on ZF set theory and the Temporal Logic of Actions TLA. The TLA +  proof system tlaps assists users in deductively verifying safety properties of TLA +  specifications. tlaps is built around a proof manager, which interprets the TLA +  proof language, generates corresponding proof obligations, and passes them to backend verifiers. In this paper we present a new backend for use with SMT solvers that supports elementary set theory, functions, arithmetic, tuples, and records. Type information required by the solvers is provided by a typing discipline for TLA +  proof obligations, which helps us disambiguate the translation of expressions of (untyped) TLA +  , while ensuring its soundness. Preliminary results show that the backend can help to significantly increase the degree of automation of certain interactive proofs.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Satisfiability Modulo Theories (SMT 2010), Edinburgh, UK (2010), http://www.SMT-LIB.org

  2. Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 116–130. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Chaudhuri, K., et al.: Verifying Safety Properties with the TLA + Proof System. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 142–148. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. de Moura, L., Bjørner, N.S.: 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 

  7. Déharbe, D.: Automatic Verification for a Class of Proof Obligations with SMT-Solvers. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 217–230. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Dutertre, B., de Moura, L.: The Yices SMT solver. Tool Paper (2006), http://yices.csl.sri.com/tool-paper.pdf

  9. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–454 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  10. Lamport, L.: Specifying Systems: The TLA +  Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  11. Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Trans. Prog. Lang. Syst. 21(3), 502–526 (1999)

    Article  Google Scholar 

  12. Parno, B., Lorch, J.R., Douceur, J.R., Mickens, J., McCune, J.M.: Memoir: Practical state continuity for protected modules. In: IEEE Symp. Security and Privacy, Berkeley, California, U.S.A., 2011. IEEE Computer Society. Formal Specifications and Correctness Proofs: Tech. Report, Microsoft Research (February 2011)

    Google Scholar 

  13. Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Nancy Grand-Est & LORIA, Nancy, France

    Stephan Merz & Hernán Vanzetto

  2. Microsoft Research-INRIA Joint Centre, Saclay, France

    Hernán Vanzetto

Authors
  1. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hernán Vanzetto
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. School of computer Science, University of Manchester, Kilburn Building, Oxford Road, MP13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Merz, S., Vanzetto, H. (2012). Automatic Verification of TLA +  Proof Obligations with SMT Solvers. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28717-6_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28716-9

  • Online ISBN: 978-3-642-28717-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation