With Cláudio Lourenço I am investigating the use of Why3 to verify safety properties of TLA+ specifications (without temporal operators). We have successfuly verified the Paxos consensus algorithm, following Lamport’s refinement of the abstract Voting protocol. We will report on this soon.

An exercise in meta-verification with Why3. This unpublished paper, co-authored with Maria João Frade, is dedicated to our colleague Luís Soares Barbosa, on the occasion of his 60th birthday. With the incresasing importance of program verification, an issue that has been receiving more attention is …

The Way of Harmonious Distributed System Proofs. In this ESOP'22 paper jointly written with Cláudio Belo Lourenço, we study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do …

A Deductive Reasoning Approach for Database Applications using Verification Conditions I. Alam, R. Halder, and J. S. Pinto. Journal of Systems and Software, 175:110903, 2021. Elsevier This paper proposes a comprehensive set of Verification Condition (VCs) generation techniques from database …