[Haskell-cafe] [ANN] Copilot 3.12

[Ivan Perez]

Dear all,

I'm very excited to announce Copilot 3.12.

Copilot is 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. It also serves as a runtime monitoring backend for the requirements
elicitation tool FRET (https://github.com/NASA-SW-VnV/fret/), via Ogma (
https://github.com/nasa/ogma).

The main changes in this release are as follows:

   - A new library copilot-prettyprinter exposes functions related to the
   Copilot Core pretty-printing backend. Pre-existing functions included as
   part of copilot-core are now deprecated.
   - The C99 backend now produces an additional header file with struct
   declarations. This file is used by the C implementation file generated by
   Copilot to define structs before the declarations of the handlers, avoiding
   potential forward declarations that the C compiler cannot resolve. Users of
   Copilot can choose to import the same new type declaration header file
   before the standard Copilot header file in their hand-written code, or use
   external definitions that declare compatible structs. Note that, in the
   former case, the header file that declares the structs must be included
   before the header file that declares the externs, handlers and step
   function.
   - The custom type equality module in copilot-core is now deprecated in
   favour of the definition of type equality in base.
   - copilot-theorem now includes support for proofs by bisimulation
   necessary for future extensions to Copilot.
   - copilot-core now complies with the coding rules established as part of
   the process of compliance with higher NASA's requirements for software with
   higher assurance classifications.

Current emphasis is on improving the codebase in terms of stability and
test coverage, removing unnecessary dependencies, hiding internal
definitions, and formatting the code to meet our new coding standards.
Users are encouraged to participate by opening issues and asking questions
via our github repo (https://github.com/copilot-language/copilot).

I'd also like to take this opportunity to announce that Copilot is now
available on Debian. As a consequence of this effort, Copilot will also be
available to Ubuntu users in the near future. We would like to publicly
thank the Debian Haskell Group and, most especially, Scott Talbert, for
continued effort making Copilot available on Debian-based distros. This
will be extremely useful to a great portion of our users, who need to use
Copilot as a runtime verification system targeting C, but do not need to
become proficient in Haskell. We hope to continue this effort by making
Copilot easily available on other distributions and OSs.

Happy Haskelling,

The Copilot team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20221114/7ed6d4cb/attachment.html>