Jean-Christophe Filliâtre

Clément Pascutto

Proceedings of the Runtime Verification - 22nd International Conference, 2022

2021

Simpler proofs with decentralized invariants.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2021

Ortac: Runtime Assertion Checking for OCaml (Tool Paper).

[BibT_eX]

[DOI]

Clément Pascutto

Proceedings of the Runtime Verification - 21st International Conference, 2021

2020

Abstraction and Genericity in Why3.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

2019

GOSPEL - Providing OCaml with a Formal Specification Language.

[BibT_eX]

[DOI]

Arthur Charguéraud

Cláudio Lourenço

Mário Pereira

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2016

The spirit of ghost code.

[BibT_eX]

[DOI]

Léon Gondelman

Formal Methods Syst. Des., 2016

Producing All Ideals of a Forest, Formally (Verification Pearl).

[BibT_eX]

[DOI]

Mário Pereira

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2016

A Modular Way to Reason About Iteration.

[BibT_eX]

[DOI]

Mário Pereira

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

2015

Let's verify this with Why3.

[BibT_eX]

[DOI]

François Bobot

Int. J. Softw. Tools Technol. Transf., 2015

How to Avoid Proving the Absence of Integer Overflows.

[BibT_eX]

[DOI]

Martin Clochard

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

2014

CAOVerif: An open-source deductive verification platform for cryptographic software implementations.

[BibT_eX]

[DOI]

José Bacelar Almeida

Manuel Barbosa

Jorge Sousa Pinto

Bárbara Vieira

Sci. Comput. Program., 2014

Trusting computations: A mechanized proof from partial differential equations to actual program.

[BibT_eX]

[DOI]

Comput. Math. Appl., 2014

Formalizing Semantics with an Automatic Program Verifier.

[BibT_eX]

[DOI]

Martin Clochard

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

2013

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Preserving User Proofs across Specification Changes.

[BibT_eX]

[DOI]

François Bobot

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Why3 - Where Programs Meet Provers.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2013

One Logic to Use Them All.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Verifying Two Lines of C with Why3: An Exercise in Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Separation Predicates: A Taste of Separation Logic in First-Order Logic.

[BibT_eX]

[DOI]

François Bobot

Proceedings of the Formal Methods and Software Engineering, 2012

The 2nd Verified Software Competition: Experience Report.

[BibT_eX]

[DOI]

Aaron Stump

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers.

[BibT_eX]

[DOI]

David Mentré

Masashi Asuka

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

2011

Deductive software verification.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2011

Real-Time Monitoring of Ocaml programs.

[BibT_eX]

[DOI]

Fabrice Le Fessant

Julien Robert

Guillaume Von Tokarski

Stud. Inform. Univ., 2011

Wave Equation Numerical Resolution: Mathematics and Program

[BibT_eX]

[DOI]

CoRR, 2011

Correct Code Containing Containers.

[BibT_eX]

[DOI]

Claire Dross

Yannick Moy

Proceedings of the Tests and Proofs - 5th International Conference, 2011

Functory: A Distributed Computing Library for Objective Caml.

[BibT_eX]

[DOI]

K. Kalyanasundaram

Proceedings of the Trends in Functional Programming, 12th International Symposium, 2011

The COST IC0701 Verification Competition 2011.

[BibT_eX]

[DOI]

Proceedings of the Formal Verification of Object-Oriented Software, 2011

2010

A Deductive Verification Platform for Cryptographic Software.

[BibT_eX]

[DOI]

Manuel Barbosa

Jorge Sousa Pinto

Bárbara Vieira

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Formal Proof of a Wave Equation Resolution Scheme: The Method Error.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Faire bonne figure avec MLPOST.

[BibT_eX]

[DOI]

Romain Bardou

Johannes Kanig

Stéphane Lescuyer

Stud. Inform. Univ., 2009

Combining Coq and Gappa for Certifying Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

2008

A functional implementation of the garsia--wachs algorithm: (functional pearl).

[BibT_eX]

[DOI]

Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008, 2008

Semi-persistent Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2008

2007

Formal proof of a program: Find.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

Designing a Generic Graph Library Using ML Functors.

[BibT_eX]

Julien Signoles

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

A persistent union-find data structure.

[BibT_eX]

[DOI]

Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007, 2007

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Formal Verification of Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Computer Arithmetic (ARITH-18 2007), 2007

2006

Type-safe modular hash-consing.

[BibT_eX]

[DOI]

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

Backtracking iterators.

[BibT_eX]

[DOI]

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

2004

Multi-prover Verification of C Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2004

Functors for Proofs and Programs.

[BibT_eX]

[DOI]

Pierre Letouzey

Proceedings of the Programming Languages and Systems, 2004

2003

Producing all ideals of a forest, functionally.

[BibT_eX]

[DOI]

François Pottier

J. Funct. Program., 2003

Verification of non-functional programs using interpretations in type theory.

[BibT_eX]

[DOI]

J. Funct. Program., 2003

2001

ICS: Integrated Canonizer and Solver.

[BibT_eX]

[DOI]

Sam Owre

Harald Rueß

Natarajan Shankar

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

1998

Proof of Imperative Programs in Type Theory.

[BibT_eX]

[DOI]