Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Fri 23 Aug 2019 14:16 - 14:40 at Elk - Compilers Chair(s): Jose Calderon

Ultra-critical systems require high level assurance, which cannot always be guaranteed at compile time. The use of runtime verification (RV) allows us to monitor these systems at runtime, detect property violations early, and limit the potential consequences of these errors. Copilot is a stream based high-level EDSL in Haskell to define monitors, it has support for different Temporal Logics (TL), and compiles to hard realtime C99 code specifically suited for embedded systems.

Although simple in its design, and relying on known techniques for EDSL implementation, Copilot is unique due to its domain of application: it is used by NASA researchers to monitor properties of Unmanned Aerial Vehicles for the purposes of verification and validation. The goal of Copilot is to provide a language that is guaranteed to compile to correct C code, targeted at people with minimal knowledge of Haskell.

In this talk we will discuss the internals of Copilot 3.0 and some of the obstacles that currently limits its use. In particular:

  • We will explain how support for structs and arrays is implemented, using type-level programming to provide compile-time guarantees and make generation of C code possible.

  • We will demonstrate how Copilot generates hard realtime C99, how memory consumption is known in advance, and the constraints that imposes in our EDSL.

Current obstacles, especially for our target audience, include:

  • Error messages are harder to understand, in part due to the use of dependent types, as well as due to the way two-stage compilation of EDSL’s is done.

  • The current implementation sometimes requires additional boilerplate to be defined by users, especially when they use structs.

Website: https://copilot-language.github.io

Fri 23 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
CompilersHIW at Elk
Chair(s): Jose Calderon Galois, Inc.
Status Update on the Helium for Haskell compiler
Jurriaan Hage Utrecht University, Netherlands
The Gibbon Compiler: Accelerating a small subset of Haskell
Ryan R. Newton Indiana University, Michael Vollmer Indiana University, USA, Chaitanya Koparkar Indiana University
Copilot 3.0: a Haskell runtime verification framework for UAVs
Frank Dedden Royal Netherlands Aerospace Center, Alwyn Goodloe NASA Langley Research Center, Ivan Perez NIA / NASA Formal Methods
Lightning talks Slot #2