Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Field |
|---|---|---|
2016 | arXiv: Software Engineering | Set theory,Notation,Programming language,Computer science,Correctness,Theoretical computer science,Schematic,Mathematical proof,Syntax,Gas meter prover,Model refactoring |
DocType | Volume | Citations |
Journal | abs/1611.02923 | 0 |
PageRank | References | Authors |
0.34 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paulius Stankaitis | 1 | 0 | 1.01 |
| Alexei Iliasov | 2 | 156 | 20.98 |
| David Adjepon-Yamoah | 3 | 0 | 0.34 |
| Alexander B. Romanovsky | 4 | 386 | 41.97 |