Sciweavers

FROCOS
2011
Springer
12 years 4 months ago
Automatic Proof and Disproof in Isabelle/HOL
Abstract. Isabelle/HOL is a popular interactive theorem prover based on higherorder logic. It owes its success to its ease of use and powerful automation. Much of the automation is...
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias...
FAC
2008
107views more  FAC 2008»
13 years 4 months ago
An incremental development of the Mondex system in Event-B
A development of the Mondex system was undertaken using Event-B and its associated proof tools. mental approach was used whereby the refinement between the abstract specification o...
Michael Butler, Divakar Yadav