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:
- Write the secification specification in EventML
- Automatically generate and prove an Inductive Logical Form of the specification
- Synthesize code
- Diversify and deploy code
...