License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.Gabbrielli.7
URN: urn:nbn:de:0030-drops-132294
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13229/
Go to the corresponding OASIcs Volume Portal

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

Abstract Interpretation, Symbolic Execution and Constraints

pdf-format:
OASIcs-Gabbrielli-7.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{amadini_et_al:OASIcs:2020:13229,
  author =	{Roberto Amadini and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Peter J. Stuckey},
  title =	{{Abstract Interpretation, Symbolic Execution and Constraints}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{7:1--7:19},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{Frank S. de Boer and Jacopo Mauro},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13229},
  URN =		{urn:nbn:de:0030-drops-132294},
  doi =		{10.4230/OASIcs.Gabbrielli.7},
  annote =	{Keywords: Abstract interpretation, symbolic execution, constraint solving, dynamic analysis, static analysis}
}

Keywords: Abstract interpretation, symbolic execution, constraint solving, dynamic analysis, static analysis
Collection: Recent Developments in the Design and Implementation of Programming Languages
Issue Date: 2020
Date of publication: 27.11.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI