see also the index (by topic, by tool, by reference, by year)
Claude Marché
https://marche.gitlabpages.inria.fr/home/
- A Formal Proof of a Unix Path Resolution Algorithm
- A Formally Verified Symbolic Interpreter for a IMP language
- A Sudoku solver
- A challenge related to the Esterel Compiler
- A toy variant of Fibonacci function
- Accuracy of Log-Sum-Exp
- Approximated Cosine in C annotated in ACSL
- Approximated Cosine in Why3
- Approximated Cosine, exact values and rounding errors
- Binary Heaps in Why3
- Binary Search, Java version
- Binary Search, SPARK/Ada version
- Binary search in C annotated in ACSL
- Bubble sort
- Counting bits in a bit vector
- Dijkstra's Dutch Flag, Java version
- Drift of a clock using floating-point numbers
- Edition distance
- Fast exponentiation
- Fibonacci function, linear/logarithmic algorithms, Why3 version
- Fibonacci sequence, linear algorithm, Java version
- Filter elements of an array
- FoVeOOS'11 Competition: challenge 1, in C
- FoVeOOS'11 Competition: challenge 1, in Java
- FoVeOOS'11 Competition: challenge 1, in Why3
- FoVeOOS'11 Competition: challenge 2, in C
- FoVeOOS'11 Competition: challenge 2, in Java
- FoVeOOS'11 Competition: challenge 3, in C
- FoVeOOS'11 Competition: challenge 3, in Java
- Greatest Common Divisor, Bezout coefficients, Java version
- Greatest common divisor, using the Euclidean algorithm
- In-Place Linked-List Reversal in Why3
- Insertion Sort, C version
- Integer square root
- Integer square root on machine integers
- Iterated quaternion multiplication
- McCarthy 91 function, Java version
- Regular expression matching using residuals
- Scalar product of vectors using floating-point numbers
- Schorr-Waite algorithm, proof using a ghost monitor
- Selection Sort, C version
- Selection Sort, Java version
- Simple Electronic Purse, Java version
- Sparse Arrays in Capucine
- Sum of even-valued Fibonacci numbers
- Sum of multiples of 3 and 5
- Sum of values in an array, C version
- Sum queries
- Summing the elements of a list
- The BitWalker, SPARK version
- The BitWalker, Why3 version
- The N-queens problem, using bit vectors
- The rightmost bit trick
- Toy compiler
- VSCOMP 2014, problem 1
- Variations on Semantics of Programming Languages
- Various programs computing the factorial, in Why3
- VerifyThis @ FM 2012, problem 1
- VerifyThis @ FM 2012, problem 2
- WP revisited in Why3
see also the index (by topic, by tool, by reference, by year)