research
∙
09/11/2023
Sound Atomicity Inference for Data-Centric Synchronization
Data-Centric Concurrency Control (DCCC) shifts the reasoning about concu...
share
research
∙
12/30/2022
Anticipation of Method Execution in Mixed Consistency Systems – Technical Report
Distributed applications often deal with data with different consistency...
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
∙
09/12/2022
On using VeriFast, VerCors, Plural, and KeY to check object usage
Typestates are a notion of behavioral types that describe protocols for ...
research
∙
04/22/2021
Cameleer: a Deductive Verification Tool for OCaml
OCaml is particularly well-fitted for formal verification. On one hand, ...
research
∙
09/17/2020
Typestates to Automata and back: a tool
Development of software is an iterative process. Graphical tools to repr...
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
∙
02/28/2020
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
We present a type-based analysis ensuring memory safety and object proto...
research
∙
09/13/2018
A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm
We present a recursive formulation of the Horn algorithm for deciding th...
research
∙
07/20/2018
Uma análise comparativa de ferramentas de análise estática para deteção de erros de memória
— Portuguese version As falhas de software estão com frequência associ...
research
∙
12/05/2017