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) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | * [http://www.spark-2014.org/proofinuse ProofInUse] laboratory. | + | * [http://www.fokus.fraunhofer.de/download/acsl_by_example ACSL by Example] initiative for providing formal specification of C algorithms and containers. |
| + | * [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. | ||
Latest revision as of 11:44, 27 March 2015
- 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.
