Paper Info
Title
Pretty-Big-Step-Semantics-Based Certified Abstract Interpretation (Preliminary Version)
Abstract
We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on a particular kind of semantics called prettybig- step semantics. We present a pretty-big-step semantics of a language with simple objects called O'While and specify a series of instrumentations of the semantics that explicitates the flows of values in a program. This leads to a semantics-based dependency analysis, at the core, e.g., of tainting analysis in software security. The formalization has been realized with the Coq proof assistant.
Year
DOI
Venue
2013
10.4204/EPTCS.129.23
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Issue
Formal semantics (linguistics),Operational semantics,Programming language,Computational semantics,Computer science,Denotational semantics,Action semantics,Type erasure,Theoretical computer science,Well-founded semantics,Semantics (computer science)
Journal
129
ISSN
Citations 
PageRank 
2075-2180
1
0.35
References 
Authors
11
3
Name
Order
Citations
PageRank
Martin Bodin1474.28
Thomas Jensen211.36
Alan Schmitt354731.50