Sciweavers

Share
CACM
2010

Reasoning about the unknown in static analysis

9 years 10 months ago
Reasoning about the unknown in static analysis
Static program analysis techniques cannot know certain values, such as the value of user input or network state, at analysis time. While such unknown values need to be treated as non-deterministic choices made by the program's execution environment, it is still possible to glean very useful information about how such statically unknown values may or must influence computation. We give a method for integrating such non-deterministic choices with an expressive static analysis. Interestingly, we cannot solve the resulting recursive constraints directly, but we give an exact method for answering all may and must queries. We show experimentally that the resulting solved forms are concise in practice, enabling us to apply the technique to very large programs, including an entire operating system.
Isil Dillig, Thomas Dillig, Alex Aiken
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CACM
Authors Isil Dillig, Thomas Dillig, Alex Aiken
Comments (0)
books