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.
- Ethan Jackson, Tihamer Levendovszky, and Daniel Balasubramanian, Reasoning about Metamodeling with Formal Specifications and Automatic Proofs, in MODELS 2011, 2011
- ethan jackson, nikolaj bjorner, and wolfram schulte, Canonical Regular Types, in ICLP (Technical Communications), 2011
- Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, Springer Verlag, 2010
- Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen, Components, platforms and possibilities: towards generic automation for MDA, in EMSOFT, ACM, 2010
- Ethan K. Jackson and Daniel Balasubramanian, Lost in Translation: Forgetful Semantic Anchoring, in Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering, 16 November 2009
- Ethan K. Jackson and Eunsuk Kang, Generalizing Design Space Exploration, in Under Review, 2009
- Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai, Reusing Model Transformations While Preserving Properties, in Under Review, 2009
- Ethan K. Jackson, Dirk Seifert, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte, and Markus Dahlweid, Specifying and Composing Non-functional Requirements in Model-Based Development, in Proceedings of the 8th International Conference on Software Composition, Springer Verlag, 2009
- Ethan K. Jackson, Wolfram Schulte, and Janos Sztipanovits, The Power of Rich Syntax for Model-based Development, Microsoft Research, 2008
- Ethan K. Jackson and Wolfram Schulte, Compositional Modeling for Data-Centric Business Applications, in Software Composition, Springer, 2008
- Ethan K. Jackson and Wolfram Schulte, Model Generation for Horn Logic with Stratified Negation, in Formal Techniques for Networked and Distributed Systems – FORTE 2008, Springer Verlag, 2008