Output details
11 - Computer Science and Informatics
University of York
Article title
Mechanising Mondex with Z/Eves
Type
D - Journal article
Title of journal
Formal Aspects of Computing
Article number
-
Volume number
20
Issue number
1
First page of article
117
ISSN of journal
0934-5043
Year of publication
2008
Number of additional authors
1
Additional information
<07>Originality: This paper reports the first major activity in the Verified Software Initiative (VSI). It demonstrates that industrial-scale verification to ITSEC L6 is clearly within the state of the art; and there is little real difference between apparently different formal methods and tools. Rigour: The work was carried out using the Z/Eves theorem prover, and is repeatable: all scripts are publicly available. Significance: Mondex is now a benchmark problem for theorem provers and model checkers. The paper is in a dedicated journal issue with six other attempts at the same problem and has inspired the list of VSI challenge problems.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - High Integrity Systems Engineering
Citation count
12
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
