Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user provided syntactic restriction o...
详细信息
Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guidedinductivesynthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T), where T is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T) within the mature synthesiser CVC4 and show that CEGIS(T) improves CVC4's results.
This paper proposes relational program synthesis, a new problem that concerns synthesizing one or more programs that collectively satisfy a relational specification. As a dual of relational program verification, relat...
详细信息
This paper proposes relational program synthesis, a new problem that concerns synthesizing one or more programs that collectively satisfy a relational specification. As a dual of relational program verification, relational program synthesis is an important problem that has many practical applications, such as automated program inversion and automatic generation of comparators. However, this relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space. As a first step towards solving this problem, this paper presents a synthesis technique that combines the counterexample-guidedinductivesynthesis framework with a novel inductivesynthesis algorithm that is based on relational version space learning. We have implemented the proposed technique in a framework called RELISH, which can be instantiated to different application domains by providing a suitable domain-specific language and the relevant relational specification. We have used the RELISH framework to build relational synthesizers to automatically generate string encoders/decoders as well as comparators, and we evaluate our tool on several benchmarks taken from prior work and online forums. Our experimental results show that the proposed technique can solve almost all of these benchmarks and that it significantly outperforms EUSoLvEn, a generic synthesis framework that won the general track of the most recent SyGuS competition.
Nowadays, formal methods are used in various areas for the verification of programs or for code generation from models in order to increase the quality of software and to reduce costs. However, there are still fields ...
详细信息
ISBN:
(纸本)9781728143958
Nowadays, formal methods are used in various areas for the verification of programs or for code generation from models in order to increase the quality of software and to reduce costs. However, there are still fields in which formal methods haven't been widely adopted, despite the large set of possible benefits offered. This is the case for the area of programmable logic controllers (PLC). This article aims to evaluate the potential of formal methods in the context of PLC development. For this purpose, the general concepts of formal methods are first introduced and then transferred to the PLC area, resulting in an engineering-oriented description of the technology that is based on common concepts from PLC development. Based on this description, PLC professionals with varying degrees of experience were interviewed for their perspective on the topic and to identify possible use cases within the PLC domain. The survey results indicate the technology's high potential in the PLC area, either as a tool to directly support the developer or as a key element within a model-based systems engineering toolchain. The evaluation of the survey results is performed with the aid of a demo application that communicates with the Totally Integrated Automation Portal from Siemens and generates programs via Fastsynth, a model-based open source code generator. Benchmarks based on an industry-related PLC project show satisfactory synthesis times and a successful integration into the workflow of a PLC developer.
Context: Craig interpolation is a significant and efficient application to formal verification and synthesis. However, there still remains a challenge in the synthesis of Craig interpolation for nonlinear ***: For qua...
详细信息
Context: Craig interpolation is a significant and efficient application to formal verification and synthesis. However, there still remains a challenge in the synthesis of Craig interpolation for nonlinear ***: For quantifier-free theories of nonlinear arithmetic, this paper proposes a new approach to generate nonlinear Craig interpolants represented as deep neural ***: The approach exploits a CEGIS framework where a learner yields a neural candidate interpolant satisfying the interpolant conditions against training data sets, and a verifier adopts computer algebra methods to confirm the correctness of the candidate or to generate counterexamples for further refining the candidate. Results: We implement the tool SyntheNI based on our CEGIS procedure, and assess the performance against a collection of benchmark examples. The tool SyntheNI performs better than existing methods in the aspect of the iteration number and the computational time. As an application, the tool SyntheNI is used to synthesize loop ***: The SyntheNI can generate nonlinear Craig interpolants for quantifier free nonlinear real arith-metic. The experimental evaluation confirms the high performance of our synthesis method.
暂无评论