Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Testing a Saturation-Based Theorem Prover: Experiences and Challenges

  • Conference paper
  • First Online:
Tests and Proofs (TAP 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10375))

Included in the following conference series:

  • 562 Accesses

Abstract

This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience with developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.

This work was supported by EPSRC Grant EP/K032674/1, ERC Starting Grant 2014 SYMCAR 639270, Austrian research projects FWF S11403-N23 and S11409-N23, and the Wallenberg Academy Fellowship 2014 – TheProSE.

Andrei Voronkov—EasyChair

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    See http://smtcomp.sourceforge.net/2016/.

  2. 2.

    Consisting of 46 nodes with quad-core Intel Xeon CPUs and 12 GB RAM.

  3. 3.

    http://valgrind.org.

  4. 4.

    All TPTP-compliant provers must produce proofs in this format (see http://www.cs.miami.edu/~tptp/TPTP/QuickGuide/Derivations.html). We note that the TPTP project also provides separate proof checking tools [23].

  5. 5.

    Currently we use E [22], iProver [13], and CVC4 [3] as independent provers but could use any accepting TPTP formatted problems.

References

  1. Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39–55. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38916-0_3

    Chapter  Google Scholar 

  2. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, vol. 1, chap. 2, pp. 19–99. Elsevier Science (2001)

    Google Scholar 

  3. Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  4. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org

  5. Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14186-7_6

    Google Scholar 

  6. Creignou, N., Egly, U., Seidl, M.: A framework for the specification of random SAT and QSAT formulas. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 163–168. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30473-6_14

    Chapter  Google Scholar 

  7. Dershowitz, N., Jayasimha, D.N., Park, S.: Bounded fairness. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 304–317. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39910-0_14

    Chapter  Google Scholar 

  8. Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29–41 (2014). Theoretical Aspects of Computing (ICTAC 2011)

    Article  MathSciNet  MATH  Google Scholar 

  9. Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40–59. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04694-0_4

    Chapter  Google Scholar 

  10. Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 313–329. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_22

    Google Scholar 

  11. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_23

    Chapter  Google Scholar 

  12. Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015)

    Article  MATH  Google Scholar 

  13. Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 292–298. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_24

    Chapter  Google Scholar 

  14. Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  15. Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: The 8th International Workshop on the Implementation of Logics, IWIL 2010. EPiC Series in Computing, vol. 2, pp. 1–11. EasyChair (2012)

    Google Scholar 

  16. Perrouin, G., Sen, S., Klein, J., Baudry, B., Traon, Y.l.: Automated and scalable t-wise test case generation strategies for software product lines. In: Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation, ICST 2010, pp. 459–468. IEEE Computer Society (2010)

    Google Scholar 

  17. Reger, G.: Better proof output for Vampire. In: Proceedings of the 3rd Vampire Workshop, Vampire 2016. EPiC Series in Computing, vol. 44, pp. 46–60. EasyChair (2017)

    Google Scholar 

  18. Reger, G., Suda, M.: The uses of sat solvers in vampire. In: Proceedings of the 1st and 2nd Vampire Workshops. EPiC Series in Computing, vol. 38, pp. 63–69. EasyChair (2016)

    Google Scholar 

  19. Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016. EPiC Series in Computing, vol. 41, pp. 11–23. EasyChair (2016)

    Google Scholar 

  20. Reger, G., Suda, M., Voronkov, A.: Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). ArXiv e-prints (2017)

    Google Scholar 

  21. Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1–2), 101–115 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  22. Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002)

    MATH  Google Scholar 

  23. Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053–1070 (2006)

    Article  Google Scholar 

  24. Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)

    Article  MATH  Google Scholar 

  25. Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99–101 (2016)

    MATH  Google Scholar 

  26. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_10

    Chapter  Google Scholar 

  27. Zeller, A.: Yesterday, my program worked. Today, it does not. Why? In: Nierstrasz, O., Lemoine, M. (eds.) ESEC/FSE 1999. LNCS, vol. 1687, pp. 253–267. Springer, Heidelberg (1999). doi:10.1007/3-540-48166-4_16

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, Manchester, UK

    Giles Reger & Andrei Voronkov

  2. TU Wien, Vienna, Austria

    Martin Suda

  3. Chalmers University of Technology, Gothenburg, Sweden

    Andrei Voronkov

Authors
  1. Giles Reger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Suda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Suda .

Editor information

Editors and Affiliations

  1. Technical University of Darmstadt, Darmstadt, Germany

    Sebastian Gabmeyer

  2. University of Oslo, Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Reger, G., Suda, M., Voronkov, A. (2017). Testing a Saturation-Based Theorem Prover: Experiences and Challenges. In: Gabmeyer, S., Johnsen, E. (eds) Tests and Proofs. TAP 2017. Lecture Notes in Computer Science(), vol 10375. Springer, Cham. https://doi.org/10.1007/978-3-319-61467-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-61467-0_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-61466-3

  • Online ISBN: 978-3-319-61467-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation