Sciweavers

Share
ASM
2010
ASM

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

9 years 10 months ago
Automatic Verification for a Class of Proof Obligations with SMT-Solvers
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.
David Déharbe
Added 29 Sep 2010
Updated 29 Sep 2010
Type Conference
Year 2010
Where ASM
Authors David Déharbe
Comments (0)
books