[Haskell-cafe] [ANN] Copilot 3.2.1 - hard realtime C runtime verification

[Frank Dedden]

Dear all,

We are very pleased to announce the release of Copilot 3.2.1, a stream-based
DSL for writing and monitoring embedded C programs, with an emphasis on
correctness and hard realtime requirements. Copilot is typically used as a
high-level runtime verification framework, and supports temporal logic (LTL,
PTLTL and MTL), clocks and voting algorithms.

Among others, Copilot has been used at the Safety Critical Avionics Systems
Branch of NASA Langley Research Center for monitoring test flights of drones.

In collaboration with the development team at Galois, Inc., the new release
introduces a backend to their What4 solver frontend. With this addition, it is
now possible to prove properties of Copilot specifications using What4 [4]. We
thank Galois for their help and their contribution.

The second big focus of this release was the documentation: the public API
documentation has been improved and completed.

Additionally, several small improvements and fixes are made in the C99 code
generator.

The newest release is available on hackage [1]. For more information,
including documentation, examples and links to the source code, please visit
the webpage [2].

Current emphasis is on facilitating the use with other systems, and improving
the codebase in terms of stability and test coverage. Users are encouraged to
participate by opening issues and asking questions via our github repo [3].

Kind regards,

The Copilot developers:

- Frank Dedden
- Alwyn Goodloe
- Ivan Perez

[1] http://hackage.haskell.org/package/copilot
[2] https://copilot-language.github.io
[3] https://github.com/Copilot-Language/copilot
[4] https://github.com/GaloisInc/what4