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

## Frama-C

Frama-C is an open environment for static analysis of C source code, annotated in ACSL

- 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
- Floating-point square root using Newton iteration
- 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)