Skip to main content
SpringerLink
Log in

Interactive Visualization of Saturation Attempts in Vampire

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2019)

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

Included in the following conference series:

Abstract

Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or models. Such an analysis is challenging due to the large number of logical formulas generated during proof/model search. In this paper we focus on saturation-based first-order theorem proving and introduce the SatVis tool for interactively visualizing saturation-based proof attempts in first-order theorem proving. We build SatVis on top of the world-leading theorem prover Vampire, by interactively visualizing the saturation attempts of Vampire in SatVis. Our work combines the automatic layout and visualization of the derivation graph induced by the saturation attempt with interactive transformations and search functionality. As a result, we are able to analyze and debug (failed) proof attempts of Vampire. Thanks to its interactive visualisation, we believe SatVis helps both experts and non-experts in theorem proving to understand first-order proofs and analyze/refine failing proof attempts of first-order provers.

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

Notes

  1. 1.

    https://smt-comp.github.io/.

  2. 2.

    A sink-node is a node such that no edge emerges out of it.

  3. 3.

    https://pygraphviz.github.io.

  4. 4.

    https://visjs.org/.

References

  1. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  2. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017)

    Google Scholar 

  3. Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., Maffei, M.: Verifying relational properties using trace logic. In: FMCAD (2019, to appear)

    Google Scholar 

  4. Byrnes, J., Buchanan, M., Ernst, M., Miller, P., Roberts, C., Keller, R.: Visualizing proof search for theorem prover development. ENTCS 226, 23–38 (2009)

    Google Scholar 

  5. 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). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  6. Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Softw. Pract. Exp. 30(11), 1203–1233 (2000)

    Article  Google Scholar 

  7. Kotelnikov, E., Kovács, L., Voronkov, A.: A FOOLish encoding of the next state relations of imperative programs. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 405–421. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_27

    Chapter  Google Scholar 

  8. Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: POPL, pp. 260–270. ACM (2017)

    Google Scholar 

  9. 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). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  10. Libal, T., Riener, M., Rukhaia, M.: Advanced proof viewing in ProofTool. In: UITP, pp. 35–47 (2014)

    Article  MathSciNet  Google Scholar 

  11. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp. 371–443 (2001)

    Chapter  Google Scholar 

  12. Rothenberger, F.: Integration and analysis of alternative SMT solvers for software verification. Master’s thesis, ETH Zurich, Zürich. Masterarbeit (2016)

    Google Scholar 

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

    MATH  Google Scholar 

  14. Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 6–22. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74510-5_4

    Chapter  Google Scholar 

  15. Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_31

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

This work was funded by the ERC Starting Grant 2014 SYMCAR 639270, the ERC Proof of Concept Grant 2018 SYMELS 842066, the Wallenberg Academy Fellowship 2014 TheProSE and the Austrian FWF project W1255-N23.

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Bernhard Gleiss, Laura Kovács & Lena Schnedlitz

  2. Chalmers University of Technology, Gothenburg, Sweden

    Laura Kovács

Authors
  1. Bernhard Gleiss
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laura Kovács
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lena Schnedlitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernhard Gleiss .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Gleiss, B., Kovács, L., Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34968-4_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34967-7

  • Online ISBN: 978-3-030-34968-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation