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
- Bitwalker
- Counting bits in a bit vector
- Euler Project problem 11, SPARK/Ada version
- The N-queens problem, using bit vectors
- The rightmost bit trick

see also the index (by topic, by tool, by reference, by year)