[Haskell-cafe] [Announcement] Copilot 3.1, hard realtime C generator and runtime verification framework

[Ivan Perez]

Dear all,

We are very pleased to announce the release of Copilot 3.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.

This new release contains a number of bug fixes and simplifications:

* The installation instructions have been updated to work with new versions
of cabal and GHC.

* Random stream generators were not being used and have been removed.

* External functions are no longer supported by the language (to prevent
side-effects in streams).

* Minor bug related to labels, nested locals, and pretty printing Copilot
core, have been fixed.

* Code internals have been simplified for a more future proof codebase.

Copilot 3.1 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 providing better documentation, facilitating the use
with other systems, and generally improving the codebase. Users are
encouraged to participate by opening issues and asking questions via our
github repo [3].

Kind regards,

The Copilot developers:

- Frank Dedden (maintainer)
- Alwyn Goodloe (maintainer)
- Ivan Perez (maintainer)

[1] http://hackage.haskell.org/package/copilot
[2] https://copilot-language.github.io
[3] https://github.com/Copilot-Language/copilot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191127/efc50af8/attachment.html>