publication . Preprint . Article . 2016

Solving non-linear Horn clauses using a linear Horn clause solver

Pierre Ganty; Bishoksan Kafle; John P. Gallagher;
Open Access English
  • Published: 14 Jul 2016
Abstract
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Ho...
Read more
doi: 10.4204/eptcs.219.4
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.1, QA1-939, Electronic computers. Computer science, QA75.5-76.95, Solver, Program transformation, Unit propagation, Horn-satisfiability, Mathematics, SLD resolution, Program analysis, Discrete mathematics, Bounded function, Horn clause
Related Organizations
Funded by
EC| ENTRA
Project
ENTRA
Whole-Systems Energy Transparency
  • Funder: European Commission (EC)
  • Project Code: 318337
  • Funding stream: FP7 | SP1 | ICT
, EC| POLCA
Project
POLCA
Programming Large Scale Heterogeneous Infrastructures
  • Funder: European Commission (EC)
  • Project Code: 610686
  • Funding stream: FP7 | SP1 | ICT
, EC| ICT-ENERGY
Project
ICT-ENERGY
Co-ordinating Research Efforts of the ICT-Energy Community
  • Funder: European Commission (EC)
  • Project Code: 611004
  • Funding stream: FP7 | SP1 | ICT
Communities
FET FP7FET Proactive: FET proactive: Coordinating communities, identifying new research topics for FET Proactive initiatives and fostering interdisciplinary dialogue
FET FP7FET Proactive: Co-ordinating Research Efforts of the ICT-Energy Community
FET FP7FET Proactive: FET Proactive: Minimising Energy Consumption of Computing to the Limit (MINECC)
FET FP7FET Proactive: Whole-Systems Energy Transparency
Download fromView all 3 versions
arXiv.org e-Print Archive
Preprint . 2016
Provider: arXiv.org e-Print Archive
Electronic Proceedings in Theoretical Computer Science
Article . 2016
Provider: Crossref
Electronic Proceedings in Theoretical Computer Science
Article
Provider: UnpayWall
Electronic Proceedings in Theoretical Computer Science
Article
Provider: Microsoft Academic Graph
30 references, page 1 of 2

[1] Foto N. Afrati, Manolis Gergatsoulis & Francesca Toni (2003): Linearisability on Datalog programs. Theor. Comput. Sci. 308(1-3), pp. 199-226, doi:10.1016/S0304-3975(02)00730-2. [OpenAIRE]

[2] Roberto Bagnara, Patricia M. Hill & Enea Zaffanella (2008): The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2), pp. 3-21, doi:10.1016/j.scico.2007.08.001.

[3] Christel Baier & Cesare Tinelli, editors (2015): Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science 9035, Springer, doi:10.1007/978-3-662-46681-0.

[4] Dirk Beyer (2015): Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015). In Baier & Tinelli [3], pp. 401-416, doi:10.1007/978-3-662-46681-0 31.

[5] Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In Francesco Logozzo & Manuel Fa¨hndrich, editors: SAS, LNCS 7935, Springer, pp. 105- 125. Available at http://dx.doi.org/10.1007/978-3-642-38856-9_8. [OpenAIRE]

[6] Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Robert M. Graham, Michael A. Harrison & Ravi Sethi, editors: POPL, ACM, pp. 238-252. Available at http://doi.acm.org/10.1145/512950. 512973.

[7] Patrick Cousot & Nicolas Halbwachs (1978): POPL. ACM Press, pp. 84-96, doi:10.1145/512760.512770. Available at http://dl.acm.org/citation.cfm?id=512760.

[8] Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In Erika A´braha´m & Klaus Havelund, editors: TACAS, LNCS 8413, Springer, pp. 568-574. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_47. [OpenAIRE]

[9] Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2015): Proving correctness of imperative programs by linearizing constrained Horn clauses. TPLP 15(4-5), pp. 635-650, doi:10.1017/S1471068415000289. [OpenAIRE]

