×

Removing unnecessary variables from Horn clause verification conditions. (English) Zbl 1482.68136

Gallagher, John P. (ed.) et al., Proceedings of the third workshop on Horn clauses for verification and synthesis, HCVS 2016, Eindhoven, The Netherlands, April 3, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 219, 49-55 (2016).
Summary: Verification conditions (VCs) are logical formulas whose satisfiability guarantees program correctness. We consider VCs in the form of constrained Horn clauses (CHC) which are automatically generated from the encoding of (an interpreter of) the operational semantics of the programming language. VCs are derived through program specialization based on the unfold/fold transformation rules and, as it often happens when specializing interpreters, they contain unnecessary variables, that is, variables which are not required for the correctness proofs of the programs under verification. In this paper we adapt to the CHC setting some of the techniques that were developed for removing unnecessary variables from logic programs, and we show that, in some cases, the application of these techniques increases the effectiveness of Horn clause solvers when proving program correctness.
For the entire collection see [Zbl 1441.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science

Software:

z3; VeriMAP; SeaHorn
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] E. Albert, M. Gómez-Zamalloa, L. Hubert & G. Puebla (2007): Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In M. Hanus, editor: Practical Aspects of Declarative Languages, Lecture Notes in Computer Science 4354, Springer, pp. 124-139, doi:10.1007/978-3-540-69611-7 8. · doi:10.1007/978-3-540-69611-7_8
[2] E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): Program Verification via Iterated Special-ization. Science of Computer Programming 95, Part 2, pp. 149-175, doi:10.1016/j.scico.2014.05.017. · doi:10.1016/j.scico.2014.05.017
[3] E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’14, Lecture Notes in Computer Science 8413, Springer, pp. 568-574, doi:10.1007/978-3-642-54862-8 47. Available at: http://www.map.uniroma2.it/VeriMAP. · doi:10.1007/978-3-642-54862-8_47
[4] E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2015): Semantics-based generation of verifi-cation conditions by program specialization. In: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015, ACM, pp. 91-102, doi:10.1145/2790449.2790529. · doi:10.1145/2790449.2790529
[5] S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101-146, doi:10.1016/0304-3975(95)00148-4. · Zbl 0872.68021 · doi:10.1016/0304-3975(95)00148-4
[6] J. P. Gallagher & B. Kafle (2014): Analysis and Transformation Tools for Constrained Horn Clause Verifi-cation. Theory and Practice of Logic Programming 14(4-5), pp. 90-101. Supplementary Materials.
[7] A. Gurfinkel, T. Kahsai, A. Komuravelli & J.A. Navas (2015): The SeaHorn Verification Framework. In: Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Springer, pp. 343-361, doi:10.1007/978-3-319-21690-4 20. · doi:10.1007/978-3-319-21690-4_20
[8] K. S. Henriksen & J. P. Gallagher (2006): Abstract Interpretation of PIC Programs through Logic Program-ming. In: Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM ’06, pp. 103-179, doi:10.1109/SCAM.2006.1. · doi:10.1109/SCAM.2006.1
[9] M. Leuschel & M. H. Sørensen (1996): Redundant Argument Filtering of Logic Programs. In J. Gallagher, editor: Logic Program Synthesis and Transformation, Proceedings LOPSTR ’96, Stockholm, Sweden, Lec-ture Notes in Computer Science 1207, Springer-Verlag, pp. 83-103, doi:10.1007/3-540-62718-9 6. · doi:10.1007/3-540-62718-9_6
[10] L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’08, Lecture Notes in Computer Science 4963, Springer, pp. 337-340, doi:10.1007/978-3-540-78800-3 24. · doi:10.1007/978-3-540-78800-3_24
[11] J. C. Peralta, J. P. Gallagher & H. Saglam (1998): Analysis of Imperative Programs through Analy-sis of Constraint Logic Programs. In G. Levi, editor: Proceedings of the 5th International Sympo-sium on Static Analysis, SAS ’98, Lecture Notes in Computer Science 1503, Springer, pp. 246-261, doi:10.1007/3-540-49727-7 15. · doi:10.1007/3-540-49727-7_15
[12] M. Proietti & A. Pettorossi (1995): Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs. Theoretical Computer Science 142(1), pp. 89-124, doi:10.1016/0304-3975(94)00227-A. · Zbl 0873.68023 · doi:10.1016/0304-3975(94)00227-A
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.