Revision as of 11:44, 27 March 2015 by Sighireanu
- ACSL by Example initiative for providing formal specification of C algorithms and containers.
- ProofInUse project is a joint laboratory between AdaCore and INRIA.
- SPARK 2014 technology for proves of Ada programs.
- Verifast a a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.