Publication

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac
2011
Thèse EPFL
Résumé

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the state of the art in decision procedures, and their use in software reliability tools. First, we observe that developing new decision procedures increases the range of properties and programs that are amenable to automated verification. In this thesis, we are particularly interested in the verification of container data structures. Existing verification tools use set abstractions to reason about the contents of data structures. However, set abstraction loses any information about duplicate occurrences of elements in a container. We therefore propose a new logic for reasoning about multisets with cardinality constraints. This logic subsumes reasoning about sets and enables reasoning about duplicate elements in containers. Cardinality constraints are useful for reasoning about the number of elements stored in a data structure. Based on an extension of linear arithmetic (which we call LIA*), we describe a decision procedure for the logic ofmultisets with cardinalities. By investigating properties of LIA*, we prove that the satisfiability of multisets with cardinality constraints is an NP-complete problem. Second, we notice that verification conditions expressing properties of data structures often can be decomposed into several well-understood logics. If the signatures of the component theories are not disjoint (i.e., they sharemore than equality) then it is often unclear whether such a reduction is possible, even if individual decision procedures for all component theories are known to exist. We investigate how to combine non-disjoint theories that share set symbols and operators. We state and prove a new combination theorem for such theories. Our theorem states that the combination is possible if each component theory can be reduced to the common theory, the theory of sets with cardinality constraints. We prove that many theories satisfy this property. The resulting combined logic enables reasoning about complex properties of data structure implementations that could not be expressed in any previously known decidable logic. Finally, we identify new applications of decision procedures in software reliability tools. We describe how a model-producing decision procedure can be generalized into a predictable and complete synthesis procedure. Given a specification, a synthesis procedure is an algorithm that outputs the code that meets this specification. We demonstrate this approach in detail for the concrete case of linear integer arithmetic. We further develop an orthogonal approach to use decision procedure for program synthesis: we show how to reconstruct code snippets that satisfy given type constraints from a proof of unsatisfiability that was computed by a theorem prover. The programmer then interactively selects the desired code snippet from a choice of code snippets generated by the synthesis engine. Together, our results provide the foundations of sound and predictable verification and synthesis tools for integer arithmetic and container data structures.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.