Sciweavers

POPL
2006
ACM

A fixpoint calculus for local and global program flows

14 years 2 months ago
A fixpoint calculus for local and global program flows
We define a new fixpoint modal logic, the visibly pushdown ?-calculus (VP-?), as an extension of the modal ?-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and interprocedural analysis, and it has constructs that allow skipping procedure calls so that local flows in a procedure can also be tracked. The logic generalizes t...
Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
Comments (0)