14 citations
- Centre Inria de l'Université Grenoble AlpesFR2 papers
- Institut national de recherche en sciences et technologies du numériqueFR2 papers
- Laboratoire d'Informatique de GrenobleFR2 papers
- Université Grenoble AlpesFR2 papers
- Canada Research ChairsCA1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- Institut polytechnique de GrenobleFR1 paper
- University of TorontoCA1 paper
- University of TriesteIT1 paper
- University of UrbinoIT1 paper
5 papers
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…
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
Lina Marsso, Radu Mateescu, Lucie Muller +1
We present two behavioral models of an autonomous vehicle and its interaction with the environment. Both models use the formal modeling language LNT provided by the CADP toolbox. T…
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…
Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
Wendelin Serwe
This paper presents two formal models of the Data Encryption Standard (DES), a first using the international standard LOTOS, and a second using the more recent process calculus LNT…
Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems
Frédéric Lang, Radu Mateescu
Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating…