Program

MoDeVVa will take place on October 3rd in Västerås, Sweden.

231007_Gamine-MoDeVVa_Keynote.pdf

Keynote Speaker: Prof. Ciprian TEODOROV (Lab-STICC, ENSTA Bretagne)

The Boundary Between Executable Specification Languages and Behavior Analysis Tools


The formal verification community strives to prove the correctness of a specification using formal logic and mathematical proofs. The tremendous progress in computer-aided formal verification tools, along with an ever-growing number of success stories renders these methods essential in the system designer toolbox. However, with the advent of domain-specific models and languages, many formalisms are proposed for writing dynamic system specifications, each one adapted to the specific needs of the targeted domain. A new question emerges: How to bridge the gap between these domain-specific formalisms, geared toward domain experts, and the formal verification tools, geared towards mathematicians?


One of the answers, ubiquitous in the literature, relies on using model transformations to translate the domain-specific model to the verification model syntactically. We argue that this approach is counterproductive leading to semantic multiplication, which requires equivalence proofs that can be hard to provide and maintain. In the talk, I will present a new semantic-level answer developed, refined, and evaluated during the last 10 years. The core building block of this approach is a language-agnostic semantic-level interface, which acts as a bridge between the dynamic semantics of a domain-specific language and the behavior analysis tools.


Short bio: Ciprian Teodorov is full professor at ENSTA Bretagne in Brest, France. Ciprian is a member of the Processes for Safe and Secure Software and Systems (P4S) team of the Lab-STICC Laboratory. His main research interests are the industrialization of formal verification techniques for complex system validation. Ciprian leads the OBP2 Semantic Diagnosis & Formal Verification research team. Since 2013, Ciprian focused on the design of a compositional software architecture that eases the creation of domain-specific verification tools. In 2023, Ciprian received the habilitation (HDR) from the University Western Brittany, Brest, France. In the past, he worked as an EDA/CAD Software engineer at Dolphin Integration (now Dolphin Design) in Meylan, France. Ciprian received his Ph.D. in Computer Science from the University of Western Brittany in 2011, for his work on model-driven physical design for emerging computing architectures.

Full-day detailed program

8:45 - 10:00 : Welcome and Keynote Talk 

10:00 - 10:30 : Break                    

10:30 - 12:00 : Session 1. Chair: Jérôme Hugues

12:00 - 13:30 : Lunch Break

13:30 - 15:00 : Session 2. Chair: Dominique Blouin

15:00 - 15:30 : Break

15:30 - 17:00 : Session 3. Chair: Iulian Ober