Abstract interpretation, symbolic execution and constraints

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

4 Citations (Scopus)

Abstract

Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each – implicitly or explicitly – maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.

Original languageEnglish
Title of host publicationRecent Developments in the Design and Implementation of Programming Languages
EditorsFrank S. de Boer, Jacopo Mauro
Place of PublicationSaarbrücken/Wadern Germany
PublisherSchloss Dagstuhl
Number of pages19
ISBN (Electronic)9783959771719
DOIs
Publication statusPublished - Nov 2020
EventRecent Developments in the Design and Implementation of Programming Languages 2020 - Bologna, Italy
Duration: 27 Nov 202027 Nov 2020

Publication series

NameOpenAccess Series in Informatics
Volume86
ISSN (Print)2190-6807

Conference

ConferenceRecent Developments in the Design and Implementation of Programming Languages 2020
Country/TerritoryItaly
CityBologna
Period27/11/2027/11/20

Keywords

  • Abstract interpretation
  • Constraint solving
  • Dynamic analysis
  • Static analysis
  • Symbolic execution

Cite this