FORMULA 2.0: a language for formal specifications. FORMULA 2.0 is a novel formal specification language based on {it open-world logic programs} and {it behavioral types}. Its goals are (1) succinct specifications of domain-specific abstractions and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse synthesis and fast verification. We take a unique approach towards achieving these goals: Specifications are written as strongly-typed open-world logic programs. They are highly declarative and easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution of logic programs into constraints. This tutorial introduces the FORMULA 2.0 language and concepts through a series of small examples.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element