Skip to Main content Skip to Navigation
New interface
Conference papers

Trace-Based Control-Flow Analysis

Benoît Montagu 1 Thomas Jensen 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We define a small-step semantics for the untyped λ-calculus, that traces the β-reductions that occur during evaluation. By abstracting the computation traces, we reconstruct-CFA using abstract interpretation, and justify constraint-based-CFA in a semantic way. The abstract interpretation of the trace semantics also paves the way for introducing widening operators in CFA that go beyond existing analyses, that are all based on exploring a finite state space. We define ∇CFA, a widening-based analysis that limits the cycles in call stacks, and can achieve better precision than-CFA at a similar cost.
Document type :
Conference papers
Complete list of metadata
Contributor : Benoît Montagu Connect in order to contact the contributor
Submitted on : Tuesday, June 22, 2021 - 11:26:42 AM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM
Long-term archiving on: : Thursday, September 23, 2021 - 6:21:36 PM


Files produced by the author(s)



Benoît Montagu, Thomas Jensen. Trace-Based Control-Flow Analysis. PLDI 2021 - 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Jun 2021, Virtual, Canada. pp.1-15, ⟨10.1145/3453483.3454057⟩. ⟨hal-03266981⟩



Record views


Files downloads