2016/11/09 by Paulius Stankaitis, Stankaitis, Paulius, Alexei Iliasov +5
Computer Science · #D.2.4 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1611.02923
openalex publication_date 2016/11/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Event-B is one of more popular notations for model-based, proof driven specification. It offers a fairly high-level mathematical lan- guage based on FOL and ZF set theory and an economical yet expres- sive modelling notation. Model correctness is established by discharging proving a number conjectures constructed via a syntactic instantiation of schematic conditions. A large proportion of provable conjectures re- quires proof hints from a user. For larger models this becomes extremely onerous as identical or similar proofs have to be repeated over and over, especially after model refactoring stages. In the paper we briefly present a new Rodin Platform proof back-end based on the Why3 umbrella prover.