Formal methods at Thales Research & Technology

Speakers: Delphine Longuet, Nikolai Kosmatov and Romain Soulat from THALES Research & Technology
Tuesday 11 January 2022, 11:00, (online)

Abstract: Formal methods adoption in Thales teams is often led by developments and experiments at the research center. Over the years, we worked on a wide variety of formal methods techniques and benchmarked a lot of tools from the academia and industry. In this talk, we present three particular past or ongoing projects:

  • the model checking of a real-time distributed algorithm
  • the ongoing development of an automated test generation tool suite for Ada
  • the formal verification of a JavaCard virtual machine with Frama-C.

Through those three projects, we present an illustrative selection of the job done at the research center by our team in the last few years.