Skip to main content
SpringerLink
Log in

Soundly Proving B Method Formulæ Using Typed Sequent Calculus

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2016 (ICTAC 2016)

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

Included in the following conference series:

Abstract

The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulæ expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulæ into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulæ in the B proof system.

This work is supported by the BWare project (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).

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

References

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

    Book  MATH  Google Scholar 

  2. Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493–507. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_34

    Chapter  Google Scholar 

  3. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (Boogie) (2011)

    Google Scholar 

  4. Bodeveix, J.-P., Filali, M.: Type synthesis in B and the translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 350–369. Springer, Heidelberg (2002). doi:10.1007/3-540-45648-1_18

    Chapter  Google Scholar 

  5. Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \varPi \)-calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving (PxTP) (2012)

    Google Scholar 

  6. 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). doi:10.1007/978-3-540-75560-9_13

    Chapter  Google Scholar 

  7. Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. In: LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Suva, Fiji (2015)

    Google Scholar 

  8. Cauderlier, R., Halmagrand, P.: Checking Zenon modulo proofs in Dedukti. In: Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Berlin, Germany (2015)

    Google Scholar 

  9. Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 274–290. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_20

    Chapter  Google Scholar 

  10. Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The Bware project: building a proof platform for the automated verification of B proof obligations. In: Ameur, Y.A., Schewe, K.-S. (eds.) Abstract State Machines, Alloy, B, VDM, and Z (ABZ). LNCS, vol. 8477, pp. 290–293. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  11. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving Modulo. J. Autom. Reasoning (JAR) 31, 33–72 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Dowek, G., Miquel, A.: Cut elimination for zermelo set theory. Archive for Mathematical Logic. Springer, Heidelberg (2007, submitted)

    Google Scholar 

  13. Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Verifying B proof rules using deep embedding and automated theorem proving. Softw. Eng. Formal Methods 7041, 253–268 (2011)

    Article  MATH  Google Scholar 

  14. Jaeger, É., Dubois, C.: Why would you trust B? In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 288–302. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75560-9_22

    Chapter  Google Scholar 

  15. Kleene, S.C.: Permutability of inferences in Gentzens calculi LK and LJ. In: Bulletin Of The American Mathematical Society, vol. 57, pp. 485–485. Amer Mathematical Soc, Providence (1951)

    Google Scholar 

  16. 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). doi:10.1007/978-3-642-30885-7_17

    Chapter  Google Scholar 

  17. Schmalz, M.: Formalizing the logic of event-B. Ph.D. thesis, Diss., Eidgenössische Technische Hochschule ETH Zürich, Nr. 20516, 2012 (2012)

    Google Scholar 

  18. ClearSy: Atelier B 4.1 (2013). http://www.atelierb.eu/

Download references

Author information

Authors and Affiliations

  1. Cnam/Inria/Ens Cachan, Paris, France

    Pierre Halmagrand

Authors
  1. Pierre Halmagrand
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pierre Halmagrand .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco Centro de Informática, Recife, Pernambuco, Brazil

    Augusto Sampaio

  2. Deptartment of Electrical Engineering BL, National Taiwan University, Taipei, Taiwan

    Farn Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Halmagrand, P. (2016). Soundly Proving B Method Formulæ Using Typed Sequent Calculus. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46750-4_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46749-8

  • Online ISBN: 978-3-319-46750-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation