Embedding SMT-LIB into B for Interactive Proof and Constraint Solving | SpringerLink
Skip to main content
Springer Nature Link
Log in

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

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

  • 922 Accesses

Abstract

The SMT-LIB language and the B language are both based on predicate logic and have some common operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation from SMT-LIB to B. Using this translation, SMT-LIB can be analyzed by tools developed for the B method. We show how Atelier B can be used for automatic and interactive proof of SMT-LIB problems. Furthermore, we incorporated our translation into the model checker ProB and applied it to several benchmarks taken from the SMT-LIB repository. In contrast to most SMT solvers, ProB relies on finite domain constraint propagation, with support for infinite domains by keeping track of the exhaustiveness of domain variable enumerations. Our goal was to see whether this kind of approach is beneficial for SMT solving.

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
¥17,985 /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
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

    The CLP(FD) library employed by ProB may generate overflows, which ProB tries to catch and provide alternative treatment for. In case this is not possible, ProB reports “unknown”.

  2. 2.

    More precisely, the definition of division in B [1] is \(n/m = \min (\{x ~|~ x \in \mathbb {N} \wedge n < m * succ(x)\})\).

  3. 3.

    We may improve our translation to remedy this, but our assumption is that most SMT-LIB examples are well-defined according to B.

  4. 4.

    At commit a6bd02c5c442b806b5e01fed40ab9d1017e42bc3, see https://github.com/CVC4/CVC4/blob/a6bd02c5c442b806b5e01fed40ab9d1017e42bc3/src/theory/arith/theory_arith_private.cpp#L1231 for the full file and context.

  5. 5.

    The development version of ProB is available at http://www3.hhu.de/stups/prob/Download.

  6. 6.

    See http://smtcomp.sourceforge.net/2016/results-NIA.shtml.

References

  1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    Book  Google Scholar 

  2. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

    Book  Google Scholar 

  3. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_32

    Chapter  Google Scholar 

  4. Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 242–269. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_13

    Chapter  MATH  Google Scholar 

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

  6. Barrett, C., de Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_4

    Chapter  Google Scholar 

  7. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Tech. rep., Department of Computer Science, The University of Iowa (2015). www.SMT-LIB.org

  8. 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 (LNAI), vol. 6803, pp. 116–130. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_11

    Chapter  Google Scholar 

  9. Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11

    Chapter  Google Scholar 

  10. Boute, R.T.: The Euclidean definition of the functions div and mod. ACM Trans. Program. Lang. Syst. 14(2), 127–144 (1992)

    Article  Google Scholar 

  11. Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_12

    Chapter  Google Scholar 

  12. Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_16

    Chapter  MATH  Google Scholar 

  13. Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 126–136. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46508-1_8

    Chapter  Google Scholar 

  14. Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0033845

    Chapter  Google Scholar 

  15. Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_12

    Chapter  Google Scholar 

  16. ClearSy: Atelier B 4.1 Release Notes. Aix-en-Provence, France (2009). http://www.atelierb.eu/

  17. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)

    Article  MathSciNet  Google Scholar 

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

  19. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194–207. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30885-7_14

    Chapter  Google Scholar 

  20. Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290–293. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_26

    Chapter  Google Scholar 

  21. Duck, G.J.: SMCHR: satisfiability modulo constraint handling rules. CoRR, abs/1210.5307 (2012)

    Article  MathSciNet  Google Scholar 

  22. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Chapter  Google Scholar 

  23. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(2), 130–143 (2014)

    Article  Google Scholar 

  24. Fröhlich, A., Kovásznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: Proceedings SMT Workshop, pp. 6–15 (2013)

    Google Scholar 

  25. Frühwirth, T.: Theory and practice of constraint handling rules. J. Logic Program. 37(1–3), 95–138 (1998)

    Article  MathSciNet  Google Scholar 

  26. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_14

    Chapter  Google Scholar 

  27. Hansen, D., Leuschel, M.: Translating TLA\(^+\) to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_3

    Chapter  Google Scholar 

  28. Middeldorp, A., Sato, T. (eds.): FLOPS 1999. LNCS, vol. 1722. Springer, Heidelberg (1999). https://doi.org/10.1007/10705424

    Book  Google Scholar 

  29. Howe, J.M., King, A.: A pearl on SAT and SMT solving in prolog. Theor. Comput. Sci. 435, 43–55 (2012)

    Article  MathSciNet  Google Scholar 

  30. Knuth, D.E.: The art of computer programming, volume 1: Fundamental Algorithms, vol. 1. Addison Wesley Longman Publishing Co., Inc., Redwood City (1997)

    MATH  Google Scholar 

  31. Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: The vampire and the FOOL. In: Proceedings CPP, CPP 2016, pp. 37–48. ACM (2016)

    Google Scholar 

  32. Kotelnikov, E., Kovács, L., Voronkov, A.: A first class boolean sort in first-order theorem proving and TPTP. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 71–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_5

    Chapter  Google Scholar 

  33. Krings, S., Leuschel, M.: SMT solvers for validation of B and event-B models. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361–375. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_23

    Chapter  Google Scholar 

  34. Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the prob constraint solver 10 years on. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427–446. Wiley ISTE (2014)

    Google Scholar 

  35. Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)

    Article  MathSciNet  Google Scholar 

  36. Matos, P.J., Fischer, B., Marques-Silva, J.: A lazy unbounded model checker for Event-B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 485–503. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_25

    Chapter  Google Scholar 

  37. Reger, G., Suda, M., Voronkov, A.: Instantiation and pretending to be an SMT solver with vampire. In: Proceedings SMT Workshop (2012)

    Google Scholar 

  38. Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_30

    Chapter  Google Scholar 

  39. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367–373. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_28

    Chapter  Google Scholar 

  40. Weissenbacher, G., Kröning, D., Rümmer, P.: A proposal for a theory of finite sets, lists, and maps for the SMT-Lib standard. In: Proceedings SMT Workshop (2009)

    Google Scholar 

  41. Witulski, J., Leuschel, M.: Checking computations of formal method tools - a secondary toolchain for ProB. In: Proceedings F-IDE, vol. 149, EPTCS. Electronic Proceedings in Theoretical Computer Science (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Düsseldorf, Universitätsstr. 1, 40225, Düsseldorf, Germany

    Sebastian Krings & Michael Leuschel

Authors
  1. Sebastian Krings
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sebastian Krings .

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

Krings, S., Leuschel, M. (2019). Embedding SMT-LIB into B for Interactive Proof and Constraint Solving. 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_15

Download citation

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

  • 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