CRASH Methodology for Correct-by-construction Attack-tolerant Systems

...

Background

Our method relies on using EventML. EventML cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements. More about EventML is at http://www.nuprl.org/software/. For and for additional examples see the EventML Tutorial

...