We manually verified the
old version in Coq (using CFML).
Lemma to_array_old_spec : forall A (l : list A) (s : func), SPEC (to_array s) PRE [Seq l s] POST (fun a => a ~> Array l). Proof using (All). (* .. *) (* .. *) (* .. *) Qed.
Sisyphus was able to automatically repair the proof to work for the new program.
We evaluated Sisyphus on 14 OCaml programs, 10 of which were taken from real-world OCaml libraries (Jane Street's Core, Inria's Menhir, Containers e.t.c.).
Sisyphus's repair procedure builds some of the most elegant truths of Computer Science, the Curry-Howard correspondence, to automatically and efficiently infer invariants for programs.
Sisyphus is built from the ground up using Free (as in freedom) technologies, and is licensed under the ultimate AGPLv3+ libre license to ensure the Freedoms of its users are preserved!
You can learn more about Sisyphus by reading our paper, or try it out using our artefact, or built and extend it from the source code: