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 that provides 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.

Popili 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 integrates with modern CI/CD tooling, as well as build systems, such as Bazel.

Popili runs on Windows, MacOS and Linux.

Eclipse and VS Code.

Once you have a licence, visit our Getting Started page, which steps you through how to get up and running with Popili.