research
∙
02/02/2023
A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)
Algebraic effects and handlers are a powerful abstraction to build non-l...
share
research
∙
12/05/2022
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification,...
research
∙
07/20/2022
Auto-active Verification of Graph Algorithms, Written in OCaml
Functional programming offers the perfect ground for building correct-by...
research
∙
04/22/2021
Cameleer: a Deductive Verification Tool for OCaml
OCaml is particularly well-fitted for formal verification. On one hand, ...
research
∙
03/08/2021
A coordination-free, convergent, and safe replicated tree
The tree is an essential data structure in many applications. In a distr...
research
∙
10/13/2020
CISE3: Verifying Weakly Consistent Applications with Why3
In this paper we present a tool for the formal analysis of applications ...
research
∙
05/29/2020
WhylSon: Proving your Michelson Smart Contracts in Why3
This paper introduces WhylSon, a deductive verification tool for smart c...
research
∙
03/11/2020
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
We present an approach to obtain formally verified implementations of cl...
research
∙
09/09/2019
CISE3: Verificação de aplicações com consistência fraca em Why3
In this article we present a tool for the verification of programs built...
research
∙
05/20/2019