2026-07-25T12:07:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13229 2026-01-26T12:00:22Z ddc:004 open_access

Abstract Interpretation, Symbolic Execution and Constraints Amadini, Roberto Gange, Graeme Schachte, Peter Søndergaard, Harald Stuckey, Peter J. Abstract interpretation symbolic execution constraint solving dynamic analysis static analysis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Roberto Amadini and Graeme Gange and Peter Schachte and Harald Søndergaard and Peter J. Stuckey 2020 Is Part Of OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.Gabbrielli.7 urn:nbn:de:0030-drops-132294 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.7 eng https://creativecommons.org/licenses/by/3.0/legalcode