14 citations · 26 across the 10 of their papers we have counts for
11 papers
Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
Hubert Garavel
LNT is a modern language for the formal description of concurrent systems. It generalizes traditional process calculi and overcomes their known limitations by incorporating feature…
Formal Modeling and Verification of the Algorand Consensus Protocol in CADP
Andrea Esposito, Francesco P. Rossi, Marco Bernardo +2
Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. In this paper we…
Four Formal Models of IEEE 1394 Link Layer
Hubert Garavel, Bas Luttik
We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model check…
Is CADP an Applicable Formal Method?
Hubert Garavel, Frédéric Lang, Radu Mateescu +1
CADP is a comprehensive toolbox implementing results of concurrency theory. This paper addresses the question, whether CADP qualifies as an applicable formal method, based on the e…
The VLSAT-2 Benchmark Suite
Pierre Bouvier, Hubert Garavel
This report presents VLSAT-2 (an acronym for "Very Large Boolean SATisfiability problems),the second part of a benchmark suite to be used in scientific experiments and softwarecomp…
Proposal for Adding Useful Features to Petri-Net Model Checkers
Hubert Garavel
Solutions proposed for the longstanding problem of automatic decomposition of Petri nets into concurrent processes, as well as methods developed in Grenoble for the automatic conve…
The VLSAT-1 Benchmark Suite
Pierre Bouvier, Hubert Garavel
This report presents VLSAT-1 (an acronym for "Very Large Boolean SATisfiability problems"), the first part of a benchmark suite to be used in scientificexperiments and software com…
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems
Ansgar Fehnker, Hubert Garavel
This volume contains the proceedings of MARS 2020, the fourth workshop on Models for Formal Analysis of Real Systems held as part of ETAPS 2020, the European Joint Conferences on T…
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Hubert Garavel, Lina Marsso
The Message Authenticator Algorithm (MAA) is one of the first cryptographic functions for computing a Message Authentication Code. Between 1987 and 2001, the MAA was adopted in int…
The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark
Hubert Garavel, Wendelin Serwe
The multiway rendezvous introduced in Theoretical CSP is a powerful paradigm to achieve synchronization and communication among a group of (possibly more than two) processes. We il…
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Hubert Garavel, Lina Marsso
We present a term rewrite system that formally models the Message Authenticator Algorithm (MAA), which was one of the first cryptographic functions for computing a Message Authenti…