Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Program Synthesis from Formal Specifications for Correctness-by-Construction in CorC

Forschungsthema:Program Verification
Typ: MA
Datum: 2024-05-31
Betreuer: Tabea Bordis
Michael Kirsten
Wolfram Pfeifer
Aushang:

Abstract

The role of software becomes increasingly important in our everyday life, and so does the demand for safety guarantees for it. In this thesis, we aim at easing the development of correct software by automating parts of its development process. Correctness-by-Construction (CbC) is a software development process. In this process, programs are provided with formal specifications and created by means of correctness-preserving refinements. The CorC tool makes it possible to develop programs using CbC. The aim of program synthesis is to automatically synthesize programs that meet the specification from a formal specification, as used in CbC.

In this master's thesis, the aim is to familiarize oneself with program synthesis techniques and develop a concept for applying these to CbC as implemented in the CorC tool. The thesis will also evaluate the degree to which program synthesis can be implemented with the resulting concept and how well the synthesized programs fit their specifications.

For this matter, we investigate the feasibility of program synthesis for small code statements. We aim at synthesizing correct code from these specifications instead of writing code by hand. For this, we use syntax-guided synthesis (SyGuS), which is a synthesis technique based on the generation of possible programs and checking them against a given specification. We propose a concept consisting of a basic workflow and multiple expansions, which are realized in a prototypical implementation. The implementation supports the synthesis of Java code and is built on the tool framework consisting of CorC, KeY and cvc5. An evaluation through multiple case studies confirmed the feasibility of SyGuS for CorC. Included features are the synthesis of loop bodies, statements which include multiple assignments and partial array support. The results highlight the potential of automated program synthesis to enhance the usability of CbC in CorC and demonstrate the feasibility of integrating SyGuS with CbC.

See also description on the TVA site.

Literature