Automatic Verification for a Class of Proof Obligations with SMT-Solvers

David Déharbe
Digital Printed Abstract View Cite
Type
Conference paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

Abstract

Software development in B and Event-B generates proof obligations that have to be discharged using theorem provers. The cost of such developments therefore depends directly on the degree of automation and efficiency of theorem proving techniques for the logics in which these lemmas are expressed. This paper presents and formalizes an approach to transform a class of proof obligations generated in the Rodin platform in a language that can be addressed by state-of-the-art SMT solvers. The work presented in the paper handles proof obligations with Booleans, integer arithmetics and basic sets.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Deharbe10,
  author       = {David D{\'{e}}harbe},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Automatic Verification for a Class of Proof Obligations with SMT-Solvers},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {217--230},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_17},
  doi          = {10.1007/978-3-642-11811-1\_17},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Deharbe10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related