Showing 1–2 of 2 results for author: Burdy, L

Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"

Authors: Lilian Burdy, David Déharbe, Étienne Prun

Abstract: The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically. Consequently, such proof obligations are often cluttered with information that is irrelevant to establish their validity. We present iapa, an "Interface to Autom… ▽ More The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically. Consequently, such proof obligations are often cluttered with information that is irrelevant to establish their validity. We present iapa, an "Interface to Automatic Proof Agents", a new tool that is being integrated to Atelier~B, through which the user will access proof obligations, apply operations to simplify these proof obligations, and then dispatch the resulting, simplified, proof obligations to a portfolio of automatic theorem provers. △ Less

Submitted 29 January, 2017; originally announced January 2017.

Comments: In Proceedings F-IDE 2016, arXiv:1701.07925

ACM Class: D.2.4; D.2.2

Journal ref: EPTCS 240, 2017, pp. 82-90

Formally Checking Large Data Sets in the Railways

Authors: Thierry Lecomte, Lilian Burdy, Michael Leuschel

Abstract: This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker. This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker. △ Less

Submitted 25 October, 2012; v1 submitted 25 October, 2012; originally announced October 2012.

Comments: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in develo** dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012