{"id":170112,"date":"2008-12-10T11:50:37","date_gmt":"2008-12-10T11:50:37","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/formula-modeling-foundations\/"},"modified":"2019-08-19T15:37:34","modified_gmt":"2019-08-19T22:37:34","slug":"formula-modeling-foundations","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/formula-modeling-foundations\/","title":{"rendered":"FORMULA – Modeling Foundations"},"content":{"rendered":"

\"\"<\/span><\/span><\/p>\n

\n

FORMULA 2.0: Formal Specifications for Verification and Synthesis<\/b>
\nFormula specifications are highly declarative logic programs that can express rich synthesis and verification problems.<\/p>\n

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.<\/p>\n

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.<\/p>\n<\/div>\n

\"\" (opens in new tab)<\/span><\/a><\/span><\/span><\/div>\n","protected":false},"excerpt":{"rendered":"

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 […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170112","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-10","related-publications":[159444,161145,162207,162208,155814,155818,155828,158382,158383],"related-downloads":[169176],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Ethan Jackson","user_id":31727,"people_section":"Group 1","alias":"ejackson"},{"type":"user_nicename","display_name":"Nikolaj Bj\u00f8rner","user_id":33067,"people_section":"Group 1","alias":"nbjorner"},{"type":"user_nicename","display_name":"Laurent Bussard","user_id":32626,"people_section":"Group 1","alias":"lbussard"}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170112"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170112\/revisions"}],"predecessor-version":[{"id":604422,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170112\/revisions\/604422"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170112"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170112"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170112"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170112"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170112"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}