- John Rushby & Friedrich von Henke
- Formal Verification of Algorithms for Critical Systems
- ACM SIGSOFT'91 Conf on Software for Critical Systems: Software Eng Notes V16n5(Dec 1991)pp1-15, republished IEEE Trans SE-19n1(Jan 1993)pp13-23
- =EXPERIENCE PROOF CHECKER LOGIC EHDM Z
- EHDM - the "implacable sceptic"
- need for a proof checker with library of reusable theories including both discrete and concrete mathematics - the "implacable sceptic" forcing you to express all assumptions, found errors in published work, typos in Z specification, corrected and simplified publishable proof of a complex real time algorithm, able to rapidly do 'what ifs', productive symbiosis, tools: editor, parser, typechecker, browesers, cross-referenceers,...typographical output, a sort of module structure for specifications, first order logic with a fragment of higher order logic (functions of functions), 19 axioms and 200 proofs
ICA problem as a challenge

Need reusable library of theories

Need a type theory which distinguishes similar algebras like velocity vs length or real time vs clock time.

- need for a proof checker with library of reusable theories including both discrete and concrete mathematics - the "implacable sceptic" forcing you to express all assumptions, found errors in published work, typos in Z specification, corrected and simplified publishable proof of a complex real time algorithm, able to rapidly do 'what ifs', productive symbiosis, tools: editor, parser, typechecker, browesers, cross-referenceers,...typographical output, a sort of module structure for specifications, first order logic with a fragment of higher order logic (functions of functions), 19 axioms and 200 proofs

Search for bibliographic items containing a matching string.

Search for a specific bibliographic item by name.

To see the complete bibliography (1Mb+) select:[Bibliography]