[10] Bruno Dutertre (2014): Yices 2.2. In Armin Biere & Roderick Bloem, editors: Computer-Aided Verification (CAV'2014), Lecture Notes in Computer Science 8559, Springer, pp. 737-744, doi:10.1007/978-3-319- 08867-9 49. [OpenAIRE]

[11] Javier Esparza, Pierre Ganty, Stefan Kiefer & Michael Luttenberger (2011): Parikh's theorem: A simple and direct automaton construction. Inf. Process. Lett. 111(12), pp. 614-619, doi:10.1016/j.ipl.2011.03.019.

[12] Javier Esparza, Stefan Kiefer & Michael Luttenberger (2007): On Fixed Point Equations over Commutative Semirings. In: STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, LNCS 4393, Springer, pp. 296-307, doi:10.1007/978-3-540-70918-3 26.

[13] J. P. Gallagher (1986): Transforming Logic Programs by Specialising Interpreters. In: Proceedings of the 7th European Conference on Artificial Intelligence (ECAI-86), Brighton, pp. 109-122.

[14] John P. Gallagher (1993): Tutorial on Specialisation of Logic Programs. In David A. Schmidt, editor: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'93, Copenhagen, Denmark, June 14-16, 1993, ACM, pp. 88-98, doi:10.1145/154630.154640. Available at http://dl.acm.org/citation.cfm?id=154630.

[15] Pierre Ganty, Radu Iosif & Filip Konecˇny´ (2013): Underapproximation of Procedure Summaries for Integer Programs. In Nir Piterman & Scott A. Smolka, editors: TACAS 2013. Proceedings, Lecture Notes in Computer Science 7795, Springer, pp. 245-259, doi:10.1007/978-3-642-36742-7 18.

30 references, page 1 of 2
Related research
Abstract
In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Ho...
Read more
doi: 10.4204/eptcs.219.4
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.1, QA1-939, Electronic computers. Computer science, QA75.5-76.95, Solver, Program transformation, Unit propagation, Horn-satisfiability, Mathematics, SLD resolution, Program analysis, Discrete mathematics, Bounded function, Horn clause
Related Organizations
Funded by
EC| ENTRA
Project
ENTRA
Whole-Systems Energy Transparency
  • Funder: European Commission (EC)
  • Project Code: 318337
  • Funding stream: FP7 | SP1 | ICT
, EC| POLCA
Project
POLCA
Programming Large Scale Heterogeneous Infrastructures
  • Funder: European Commission (EC)
  • Project Code: 610686
  • Funding stream: FP7 | SP1 | ICT
, EC| ICT-ENERGY
Project
ICT-ENERGY
Co-ordinating Research Efforts of the ICT-Energy Community
  • Funder: European Commission (EC)
  • Project Code: 611004
  • Funding stream: FP7 | SP1 | ICT
Communities
FET FP7FET Proactive: FET proactive: Coordinating communities, identifying new research topics for FET Proactive initiatives and fostering interdisciplinary dialogue
FET FP7FET Proactive: Co-ordinating Research Efforts of the ICT-Energy Community
FET FP7FET Proactive: FET Proactive: Minimising Energy Consumption of Computing to the Limit (MINECC)
FET FP7FET Proactive: Whole-Systems Energy Transparency
Download fromView all 3 versions
arXiv.org e-Print Archive
Preprint . 2016
Provider: arXiv.org e-Print Archive
Electronic Proceedings in Theoretical Computer Science
Article . 2016
Provider: Crossref
Electronic Proceedings in Theoretical Computer Science
Article
Provider: UnpayWall
Electronic Proceedings in Theoretical Computer Science
Article
Provider: Microsoft Academic Graph
30 references, page 1 of 2

[1] Foto N. Afrati, Manolis Gergatsoulis & Francesca Toni (2003): Linearisability on Datalog programs. Theor. Comput. Sci. 308(1-3), pp. 199-226, doi:10.1016/S0304-3975(02)00730-2. [OpenAIRE]

[2] Roberto Bagnara, Patricia M. Hill & Enea Zaffanella (2008): The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2), pp. 3-21, doi:10.1016/j.scico.2007.08.001.

[3] Christel Baier & Cesare Tinelli, editors (2015): Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science 9035, Springer, doi:10.1007/978-3-662-46681-0.

[4] Dirk Beyer (2015): Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015). In Baier & Tinelli [3], pp. 401-416, doi:10.1007/978-3-662-46681-0 31.

[5] Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In Francesco Logozzo & Manuel Fa¨hndrich, editors: SAS, LNCS 7935, Springer, pp. 105- 125. Available at http://dx.doi.org/10.1007/978-3-642-38856-9_8. [OpenAIRE]

[6] Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Robert M. Graham, Michael A. Harrison & Ravi Sethi, editors: POPL, ACM, pp. 238-252. Available at http://doi.acm.org/10.1145/512950. 512973.

[7] Patrick Cousot & Nicolas Halbwachs (1978): POPL. ACM Press, pp. 84-96, doi:10.1145/512760.512770. Available at http://dl.acm.org/citation.cfm?id=512760.

[8] Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In Erika A´braha´m & Klaus Havelund, editors: TACAS, LNCS 8413, Springer, pp. 568-574. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_47. [OpenAIRE]

[9] Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2015): Proving correctness of imperative programs by linearizing constrained Horn clauses. TPLP 15(4-5), pp. 635-650, doi:10.1017/S1471068415000289. [OpenAIRE]

[10] Bruno Dutertre (2014): Yices 2.2. In Armin Biere & Roderick Bloem, editors: Computer-Aided Verification (CAV'2014), Lecture Notes in Computer Science 8559, Springer, pp. 737-744, doi:10.1007/978-3-319- 08867-9 49. [OpenAIRE]

[11] Javier Esparza, Pierre Ganty, Stefan Kiefer & Michael Luttenberger (2011): Parikh's theorem: A simple and direct automaton construction. Inf. Process. Lett. 111(12), pp. 614-619, doi:10.1016/j.ipl.2011.03.019.

[12] Javier Esparza, Stefan Kiefer & Michael Luttenberger (2007): On Fixed Point Equations over Commutative Semirings. In: STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, LNCS 4393, Springer, pp. 296-307, doi:10.1007/978-3-540-70918-3 26.

[13] J. P. Gallagher (1986): Transforming Logic Programs by Specialising Interpreters. In: Proceedings of the 7th European Conference on Artificial Intelligence (ECAI-86), Brighton, pp. 109-122.

[14] John P. Gallagher (1993): Tutorial on Specialisation of Logic Programs. In David A. Schmidt, editor: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'93, Copenhagen, Denmark, June 14-16, 1993, ACM, pp. 88-98, doi:10.1145/154630.154640. Available at http://dl.acm.org/citation.cfm?id=154630.

[15] Pierre Ganty, Radu Iosif & Filip Konecˇny´ (2013): Underapproximation of Procedure Summaries for Integer Programs. In Nir Piterman & Scott A. Smolka, editors: TACAS 2013. Proceedings, Lecture Notes in Computer Science 7795, Springer, pp. 245-259, doi:10.1007/978-3-642-36742-7 18.

30 references, page 1 of 2
Related research
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue