FORMULA – Modeling Foundations

Established: December 10, 2008

FORMULA 2.0: Formal Specifications for Verification and Synthesis
Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems.

FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs) and model transformations. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation and execution of input programs, (3) program synthesis and compiler verification.

FORMULA 2.0 provides these features in a unique way: Specifications are written as strongly-typed open-world logic programs. These specifications are highly declarative and easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution of logic programs into quantifier-free constraints, which are dispatched to the state-of-the-art SMT solver Z3. FORMULA has been applied within Microsoft to develop DSLs for verifiable device drivers and protocols. It has been used by the automotive / embedded systems industries for software / hardware co-design under hard resource allocation constraints.





August 2011

FORMULA (Formal Modeling Using Logic Programming and Analysis) is a modern formal specification language targeting model-based development (MBD). It is based on algebraic data types (ADTs) and strongly-typed constraint logic programming (CLP), which support concise specifications of abstractions and model transformations. Around this core is a set of composition operators for composing specifications in the…

Size: 7 MB

    Click the icon to access this download

  • Website