TY - GEN
T1 - Normalizable horn clauses, strongly recognizable relations, and spi
AU - Nielson, Flemming
AU - Nielson, Hanne Riis
AU - Seidl, Helmut
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002
Y1 - 2002
N2 - We exhibit a rich class of Horn clauses, which we call H1, whose least models, though possibly infinite, can be computed effectively. We show that the least model of an H1 clause consists of so-called strongly recognizable relations and present an exponential normalization procedure to compute it. In order to obtain a practical tool for program analysis, we identify a restriction of H1 clauses, which we call H2, where the least models can be computed in polynomial time. This fragment still allows to express, e.g., Cartesian product and transitive closure of relations. Inside H2, we exhibit a fragment H3 where normalization is even cubic. We demonstrate the usefulness of our approach by deriving a cubic control-flow analysis for the Spi calculus [1] as presented in [14].
AB - We exhibit a rich class of Horn clauses, which we call H1, whose least models, though possibly infinite, can be computed effectively. We show that the least model of an H1 clause consists of so-called strongly recognizable relations and present an exponential normalization procedure to compute it. In order to obtain a practical tool for program analysis, we identify a restriction of H1 clauses, which we call H2, where the least models can be computed in polynomial time. This fragment still allows to express, e.g., Cartesian product and transitive closure of relations. Inside H2, we exhibit a fragment H3 where normalization is even cubic. We demonstrate the usefulness of our approach by deriving a cubic control-flow analysis for the Spi calculus [1] as presented in [14].
KW - Program analysis
KW - Spi calculus
KW - Strongly recognizable relations
KW - Uniform horn clauses
UR - http://www.scopus.com/inward/record.url?scp=84958766164&partnerID=8YFLogxK
U2 - 10.1007/3-540-45789-5_5
DO - 10.1007/3-540-45789-5_5
M3 - Conference contribution
AN - SCOPUS:84958766164
SN - 3540442359
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 35
EP - 2002
BT - Static Analysis - 9th International Symposium, SAS 2002 Madrid, Spain, September 17-20, 2002 Proceedings
A2 - Hermenegildo, Manuel V.
A2 - Puebla, German
PB - Springer Verlag
T2 - 9th International Static Analysis Symposium, SAS 2002
Y2 - 17 September 2002 through 20 September 2002
ER -