Difference between revisions of "Related Projects"
From vecolib
Sighireanu (Talk | contribs) (Created page with "* [http://www.spark-2014.org/proofinuse ProofInUse] laboratory. * [http://www.spark-2014.org/ SPARK 2014] technology for proves of Ada programs. * [http://people.cs.kuleuven.b...") |
Sighireanu (Talk | contribs) |
||
| Line 1: | Line 1: | ||
| − | * [http://www.spark-2014.org/proofinuse ProofInUse] laboratory. | + | * [http://www.spark-2014.org/proofinuse ProofInUse] project is a joint laboratory between AdaCore and INRIA. |
* [http://www.spark-2014.org/ SPARK 2014] technology for proves of Ada programs. | * [http://www.spark-2014.org/ SPARK 2014] technology for proves of Ada programs. | ||
* [http://people.cs.kuleuven.be/~bart.jacobs/verifast/ Verifast] a a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. | * [http://people.cs.kuleuven.be/~bart.jacobs/verifast/ Verifast] a a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. | ||
Revision as of 12:25, 27 March 2015
- 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.
