Many meta-languages have been proposed for writing rule-based operational semantics, in order to provide general interpreters and analysis tools. We take a different approach. We develop a meta-language for a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We provide four generic interpretations of our skeletal semantics to yield: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results, establishing that the concrete and abstract interpretations are consistent and that any solution to the constraints generated by the constraint generator must be a correct abstract semantics.
Slides (slides.pdf) | 1019KiB |
Fri 18 Jan
10:35 - 12:03: Research Papers - Abstract Interpretation at Sala II Chair(s): David NaumannStevens Institute of Technology | ||||||||||||||||||||||||||||||||||||||||||
10:35 - 10:57 Talk | Patrick Cousot, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Francesco RanzatoUniversity of Padova Link to publication DOI Media Attached File Attached | |||||||||||||||||||||||||||||||||||||||||
10:57 - 11:19 Talk | Link to publication DOI Media Attached | |||||||||||||||||||||||||||||||||||||||||
11:19 - 11:41 Talk | Martin BodinImperial College London, Philippa GardnerImperial College London, Thomas P. JensenINRIA Rennes, Alan SchmittInria Link to publication DOI Pre-print Media Attached File Attached | |||||||||||||||||||||||||||||||||||||||||
11:41 - 12:03 Talk | John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Zachary KincaidPrinceton University, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc. Link to publication DOI Media Attached File Attached |