<div dir="ltr"><div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>Dear all,</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>I'm very excited to announce Copilot 3.12.</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>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.</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>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 (</span></span><span><a href="https://github.com/NASA-SW-VnV/fret/" class="gmail-_1FRfMxEAy__7c8vezYv9qP"><span><span>https://github.com/NASA-SW-VnV/fret/</span></span></a></span><span><span>), via Ogma (</span></span><span><a href="https://github.com/nasa/ogma" class="gmail-_1FRfMxEAy__7c8vezYv9qP"><span><span>https://github.com/nasa/ogma</span></span></a></span><span><span>).</span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><br></span></div></div><span></span><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>The main changes in this release are as follows:</span></span></div></div><ul><li><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>A new library </span></span><span style="font-family:Noto Mono,Menlo,Monaco,Consolas,monospace;padding:0.1em 0.2em;font-size:0.8em;border-radius:3px"><span>copilot-prettyprinter</span></span><span><span> exposes functions related to the Copilot Core pretty-printing backend. Pre-existing functions included as part of copilot-core are now deprecated.</span></span></div></li><li><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>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.</span></span></div></li><li><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>The custom type equality module in </span></span><span style="font-family:Noto Mono,Menlo,Monaco,Consolas,monospace;padding:0.1em 0.2em;font-size:0.8em;border-radius:3px"><span>copilot-core</span></span><span><span> is now deprecated in favour of the definition of type equality in </span></span><span style="font-family:Noto Mono,Menlo,Monaco,Consolas,monospace;padding:0.1em 0.2em;font-size:0.8em;border-radius:3px"><span>base</span></span><span><span>.</span></span></div></li><li><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span style="font-family:Noto Mono,Menlo,Monaco,Consolas,monospace;padding:0.1em 0.2em;font-size:0.8em;border-radius:3px"><span>copilot-theorem</span></span><span><span> now includes support for proofs by bisimulation necessary for future extensions to Copilot.</span></span></div></li><li><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span style="font-family:Noto Mono,Menlo,Monaco,Consolas,monospace;padding:0.1em 0.2em;font-size:0.8em;border-radius:3px"><span>copilot-core</span></span><span><span> 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.</span></span></div></li></ul><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>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 (</span></span><span><a href="https://github.com/copilot-language/copilot" class="gmail-_1FRfMxEAy__7c8vezYv9qP"><span><span>https://github.com/copilot-language/copilot</span></span></a></span><span><span>).</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>I'd also like to take this opportunity to announce that </span></span><span style="font-style:italic"><span>Copilot is now available on Debian</span></span><span><span>. As a consequence of this effort, Copilot will also be available to Ubuntu users in the near future. We would like to publicly</span></span><span style="font-style:italic"><span> thank the Debian Haskell Group and, most especially, Scott Talbert</span></span><span><span>, 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.</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>Happy Haskelling,</span></span></div><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span><br></span></span></div></div><div class="gmail-"><div class="gmail-public-DraftStyleDefault-block gmail-public-DraftStyleDefault-ltr"><span><span>The Copilot team</span></span></div></div></div></div>