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.

Why3 source code: browse / download
proof details

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:

baint32.h: browse / download
baint32.c: browse / download
bfstring.h: browse / download
bfstring.c: browse / download
client.c: browse / download