short-paper

Constraint Specialisation in Horn Clause Verification

Authors:

Bishoksan Kafle,

John P. GallagherAuthors Info & Claims

PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation

Pages 85 - 90

https://doi.org/10.1145/2678015.2682544

Published: 13 January 2015 Publication History

Abstract

We present a method for specialising the constraints in constrained Horn clauses with respect to a goal. We use abstract interpretation to compute a model of a query-answer transformation of a given set of clauses and a goal. The effect is to propagate the constraints from the goal top-down and propagate answer constraints bottom-up. Our approach does not unfold the clauses at all; we use the constraints from the model to compute a specialised version of each clause in the program. The approach is independent of the abstract domain and the constraints theory underlying the clauses. Experimental results on verification problems show that this is an effective transformation, both in our own verification tools (convex polyhedra analyser) and as a pre-processor to other Horn clause verification tools.

References

[1]

R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1-2):3--21, 2008.

Digital Library

[2]

T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with slam. Commun. ACM, 54(7):68--76, 2011.

Digital Library

[3]

F. Bancilhon, D. Maier, Y. Sagiv, and J. Ullman. Magic sets and other strange ways to implement logic programs. In Proceedings of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems, 1986.

Digital Library

[4]

F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher, editor, Logic-Based Program Synthesis and Transformation (LOPSTR'96), volume 1207 of Springer-Verlag LNCS, pages 204--223, August 1996.

Digital Library

[5]

D. Beyer. Second competition on software verification - (summary of sv-comp 2013). In N. Piterman and S. A. Smolka, editors, TACAS, volume 7795 of LNCS, pages 594--609. Springer, 2013.

Digital Library

[6]

N. Bjørner, K. L. McMillan, and A. Rybalchenko. On solving universally quantified horn clauses. In F. Logozzo and M. Fähndrich, editors, SAS, volume 7935 of LNCS, pages 105--125. Springer, 2013.

[7]

F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. Lopez-García, and G. Puebla. The Ciao Prolog system. reference manual. Technical Report CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), August 1997. Available from http://www.clip.dia.fi.upm.es/.

[8]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752--794, 2003.

Digital Library

[9]

M. Codish and B. Demoen. Analyzing logic programs using 'PROP'- ositional logic programs and a magic wand. J. Log. Program., 25(3): 249--274, 1995. .

[10]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pages 238--252, 1977.

Digital Library

[11]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In R. M. Graham, M. A. Harrison, and R. Sethi, editors, POPL, pages 238--252. ACM, 1977.

Digital Library

[12]

P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.

[13]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages, pages 84--96, 1978.

Digital Library

[14]

E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying programs via iterated specialization. In E. Albert and S.-C. Mu, editors, PEPM, pages 43--52. ACM, 2013.

Digital Library

[15]

E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Verimap: A tool for verifying programs through transformations. In E. Abraham and K. Havelund, editors, TACAS, volume 8413 of LNCS, pages 568--574. Springer, 2014. ISBN 978--3--642--54861--1.

[16]

S. Debray and R. Ramakrishnan. Abstract Interpretation of Logic Programs Using Magic Transformations. Journal of Logic Programming, 18:149--176, 1994.

[17]

H. Fujita. An algorithm for partial evaluation with constraints. Technical Report TR-258, ICOT, 1987.

[18]

J. P. Gallagher. Specialisation of logic programs: A tutorial. In Proceedings PEPM'93, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 88--98, Copenhagen, June 1993. ACM Press.

Digital Library

[19]

J. P. Gallagher and M. Bruynooghe. Some low-level source transformations for logic programs. In Proceedings of Meta90 Workshop on Meta Programming in Logic. Katholieke Universiteit Leuven, Belgium, 1990.

[20]

J. P. Gallagher and D. de Waal. Deletion of redundant unary type predicates from logic programs. In K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation,Workshops in Computing, pages 151--167. Springer-Verlag, 1993.

[21]

J. P. Gallagher and D. deWaal. Fast and precise regular approximation of logic programs. In P. Van Hentenryck, editor, Proceedings of the International Conference on Logic Programming (ICLP'94), Santa Margherita Ligure, Italy. MIT Press, 1994.

Digital Library

[22]

J. P. Gallagher, M. Codish, and E. Shapiro. Specialisation of Prolog and FCP programs using abstract interpretation. New Generation Computing, 6:159--186, 1988.

Digital Library

[23]

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey. Failure tabled constraint logic programming by interpolation. TPLP, 13(4--5):593--607, 2013.

[24]

S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko. Hsf(c): A software verifier based on Horn clauses - (competition contribution). In C. Flanagan and B. König, editors, TACAS, volume 7214 of LNCS, pages 549--551. Springer, 2012.

Digital Library

[25]

A. Gupta and A. Rybalchenko. Invgen: An efficient invariant generator. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of LNCS, pages 634--640. Springer, 2009. ISBN 978-3-642-02657-7.

Digital Library

[26]

A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over li+uif. In H. Yang, editor, APLAS, volume 7078 of LNCS, pages 188--203. Springer, 2011. ISBN 978-3-642-25317-1.

Digital Library

[27]

N. Halbwachs, Y. E. Proy, and P. Raymound. Verification of linear hybrid systems by means of convex approximations. In Proceedings of the First Symposium on Static Analysis, volume 864 of LNCS, pages 223--237, September 1994.

[28]

J. Jaffar and M. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19/20:503--581, 1994.

[29]

J. Jaffar, J. A. Navas, and A. E. Santosa. Unbounded symbolic execution for program verification. In S. Khurshid and K. Sen, editors, RV, volume 7186 of LNCS, pages 396--411. Springer, 2011.

Digital Library

[30]

N. Jones, C. Gomard, and P. Sestoft. Partial Evaluation and Automatic Software Generation. Prentice Hall, 1993.

Digital Library

[31]

N. D. Jones. Combining abstract interpretation and partial evaluation. In P. Van Hentenryck, editor, Symposium on Static Analysis (SAS'97), volume 1302 of Springer-Verlag LNCS, pages 396--405, 1997.

Digital Library

[32]

H. J. Komorowski. An introduction to partial deduction. In A. Pettorossi, editor, META, volume 649 of LNCS, pages 49--69. Springer, 1992. ISBN 3--540--56282--6.

Digital Library

[33]

L. Lafave and J. P. Gallagher. Partial evaluation of functional logic programs in rewriting-based languages. In N. Fuchs, editor, Logic Program Synthesis and Transformation (LOPSTR'97), Springer-Verlag LNCS, 1998.

[34]

L. Lakhdar-Chaouch, B. Jeannet, and A. Girault. Widening with thresholds for programs with complex control graphs. In T. Bultan and P.-A. Hsiung, editors, ATVA 2011, volume 6996 of LNCS, pages 492--502. Springer, 2011.

Digital Library

[35]

M. Leuschel. Advanced logic program specialisation. In J. Hatcliff, T. Æ. Mogensen, and P. Thiemann, editors, Partial Evaluation - Practice and Theory, volume 1706 of LNCS, pages 271--292. Springer, 1999.

Digital Library

[36]

M. Leuschel. A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst., 26(3):413--463, 2004. URL http://doi.acm.org/10.1145/982158.982159.

Digital Library

[37]

M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, LOPSTR'99, volume 1817 of LNCS, pages 62--81. Springer, 1999.

Digital Library

[38]

A. Lisitsa and A. P. Nemytykh. Reachability analysis in verification via supercompilation. Int. J. Found. Comput. Sci., 19(4):953--969, 2008. . URL http://dx.doi.org/10.1142/S0129054108006066.

[39]

K. Marriott, L. Naish, and J.-L. Lassez. Most specific logic programs. In Proc. Fifth International Conference on Logic programming, Seattle, WA. MIT Press, 1988.

[40]

D. Monniaux and L. Gonnord. Using bounded model checking to focus fixpoint iterations. In E. Yahav, editor, Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14--16, 2011. Proceedings, volume 6887 of LNCS, pages 369--385. Springer, 2011. ISBN 978--3--642--23701-0.

Digital Library

[41]

J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In M. Leuschel, editor, LOPSTR, volume 2664 of LNCS, pages 90--108. Springer, 2002. ISBN 3--540--40438--4.

Digital Library

[42]

A. Pettorossi and M. Proietti. Perfect model checking via unfold/fold transformations. In J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.- K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors, Computational Logic, volume 1861 of LNCS, pages 613--628. Springer, 2000.

Digital Library

[43]

A. Podelski and A. Rybalchenko. ARMC: the logical choice for software model checking with abstraction refinement. In M. Hanus, editor, Practical Aspects of Declarative Languages, 9th International Symposium, PADL 2007, Nice, France, January 14--15, 2007., volume 4354 of LNCS, pages 245--259. Springer, 2007. ISBN 978-3-540-69608-7. URL http://dx.doi.org/10.1007/978-3-540-69611-7 16.

Digital Library

[44]

V. F. Turchin. The use of metasystem transition in theorem proving and program optimization. In J.W. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, July 14--18, 1980, Proceedings, volume 85 of LNCS, pages 645--657. Springer, 1980. ISBN 3-540-10003-2. . URL http://dx.doi.org/10.1007/3-540-10003-2 105.

Digital Library

Cited By

Yoon YLee WYi K(2023)Inductive Program Synthesis via Iterative Forward-Backward Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35912887:PLDI(1657-1681)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591288
Kafle BGallagher J(2017)Horn clause verification with convex polyhedral abstraction and tree automata-based refinementComputer Languages, Systems & Structures10.1016/j.cl.2015.11.00147(2-18)Online publication date: Jan-2017
https://doi.org/10.1016/j.cl.2015.11.001
Bakhirkin AMonniaux D(2017)Combining Forward and Backward Abstract Interpretation of Horn ClausesStatic Analysis10.1007/978-3-319-66706-5_2(23-45)Online publication date: 19-Aug-2017
https://doi.org/10.1007/978-3-319-66706-5_2
Show More Cited By

Index Terms

Constraint Specialisation in Horn Clause Verification

Recommendations

Reducing the overhead of assertion run-time checks via static analysis
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

In order to aid in the process of detecting incorrect program behaviors, a number of approaches have been proposed which include a combination of language-level constructs (such as procedure-level assertions/contracts, program-point assertions, gradual ...
Logical Inference of Horn Clauses in Petri Net Models

Petri net models for the Horn clause form of propositional logic and of first-order predicate logic are studied. A net model for logical inconsistency check is proposed. Algorithms for computing T-invariants of Petri net models of logical inference ...
Horn clause computability
Abstract
It is proved that a Turing computable functionf is computable in binary Horn clauses, which are a subset of first order logic. Moreover, it is proved that the binary Horn clauses do not need more than one function symbol. The proofs comprise ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation

January 2015

152 pages

ISBN:9781450332972

DOI:10.1145/2678015

Program Chairs:
Kenichi Asai
Ochanomizu University, Japan
,
Kostis Sagonas
Uppsala University, Sweden / NTUA, Greece

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Funding Sources

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

PEPM '15 Paper Acceptance Rate 14 of 27 submissions, 52%;

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
105
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yoon YLee WYi K(2023)Inductive Program Synthesis via Iterative Forward-Backward Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35912887:PLDI(1657-1681)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591288
Kafle BGallagher J(2017)Horn clause verification with convex polyhedral abstraction and tree automata-based refinementComputer Languages, Systems & Structures10.1016/j.cl.2015.11.00147(2-18)Online publication date: Jan-2017
https://doi.org/10.1016/j.cl.2015.11.001
Bakhirkin AMonniaux D(2017)Combining Forward and Backward Abstract Interpretation of Horn ClausesStatic Analysis10.1007/978-3-319-66706-5_2(23-45)Online publication date: 19-Aug-2017
https://doi.org/10.1007/978-3-319-66706-5_2
Kafle BGallagher J(2016)Interpolant Tree Automata and their Application in Horn Clause VerificationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.216.6216(104-117)Online publication date: 6-Jul-2016
https://doi.org/10.4204/EPTCS.216.6
De Angelis EFioravanti FPettorossi AProietti M(2016)Relational Verification Through Horn Clause TransformationStatic Analysis10.1007/978-3-662-53413-7_8(147-169)Online publication date: 31-Aug-2016
https://doi.org/10.1007/978-3-662-53413-7_8
Kafle BGallagher JMorales J(2016)Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree AutomataComputer Aided Verification10.1007/978-3-319-41528-4_14(261-268)Online publication date: 13-Jul-2016
https://doi.org/10.1007/978-3-319-41528-4_14
Kafle BGallagher JGanty P(2015)Decomposition by tree dimension in Horn clause verificationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.199.1199(1-14)Online publication date: 7-Dec-2015
https://doi.org/10.4204/EPTCS.199.1
De Angelis EFioravanti FPettorossi AProietti MFalaschi MAlbert E(2015)Semantics-based generation of verification conditions by program specializationProceedings of the 17th International Symposium on Principles and Practice of Declarative Programming10.1145/2790449.2790529(91-102)Online publication date: 14-Jul-2015
https://dl.acm.org/doi/10.1145/2790449.2790529
Bjørner NGurfinkel AMcMillan KRybalchenko A(2015)Horn Clause Solvers for Program VerificationFields of Logic and Computation II10.1007/978-3-319-23534-9_2(24-51)Online publication date: 5-Sep-2015
https://doi.org/10.1007/978-3-319-23534-9_2

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten