New Generation Computing, 24(2006)53-78
Ohmsha, Ltd. and Springer

Static Extensivity Analysis for -Definable Functions over Lattices

Hyunjun EO*, Kwangkeun YI** and Kwang-Moo CHOE*
* Division of Computer Science
Korea Advanced Institute of Science and Technology
373-1 Guseong-dong Yuseong-gu, Daejeon 305-701, Korea
poisson@ropas.kaist.ac.kr
choe@cs.kaist.ac.kr
**School of Computer Science and Engineering
Seoul National University
San 56-1 Sillim-dong Gwanak-gu, Seoul 151-742, Korea
kwang@ropas.snu.ac.kr

Received 26 April 2004
Revised manuscript received 29 July 2005

Abstract

We employ a static analysis to examine the extensivity (∀x : x ≤ f(x)) of functions defined over lattices in λ-calculus augmented with lattice operations. The need for such a verification procedure has arisen in our work on a generator system (called Zoo) of static program-analyzers. The input to Zoo is a static analysis specification that consists of lattice definitions and function definitions over the lattices. Once the extensivity of the functions is ascertained, the generated analyzer is guaranteed to terminate when the lattices have finite-heights. The extensivity analysis consists of a sound syntax-driven deductive rules whose satisfiability check is done by a constraint solving procedure.

Keywords:Static Analysis, Functional Static-Analysis Specification, Function Extensivity, Deductive System, Constraints Solving.

[Back]