Abstract
We exhibit a rich class of Horn clauses, which we call \( \mathcal{H}_{\text{1}} \), whose least models, though possibly infinite, can be computed effectively. We show that the least model of an \( \mathcal{H}_{\text{1}} \) 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 \( \mathcal{H}_{\text{1}} \) clauses, which we call \( \mathcal{H}_{\text{2}} \), 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 \( \mathcal{H}_{\text{2}} \), we exhibit a fragment \( \mathcal{H}_{\text{3}} \) 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].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and A.D. Gordon. A Calculus for Cryptographic Protocols-The Spi Calculus. Information and Computation, 148:1–70, January 1999.
A. Aiken. Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming (SCP), 35(2):79–111, 1999.
D.A. Basin and H. Ganzinger. Complexity Analysis Based on Ordered Resolution. Journal of the ACM, 48(1):70–109, 2001.
W. Charatonik and A. Podelski. Set Constraints with Intersection. In 12th Ann. IEEE Symp. on Logic in Computer Science (LICS), 362–372, 1997.
H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. Available on: http://www.grappa.univ-lille3.fr/tata, 1999.
T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic Programs as Types of Logic Programs. In 6th Symp. on Logic in Computer Science (LICS), 300–309, 1991.
H. Ganzinger and D.A. McAllester. A New Meta-complexity Theorem for Bottom-Up Logic Programs. In First Int. Joint Conference on Automated Reasoning (IJ-CAR), 514–528. LNCS 2083, 2001.
N. Heintze and J. Jaffar. A Decision Procedure for a Class of Set Constraints. In 5th Ann. IEEE Symp. on Logic in Computer Science (LICS), 42–51, 1990.
N.D. Jones and S.S. Muchnick. Complexity of Flow Analysis, Inductive Assertion Synthesis, and a Language due to Dijkstra. In Steven S. Muchnick and Neil D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 12, 380–393. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.
D. Lugiez and P. Schnoebelen. Decidable First-Order Transition Logics for PA-Processes. In 27th Int. Coll. on Automata, Languages and Programming (ICALP), 342–353. LNCS 1853, 2000.
D. McAllester. On the Complexity Analysis of Static Analyses. In 6th Static Analysis Symposium (SAS), 312–329. LNCS 1694, 1999.
F. Nielson, H. Riis Nielson, and C. L. Hankin. Principles of Program Analysis. Springer, 1999.
F. Nielson, H. Riis Nielson, and H. Seidl. Automatic Complexity Analysis. In European Symposium on Programming (ESOP), 243–261. LNCS 2305, 2002.
F. Nielson, H. Riis Nielson, and H. Seidl. Cryptographic Analysis in Cubic Time. In Electronic Notes in Theoretical Computer Science (ENTCS), volume 62. Elsevier Science Publishers, 2002.
F. Nielson and H. Seidl. Control-Flow Analysis in Cubic Time. In European Symposium on Programming (ESOP), 252–268. LNCS 2028, 2001.
F. Nielson and H. Seidl. Succinct Solvers. Tech. Report 01-12, Trier, 2001.
L. Pacholski and A. Podelski. Set Constraints-a Pearl in Research on Constraints. In Gert Smolka, editor, 3rd Int. Conf. on Principles and Practice of Constraint Programming (CP), volume 1330 of Springer LNCS, 549–561. Springer-Verlag, 1997.
H. Seidl. Haskell Overloading is DEXPTIME Complete. Information Processing Letters (IPL), 54:57–60, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R., Seidl, H. (2002). Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_5
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive