Inactive.
Develop a highly precise and powerful program analysis applicable across a wide range of higher-order programming paradigms, based on the idea of extracting inductive definitions from programs. Inductive definitions are the lingua franca of modern theorem provers and compiling a program directly to an inductive definition puts the program in a language the theorem prover will best be able to reason about.
Paritosh Shroff, Christian Skalka, and Scott Smith. The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification. In APLAS 2007: The Fifth ASIAN Symposium on Programming Languagues and Systems.
We develop a static analysis which distills first-order computational structure from higher-order functional programs. The analysis condenses higher-order programs into a first-order rule-based system, a nugget, that characterizes all value bindings that may arise from program execution. Theorem provers are limited in their ability to automatically reason about higher-order programs; nuggets address this problem, being inductively defined structures that can be simply and directly encoded in a theorem prover. The theorem prover can then prove non-trivial program properties, such as the range of values assignable to particular variables at runtime. Our analysis is flow- and path-sensitive, and incorporates a novel prune-rerun analysis technique to approximate higher-order recursive computations.