Abstraction and Genericity in Why3

These are the Why3 source files for the verified programs described in the paper Abstraction and Genericity in Why3 (Jean-Christophe FilliĆ¢tre, Andrei Paskevich, 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 12476 of Lecture Notes in Computer Science, Rhodes, Greece, October 2020. Springer.).

These proofs were prepared using Why3 version 1.3.1.

C code is obtained with the following commands:
  why3 extract -D c -L . --recursive --modular --interface code.BAint32  -o dir
  why3 extract -D c -L . --recursive --modular --interface code.BFstring -o dir
  why3 extract -D c -L . --recursive --modular --interface code.Client   -o dir
Here are the resulting files: