see also the index (by topic, by tool, by reference, by year)
Ghost code
Examples involving ghost code
- A Formally Verified Interpreter for the Shell-like Language CoLiS
- A Formally Verified Symbolic Interpreter for a IMP language
- A small puzzle involving a Roberval balance
- A toy variant of Fibonacci function
- Abstract models and refinement in SPARK: allocators example
- Algorithm 63 (partition)
- Bellman-Ford algorithm
- Cartesian Trees (from VerifyThis 2019) in SPARK
- Circular queue in an array
- Computing the number of solutions to the N-queens puzzle
- Conjugate of a partition
- Counting bits in a bit vector
- Greatest Common Divisor, Bezout coefficients, Java version
- Greatest common divisor with Bezout coefficients
- In-Place Linked-List Reversal in Why3
- Maximum subarray problem
- Optimal replay
- Pigeonhole principle
- Red-Black Trees in SPARK
- Schorr-Waite algorithm
- Schorr-Waite algorithm, proof using a ghost monitor
- Schorr-Waite algorithm, proof via recursion
- Sum of even-valued Fibonacci numbers
- Sum queries
- The N-queens problem, using bit vectors
- The rightmost bit trick
- Towers of Hanoi
- Unraveling a Card Trick
- VSCOMP 2014, problem 1
- Various ways of proving an induction principle
- VerifyThis @ FM 2012, problem 1
- VerifyThis @ FM 2012, problem 2
- VerifyThis @ FM 2012, problem 3
see also the index (by topic, by tool, by reference, by year)