see also the index (by topic, by tool, by reference, by year)
ProofInUse joint laboratory
http://www.spark-2014.org/proofinuse
ProofInUse is joint laboratory between Toccata and SME AdaCore. Its goal is to provide verification tools, based on mathematical proof, to industry users.
- A Formal Proof of a Unix Path Resolution Algorithm
- A challenge related to the Esterel Compiler
- Abstract models and refinement in SPARK: allocators example
- Cartesian Trees (from VerifyThis 2019) in SPARK
- Computation of the trajectory of an object submitted to gravity
- Counting bits in a bit vector
- Euler Project problem 11, SPARK/Ada version
- Longest common prefix, in SPARK
- Queues, in SPARK
- Red-Black Trees in SPARK
- The BitWalker, SPARK version
- The BitWalker, Why3 version
- The N-queens problem, using bit vectors
- The rightmost bit trick
see also the index (by topic, by tool, by reference, by year)