Invited Speakers at FMICS 2024
Byron Cook
The keynote of Byron is shared with the Industry Day of FM.
Title: The Business of Proof
Abstract
With only a few niche exceptions, the software industry had not previously figured out how to make deep use of formal mechanical reasoning based on mathematical logic.
At Amazon we have recently seen tremendous adoption of the approach by product groups, with a variety of customer-facing launches that use automated reasoning, and numerous internal proof projects.
This talk describes those projects, and tries explain what went well at Amazon.
The talk also describes challenges that we face to scale the approach to the next level.
About Byron Cook
Byron Cook is Professor of Computer Science at University College London (UCL); as well as Vice President and Distinguished Scientist at Amazon Web Services (AWS).
Byron has worked in a variety of areas over the years, including computer and network security, program analysis and verification, programming languages, theorem proving, hardware design, operating systems, and biological systems.
Thierry Lecomte
Title: B+ or how to model system properties in a formal software model
Abstract
Software development for mission-critical applications requires a level of confidence that can be achieved through the use of formal methods. For a number of industrial applications, there is a lack of high-level properties to be verified, and proof mainly replaces unit testing.
This talk presents an integrated approach based on more than 20 years of industrial practice, which enables so-called "system" properties to be modelled in a formal software model. The proof of the system's safety is not carried out entirely formally, but it is entirely guided by the model. It is based on 2 principles which are illustrated by means of a demonstrative example.
About Thierry Lecomte
With 30 years of experience in R&D, Thierry Lecomte has worked on industrial projects in the automotive, healthcare, microelectronics, nuclear energy, railway and space industries. Today he is R&D director of CLEARSY, a French SME specialized in the invention of safety critical systems, where he has worked since its creation in 2001. His current subjects of interest are safety and security co-engineering, safe artificial intelligence, and autonomous mobility - all related to formal methods.
Back to the FMICS 2024 main page
Last updated on 2024/05/13 17:03:48