Coco is designed specifically for building event-driven software. This type of software handles events coming from other software or hardware parts in the system, with limited control over or knowledge of the ordering or arrival of events, and coordinates responses accordingly. It is typically stateful, concurrent and asynchronous.

No, our users develop the event-driven parts of their software using Coco, and develop the other parts of their software using whichever tools are most suited. Coco was designed with this in mind and has numerous constructs to support this.

No, both Coco and Popili have been specifically designed for widespread use by developers with no background or expertise in formal verification.

Coco provides a number of built-in constucts to help your generated code seamlessly integrate into the rest of your code base. This includes support for allowing Coco to be given information about handwritten code to enable sufficient verification, and an attribute system provide a way of attaching metadata to Coco declarations, to indicate mappings into languages.

Coco supports both multi-threaded and single-threaded runtimes, as well as the combination of the two where single-threaded software stacks run within a multi-threaded environment.

Yes, you can find the Coco language reference here.

Coco generates standard-compliant:

• C++, targeting C++11/14/17
• C, targeting C99
• C#, targeting C# 11 and .NET 8

Yes, Popili also comes as a command-line tool, and integrate seamlessly with modern CI/CD tooling, as well as build systems, such as Bazel.

Popili runs on Windows, MacOS and Linux. See our Downloads page for details on the operating systems we support.

Eclipse and VS Code.

See our Getting Started page, which steps you through how to install Popili, and get up and running.