Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
This addresses the problem of automating program synthesis from formal specifications for engineers, but it appears incremental as it builds on existing realizability proofs and benchmark models.
The paper tackles the problem of automatically constructing implementations from formal requirements by proposing a novel approach to program synthesis using k-inductive proofs of realizability and extracting Skolem functions. The result is the implementation in the JSyn tool, which synthesizes C code from contracts and demonstrates usability and effectiveness on benchmark models with hand-written implementations.
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizability is proven, is to construct such an implementation automatically, and thus solve the problem of program synthesis. In this paper, we propose a novel approach to pro- gram synthesis guided by k-inductive proofs of realizability of assume- guarantee contracts constructed from safety properties. The proof of re- alizability is performed over a set of forall-exists formulas, and synthesis is per- formed by extracting Skolem functions witnessing the existential quan- tification. These Skolem functions can then be combined into an imple- mentation. Our approach is implemented in the JSyn tool which con- structs Skolem functions from a contract written in a variant of the Lus- tre programming language and then compiles the Skolem functions into a C language implementation. For a variety of benchmark models that already contained hand-written implementations, we are able to identify the usability and effectiveness of the synthesized counterparts, assuming a component-based verification framework.