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

EventML

Our method relies on using
http://newsite.nuprl.org/software/

To create correct-by-construction code we:

1. Write the secification specification in EventML
   Image Removed
2. Automatically generate and prove an Inductive Logical Form of the specification
3. Synthesize code
4. Diversify and deploy code

...