Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François
Formal proof and analysis of an incremental cycle detection
Submitted, February 2019.
[ bib |
We exploit Separation Logic with Time Credits to verify
the correctness and worst-case amortized asymptotic complexity of a
state-of-the-art incremental cycle detection algorithm.
Procrastination, a proof engineering technique.
Talk proposal for the FLoC Coq Workshop 2018, April 2018.
[ bib |
We present a small Coq library for collecting side conditions and deferring their proof.
Armaël Guéneau, Arthur Charguéraud, and François Pottier.
A fistful of dollars: Formalizing asymptotic complexity claims via
deductive program verification.
In European Symposium on Programming (ESOP), 2018.
[ bib |
We present a framework for simultaneously verifying the
functional correctness and the worst-case asymptotic time
complexity of higher-order imperative programs. We build on
top of Separation Logic with Time Credits, embedded in an
interactive proof assistant. We formalize the O notation,
which is key to enabling modular specifications and proofs. We
cover the subtleties of the multivariate case, where the
complexity of a program fragment depends on multiple
parameters. We propose a way of integrating complexity bounds
into specifications, present lemmas and tactics that support a
natural reasoning style, and illustrate their use with a
collection of examples.
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish.
Verified characteristic formulae for CakeML.
In European Symposium on Programming (ESOP), 2017.
[ bib |
Characteristic Formulae (CF) offer a productive, principled
approach to generating verification conditions for
higher-order imperative programs, but so far the soundness of
CF has only been considered with respect to an informal
specification of a programming language (OCaml). This leaves a
gap between what is established by the verification framework
and the program that actually runs. We present a
fully-fledged CF framework for the formally specified CakeML
programming language. Our framework extends the existing CF
approach to support exceptions and I/O, thereby covering the
full feature set of CakeML, and comes with a formally verified
soundness theorem. Furthermore, it integrates with existing
proof techniques for verifying CakeML programs. This validates
the CF approach, and allows users to prove end-to-end theorems
for higher-order imperative programs, from specification to
language semantics, within a single theorem prover.
Armaël Guéneau, François Pottier, and Jonathan Protzenko.
The ins and outs of iteration in Mezzo.
Talk proposal for HOPE 2013, July 2013.
[ bib |
This is a talk proposal for HOPE 2013. Using iteration
over a collection as a case study, we wish to
illustrate the strengths and weaknesses of the
prototype programming language Mezzo.