Sound, complete and scalable path-sensitive analysis

Citations Over TimeTop 1% of 2008 papers

Abstract

We present a new, precise technique for fully path- and context-sensitive program analysis. Our technique exploits two observations: First, using quantified, recursive formulas, path- and context-sensitive conditions for many program properties can be expressed exactly. To compute a closed form solution to such recursive constraints, we differentiate between observable and unobservable variables, the latter of which are existentially quantified in our approach. Using the insight that unobservable variables can be eliminated outside a certain scope, our technique computes satisfiability- and validity-preserving closed-form solutions to the original recursive constraints. We prove the solution is as precise as the original system for answering may and must queries as well as being small in practice, allowing our technique to scale to the entire Linux kernel, a program with over 6 million lines of code.

Related Papers

• → Strategic behavior in the partially observable Markovian queues with partial breakdowns(2017)14 cited
• → Output canonical form for observable and unobservable systems(1971)1 cited
• → Reduction of time-varying linear systems to controllable and observable form†(1970)1 cited
• The Woes of Scientific Realism(2012)
• → Partially Observable Control Models(1989)