Show simple item record

dc.contributor.advisorD'Souza, Deepak
dc.contributor.authorSumanth Prabhu, S
dc.date.accessioned2024-01-01T11:15:45Z
dc.date.available2024-01-01T11:15:45Z
dc.date.submitted2023
dc.identifier.urihttps://etd.iisc.ac.in/handle/2005/6338
dc.description.abstractMany practical problems in software development, verification and testing rely on specifications. The problem of specification synthesis is to automatically find relational constraints for undefined functions, called specifications, in a given program and a postcondition. Specifications are helpful in verifying open programs, compositional verification, automatic test case generation, run-time checks, program understanding and many more applications. Maximal (or logically weakest) specifications are desirable in all these applications. The specifications also have to be valid with respect to the given program's semantics and the postcondition. Existing tools expect the developers of programs to provide specifications. Providing specifications is tedious for developers, hindering the wide adoption of program verification and synthesis tools. Automatic synthesis of valid and maximal specifications is beneficial; but has several challenges. This thesis proposes techniques to overcome the challenges. The techniques work in a framework called Infer-Check-Weaken, using which valid and maximal specifications are effectively synthesised. The core idea behind Infer-Check-Weaken is first to infer a valid specification. Then, in a loop, the specification is checked for maximality. When the check fails, weakening is performed. This loop continues till a maximal specification is obtained. Depending on the specifications to be inferred and the structure of the programs, we propose different techniques to perform each task. We show the effectiveness of these techniques over publicly available benchmarks. More specifically, for programs with integer variables and linear arithmetic operations, we propose an inference technique called Non-vacuous Specification Synthesis (NSS), which can find specifications like function contracts on undefined functions, preconditions, and others along with inductive invariants. NSS works on the idea of backward and forward reasoning. The maximality checking is performed by encoding the problem as a logical formula and then using an SMT solver. Further, weakening is done using the feedback from maximality checking and the NSS module. This thesis's second and third contributions are in finding the weakest precondition for deterministic and non-deterministic terminating programs that manipulate arrays. Such programs often require quantified preconditions, which are difficult to reason about. To infer quantified preconditions, we propose two techniques: Range Abduction (RA) and its extension Structural Array Abduction (SAA). RA extends the logical abduction to quantified formulas over arrays. SAA further extends RA to find proof of maximality additionally. We propose different maximality-checking techniques for deterministic and non-deterministic programs based on program transformation and a syntax-guided-synthesis-based weakening procedure. These techniques work at the level of a logical intermediate representation in the Floyd-Hoare style, making them agnostic to programming languages. The intermediate representation is called constrained Horn clauses, which are gaining popularity among various program verification tools. Hence, our techniques can be integrated with the existing tools.en_US
dc.description.sponsorshipTCS Researchen_US
dc.language.isoen_USen_US
dc.relation.ispartofseries;ET00350
dc.rightsI grant Indian Institute of Science the right to archive and to make available my thesis or dissertation in whole or in part in all forms of media, now hereafter known. I retain all proprietary rights, such as patent rights. I also retain the right to use in future works (such as articles or books) all or part of this thesis or dissertationen_US
dc.subjectspecification synthesisen_US
dc.subjectInfer-Check-Weakenen_US
dc.subjectNon-vacuous Specification Synthesisen_US
dc.subjectcomputer programsen_US
dc.subjectHorn clausesen_US
dc.subject.classificationResearch Subject Categories::TECHNOLOGY::Information technology::Computer science::Computer scienceen_US
dc.titleSpecification Synthesis with Constrained Horn Clausesen_US
dc.typeThesisen_US
dc.degree.namePhDen_US
dc.degree.levelDoctoralen_US
dc.degree.grantorIndian Institute of Scienceen_US
dc.degree.disciplineEngineeringen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record