Programming Languages for High-Assurance Autonomous Vehicles

Presented as part of the 2014 HCSS conference.

Abstract:

I will discuss how, in just 1.5 years, Galois built two new domain-specific languages (DSLs) and used them to develop a “hack-proof", full-featured unpiloted air system.  The secret to our increased productivity and assurance was building embedded DSLs, in which the DSLs are libraries in Haskell.  We generate embedded C code that is guaranteed to be memory-safe from a relatively small specification.

The autopilot and more information is available at smaccmpilot.org.

Speaker Bio:

Lee Pike manages the Cyber-Physical Systems program at Galois, Inc., a company specializing in software-intensive critical systems. He has been the PI on approximately $10 million of R&D projects funded by NASA, DARPA, and other federal agencies. His research focuses on applying techniques from functional programming, run-time verification, and formal verification to the areas of operating systems, compilers, cryptographic systems, avionics, and control systems. Previously, he was a research scientist in the NASA Langley Formal Methods Group and has a Ph.D in Computer Science from Indiana University.