FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024
Mon 15 Apr 2024 12:00 - 12:30 at Eugénio de Andrade - Theorem proving and applications Chair(s): Claire Dross

Smart cyber agents play a crucial role in software-intensive systems by monitoring their physical surroundings and making impactful decisions. This paper addresses the challenge of specifying multi-agent patterns, which include interactions with human agents in possibly safety-critical environments. To this end, we introduce the foundations of a domain-agnostic and flexible Domain-Specific Language (DSL) called LIrAs. The language is designed to be accessible to users without programming expertise. LIrAs’ semantics are mapped to Deterministic Finite-state Automata, making specifications amenable to formal verification. The DSL is exemplified through an illustrative scenario from the service robotics field.

Mon 15 Apr

Displayed time zone: Lisbon change

11:00 - 12:30
Theorem proving and applicationsFormaliSE 2024 at Eugénio de Andrade
Chair(s): Claire Dross AdaCore
11:00
30m
Talk
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification
FormaliSE 2024
Louis Gauthier Université Paris-Saclay, CEA, List, Virgile Prevosto Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
11:30
30m
Talk
Formally Verified Interval Arithmetic and Its Application to Program Verification
FormaliSE 2024
Achim D. Brucker University of Exeter, Teddy Cameron-Burke University of Exeter, Amy Stell University of Exeter
12:00
30m
Talk
Towards Verifiable Multi-Agent Interaction Pattern Specification
FormaliSE 2024
Alberto Tagliaferro Politecnico di Milano, Italy, Livia Lestingi DEIB, Politecnico di Milano, Matteo Rossi Politecnico di Milano