Context-updates analysis and refinement in chisel

Abstract

This paper presents the context-updates synthesis component of Chisel, a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. By context-updates we understand programming language constructs that induce unconditional control-flow non-sequentiality, i.e., gotos or subroutine calls. The context-updates synthesis follows two directions: an over-approximation phase that extracts a set of potential context-update constructs and an under-approximation phase that refines the results of the first step by testing the behavior of the context-updates constructs produced at the previous phase. We use two experimental semantics that cover two types of language paradigms: high-level imperative languages and low-level assembly languages and we conduct the tests on standard benchmarks used in avionics.