NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


Michael Wagner, CMU



Formal methods for the informal world

Abstract: For good reason, the use of formal methods is demanded for high-integrity applications. However, in many other safety-relevant applications, developers stand to benefit from formal methods but usually don't. Partially this is because of a lack of developers familiar with formal methods, but in this talk I'd like to address another reason: developers often don't know really what they're trying to build. Developers' models of how customers will interact with their product, of conditions present in the environment, and of important failure modes can be overly simplistic and often wrong. In my experience, when building a novel sort of system, such as an autonomous vehicle, implementation and specification are intertwined; and each only matures after progress on the other. In this talk, I will present my perspective on how formal methods could serve these developers

General Chair

Misty Davies
(NASA Ames)

Program Chairs

Clark Barrett
(Stanford University)

Temesghen Kahsai
(NASA Ames / CMU)

Local organization

Guy Katz
(Stanford University)

Rody Kersten
(CMU Silicon Valley)

Program Committee

Aarti Gupta (Princeton)
Alberto Griggio (FBK-IRST)
Alessandro Cimatti (FBK-IRST)
Alwyn Goodloe (NASA Langley)
Arie Gurfinkel (University of Waterloo)
Cesare Tinelli (University of Iowa)
Christoph Torens (German Aerospace Center)
Daniel Kroening (University of Oxford)
Dejan Jovanović (SRI)
Dino Distefano (Facebook)
Dirk Beyer (LMU Munich)
Domagoj Babic (Google)
Ella Atkins (University of Michigan)
Eric Feron (Georgia Tech)
Ewen Denney (SGT / NASA Ames)
Gerwin Klein (NICTA and UNSW)
John Harrison (Intel)
John Rushby (SRI)
Jorge Navas (SRI)
Julia Badger (NASA)
Kalou Cabrera Castillos (LAAS-CNRS)
Kelly Hayhurst (NASA)
Kirstie L. Bellman (The Aerospace Corporation)
Klaus Havelund (NASA JPL)
Kristin Yvonne Rozier (Iowa State University)
Lael Rudd (Draper)
Lee Pike (Galois)
Martin Schäf (SRI)
Mats Heimdahl (University of Minnesota)
Meeko Oishi (University of New Mexico)
Mike Hinchey (Lero-the Irish Software Engineering Research Centre)
Michael Lowry (NASA Ames)
Murali Rangarajan (Boeing)
Natasha Neogi (NASA Langley)
Neha Rungta (AWS)
Nikolaj Bjorner (Microsoft Research)
Patrice Godefroid (Microsoft Research)
Philipp Ruemmer (Uppsala University)
Pierre-Loïc Garoche (ONERA)
Rajeev Joshi (NASA JPL)
Sriram Sankaranarayanan (University of Colorado Boulder)
Susmit Jha (United Technologies)
Virginie Wiels (ONERA)
Wenchao Li (Boston University)
Zvonimir Rakamaric (University of Utah)

First Gov logo
NASA Logo - nasa.gov