Copilot Related
Copilot Benefits


• Completely open-source (BSD3 license) and extensible.

• Automatically generates constant-time and constant-space C99 code.

• Provides the benefits of high-level functional programming for low-level embedded systems development.


Copilot is a domain-specific, embedded stream language for generating hard real-time C code. Copilot is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.

An application of Copilot is the run-time monitoring of safety and security properties for guidance, navigation, and control (GN&C) systems in UAVs. Copilot monitors integrate with hard real-time GN&C systems, and they generate their own scheduler, obviating the need for an underlying RTOS.

The Copilot system contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom Language.

Copilot is a product of Galois' Cyber-Physical Systems program. Learn more at the Copilot site.


Building an Open-Source Autonomous Quad-Copter from Galois Video on Vimeo.

Collaborate with Us

Licensing - Obtain a license for one of our advanced technologies.

Research & Development - Solve your toughest problems by exploring new approaches with us.

Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.

Let's Work TogetherStart the Conversation >>