We describe Chisel—a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. This semantics is assumed to be a rewriting logic specification, given in Maude, while the program is a ground term of this specification. We present the tool on two types of language parar digms: high-level, imperative and low-level assembly languages. We conduct experiments with standard benchmarking used in avionics.
展开▼
