see also the index (by topic, by tool, by reference, by year)
Jessie
http://www.frama-c.com/jessie.html
Jessie is a deductive verification plug-in of Frama-C, using Why as back-end
- Accurate discriminant
- Approximated Cosine in C annotated in ACSL
- Approximated Cosine, exact values and rounding errors
- Area of a triangle
- Binary search in C annotated in ACSL
- Discretization of the 1D acoustic wave equation
- Drift of a clock using floating-point numbers
- Exact subtraction: Sterbenz's theorem
- FoVeOOS'11 Competition: challenge 1, in C
- FoVeOOS'11 Competition: challenge 2, in C
- FoVeOOS'11 Competition: challenge 3, in C
- Insertion Sort, C version
- Iterated quaternion multiplication
- KB3D: an avionics example
- Linear recurrence of order 2
- Malcolm algorithm to determine the radix
- Scalar product of vectors using floating-point numbers
- Selection Sort, C version
- Sum of values in an array, C version
- Veltkamp/Dekker algorithm
see also the index (by topic, by tool, by reference, by year)