Skip to main content
SpringerLink
Log in

Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo

  • Conference paper
  • First Online:
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail 2016)

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

Abstract

In this paper, we report on our recent improvements in the Alt-Ergo SMT solver to make it effective in discharging proof obligations (POs) translated from the Atelier-B framework. In particular, we made important modifications in its internal data structures to boost performances of its core decision procedures, we improved quantifiers instantiation heuristics, and enhanced the interaction between the SAT solver and the decision procedures. We also introduced a new plugin architecture to facilitate experiments with different SAT engines, and implemented a profiling plugin to track and identify “bottlenecks” when a formula requires a long time to be discharged, or makes the solver timeout. Experiments made with more than 10,000 POs generated from real industrial B projects show significant improvements compared to both previous versions of Alt-Ergo and Atelier-B’s automatic main prover.

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.

    A first release is available here: http://bware.lri.fr/index.php/Benchmarks.

  2. 2.

    Triggers are terms with variables that prevent the instantiation of quantified formulas unless they “match” some ground terms present in the decision procedures.

  3. 3.

    The prelude is still under development, and some axioms may be missing to discharge a PO, or may be written in an “unsuitable” way for the solvers.

References

  1. Abrial, J.-R.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  2. Adjepon-Yamoah, D., Romanovsky, A., Iliasov, A.: A reactive architecture for cloud-based system engineering. In: Proceedings of the 2015 International Conference on Software and System Process, ICSSP 2015, pp. 77–81. ACM, New York, NY, USA (2015)

    Google Scholar 

  3. Bobot, F., Conchon, S., Contejean, E., Iguernlala, M., Lescuyer, S., Mebsout, A.: Alt-Ergo version 0.99.1. CNRS, Inria, Université Paris-Sud 11, and OCamlPro, Dec 2014. http://alt-ergo.lri.fr/, http://alt-ergo.ocamlpro.com/

  4. ClearSy System Engineering. Atelier B User Manual, version 4.0. http://tools.clearsy.com/wp-content/uploads/sites/8/resources/User_uk.pdf

  5. Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and groundAC completion modulo Shostak theories: design and implementation. Logical Methods Comput. Sci. 8(3), 653–683 (2012)

    Google Scholar 

  6. Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): semantic combination of congruence closure with solvable theories. Electron. Notes Theor. Comput. Sci. 198(2), 51–69 (2008)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  Google Scholar 

  8. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Mentré, D., Marché, C., Filliâtre, J.-C., Asuka, M.: Discharging proof obligations from atelier B using multiple automated provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238–251. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. The \(\sf BWare\) Project (2012). http://bware.lri.fr/

  11. Voisin, L., Abrial, J.-R.: The Rodin platform has turned ten. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 1–8. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI, Université Paris-Sud, 91405, Orsay, France

    Sylvain Conchon & Mohamed Iguernlala

  2. Toccata, INRIA Saclay Ile-de-France, 91893, Orsay, France

    Sylvain Conchon

  3. OCamlPro SAS, 91190, Gif-sur-Yvette, France

    Mohamed Iguernlala

Authors
  1. Sylvain Conchon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamed Iguernlala
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed Iguernlala .

Editor information

Editors and Affiliations

  1. ClearSy, Aix en Provence, France

    Thierry Lecomte

  2. Siemens AG, Braunschweig, Niedersachsen, Germany

    Ralf Pinger

  3. Newcastle University, Newcastle upon Tyne, United Kingdom

    Alexander Romanovsky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Conchon, S., Iguernlala, M. (2016). Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo . In: Lecomte, T., Pinger, R., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2016. Lecture Notes in Computer Science(), vol 9707. Springer, Cham. https://doi.org/10.1007/978-3-319-33951-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33951-1_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33950-4

  • Online ISBN: 978-3-319-33951-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation