# Synthesizing Formal Semantics from Executable Interpreters

**Authors:** Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J. C. Johnson, Thomas Reps, Loris D'Antoni  
**arXiv:** [2408.14668](https://arxiv.org/abs/2408.14668)  
**Date:** 2024-08-26  
**Summary page:** https://www.summarizepaper.com/en/arxiv-id/2408.14668v1/

## Key points

- Frameworks in program verification and synthesis often require users to provide formally defined semantics for the language of interest
- A new algorithm has been developed to automatically synthesize inductively defined syntax-directed semantics
- The algorithm requires a grammar describing the syntax of a language and an executable interpreter for computing program semantics
- Synthesized semantics are expressed in Constrained-Horn Clauses (CHCs), a formal logical framework widely used in program verification and synthesis
- The algorithm uses Counterexample-Guided Synthesis (CEGIS) approach to break down the problem into smaller expression-synthesis problems
- The tool Synantic successfully synthesized formal semantics from 14 interpreters for commonly used languages, leading to efficiency improvements in some cases
- Challenges include breaking down synthesis problems effectively leveraging compositionality within semantic definitions

## Summary

, , , , 

In the field of program verification and synthesis, frameworks that allow for customization of programming languages often require users to provide formally defined semantics for the language of interest. However, writing formal semantics can be a challenging and error-prone task, hindering the adoption of such frameworks by non-expert users. To address this issue, a new algorithm has been developed that can automatically synthesize inductively defined syntax-directed semantics. This algorithm requires two inputs: (i) a grammar describing the syntax of a language and (ii) an executable interpreter for computing program semantics in the specified language. The synthesized semantics are expressed in Constrained-Horn Clauses (CHCs), a formal logical framework widely used in program verification and synthesis. A key innovation of this synthesis algorithm is its Counterexample-Guided Synthesis (CEGIS) approach, which breaks down the complex problem of synthesizing constrained Horn clauses into smaller, more manageable expression-synthesis problems. These smaller problems can then be solved using existing SyGuS synthesizers. The tool developed based on this algorithm, called Synantic, successfully synthesized inductively-defined formal semantics from 14 interpreters for languages commonly used in program-synthesis applications. Notably, when synthesizing formal semantics for one benchmark language (regular expressions), Synantic identified an inconsistency in the computed semantics by the interpreter. By resolving this inconsistency, a more efficient semantics was achieved, leading to a 1.2x speedup for a synthesizer solving synthesis problems over that particular language. Furthermore, the paper discusses challenges related to breaking down the synthesis problem into simpler components to design practical solutions effectively leveraging compositionality within semantic definitions. By addressing these challenges and providing insights into improving existing semantic representations through automated synthesis techniques, this research contributes significantly to advancing program verification and synthesis methodologies. Overall, this work showcases how automated synthesis algorithms can streamline the process of defining formal semantics for programming languages, making advanced program verification and synthesis techniques more accessible to both expert and non-expert users alike.