Analysis and transformation of constrained Horn clauses for program verification. (English) Zbl 1541.68215
Summary: This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N17 | Logic programming |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Keywords:
program verification; program analysis; program transformation; constrained Horn clauses; constraint logic programmingSoftware:
VeriMAP; Isabelle/HOL; Eiffel; JML; z3; CVC4; LOGEN; ProVerif; Why3; RAHFT; Ciao; SeaHorn; TRACER; WhyML; PRISM; Coq; Boolector; MathSAT5; Spacer; Apron; PrologCheck; ATGen; K tool; SMT-LIB; eThor; CoVaC; Boogie; ECCE; Yices; K Prover; CiaoPP; DART; OCaml; ProbLog; PPL; JayHorn; QuickCheckReferences:
| [1] | Albarghouthi, A.2017. Probabilistic Horn clause verification. In SAS 2017. LNCS 10422. Springer, 1-22. · Zbl 1420.68059 |
| [2] | Albert, E., Arenas, P., Genaim, S. and Puebla, G.2011. Closed-form upper bounds in static cost analysis. Journal of Automated Reasoning 46, 2, 161-203. · Zbl 1213.68200 |
| [3] | Albert, E., Arenas, P., Genaim, S., Puebla, G. and Zanardini, D.2007. Cost analysis of Java bytecode. In ESOP 2007. LNCS 4421. Springer, 157-172. · Zbl 1236.68042 |
| [4] | Albert, E., Arenas, P., Genaim, S., Puebla, G. and Zanardini, D.2008. Removing useless variables in cost analysis of Java bytecode. In ACM SAC - Software Verification Track (SV 2008). ACM Press, 368-375. |
| [5] | Albert, E., Arenas, P. and Gómez-Zamalloa, M.2018. Systematic testing of actor systems. Software Testing, Verification & Reliability 28, 3, e1661. · Zbl 1471.68050 |
| [6] | Albert, E., Gómez-Zamalloa, M. and Puebla, G.2010. PET: A partial evaluation-based test case generation tool for Java bytecode. In PEPM 2010. ACM Press, 25-28. |
| [7] | Alberti, F., Ghilardi, S. and Sharygina, N.2015. Decision procedures for flat array properties. Journal of Automated Reasoning 54, 4, 327-352. · Zbl 1356.03049 |
| [8] | Amaral, C., Florido, M. and Costa, V. S.2014. PrologCheck - Property-based testing in Prolog. In 12th FLOPS 2014. LNCS 8475. Springer, 1-17. |
| [9] | Apt, K. R.1990. Introduction to logic programming. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Elsevier, 493-576. · Zbl 0900.68136 |
| [10] | Apt, K. R. and Bol, R. N.1994. Logic programming and negation: A survey. Journal of Logic Programming 19, 20, 9-71. · Zbl 0942.68518 |
| [11] | Bagnara, R., Hill, P. M. and Zaffanella, E.2008. 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. |
| [12] | Bancilhon, F., Maier, D., Sagiv, Y. and Ullman, J.1986. Magic sets and other strange ways to implement logic programs (Extended abstract). In 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems, 1985. ACM Press, 1-15. |
| [13] | Banda, G. and Gallagher, J. P.2009. Analysis of linear hybrid systems in CLP. In LOPSTR 2008. LNCS 5438. Springer, 55-70. · Zbl 1185.68406 |
| [14] | Barbuti, R. and Giacobazzi, R.1992. A bottom-up polymorphic type inference in logic programming. Science of Computer Programming 19, 281-313. · Zbl 0774.68024 |
| [15] | Barnett, M., Chang, B.-Y. E., De Line, R., Jacobs, B. and Leino, K. R. M.2006. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects. LNCS 4111. Springer, 364-387. |
| [16] | Barras, B., Boutin, S., Cornes, C., Courant, J., Filliâtre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saibi, A. and Werner, B.1997. The Coq Proof Assistant Reference Manual: Version 6.1. Tech. Rep. RT-0203. https://hal.inria.fr/inria-00069968 |
| [17] | Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A. and Tinelli, C.2011. CVC4. In CAV 2011. LNCS 6806. Springer, 171-177. |
| [18] | Barrett, C., Fontaine, P. and Tinelli, C.2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org |
| [19] | Barrett, C. W. and Tinelli, C.2018. Satisfiability modulo theories. In Handbook of Model Checking, E. M. Clarke and et al., Eds. Springer, 305-343. · Zbl 1392.68379 |
| [20] | Barthe, G., Crespo, J. M. and Kunz, C.2011. Relational verification using product programs. In FM 2011. LNCS 6664. Springer, 200-214. |
| [21] | Basold, H., Komendantskaya, E. and Li, Y.2019. Coinduction in Uniform: Foundations for corecursive proof search with Horn clauses. In ESOP 2019. LNCS 11423. Springer, 783-813. · Zbl 1524.68183 |
| [22] | Benoy, F. and King, A.1997. Inferring argument size relationships with CLP(R). In LOPSTR 1996. LNCS 1207. Springer, 204-223. |
| [23] | Benton, N.2004. Simple relational correctness proofs for static analyses and program transformations. In POPL 2004. ACM Press, 14-25. · Zbl 1325.68057 |
| [24] | Beyene, T. A., Popeea, C. and Rybalchenko, A.2013. Solving existentially quantified horn clauses. In CAV 2013. LNCS 8044. Springer, 869-882. |
| [25] | Bjørner, N., Gurfinkel, A., Mcmillan, K. L. and Rybalchenko, A.2015. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays dedicated to Yuri Gurevich. LNCS 9300. Springer, 24-51. · Zbl 1465.68044 |
| [26] | Blanchet, B.2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends in Privacy and Security 1, 1-2, 1-135. |
| [27] | Blazy, S. and Leroy, X.2009. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning 43, 3, 263-288. · Zbl 1185.68136 |
| [28] | Borralleras, C., Lucas, S., Oliveras, A., Rodrguez-Carbonell, E. and Rubio, A.2012. SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning 48, 1, 107-131. · Zbl 1243.68210 |
| [29] | Bradley, A. R.2011. SAT-based model checking without unrolling. In VMCAI 2011. LNCS 6538. Springer, 70-87. · Zbl 1317.68109 |
| [30] | Bradley, A. R. and Manna, Z.2007. The Calculus of Computation. Springer. · Zbl 1126.03001 |
| [31] | Brain, M., D’Silva, V., Griggio, A., Haller, L. and Kroening, D.2014. Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design 45, 2, 213-245. · Zbl 1317.68110 |
| [32] | Brough, D. R. and Hogger, C. J.1991. Grammar-related transformations of logic programs. New Generation Computing 9, 1, 115-134. · Zbl 0722.68019 |
| [33] | Brummayer, R. and Biere, A.2009. Boolector: An efficient SMT solver for bit-vectors and arrays. In TACAS 2009. LNCS 5505. Springer, 174-177. |
| [34] | Bueno, F., Deransart, P., Drabent, W., Ferrand, G., Hermenegildo, M., Maluszynski, J. and Puebla, G.1997. On the role of semantic approximations in validation and diagnosis of constraint logic programs. In 3rd Workshop on Automated Debugging - AADEBUG 1997. Univ. of Linköping Press, Linköping, Sweden, 155-170. |
| [35] | Bulyonkov, M. A.1984. Polyvariant mixed computation for analyzer programs. Acta Informatica 21, 473-484. · Zbl 0544.68005 |
| [36] | Bundy, A.2001. The automation of proof by mathematical induction. In Handbook of Automated Reasoning (I), Robinson, A. and Voronkov, A., Eds. North Holland, 845-911. · Zbl 0994.03007 |
| [37] | Burn, T. C., Ong, C. L. and Ramsay, S. J.2018. Higher-order constrained Horn clauses for verification. In Proceedings of the ACM on Programming Languages 2, POPL 2018, 11:1-11:28. |
| [38] | Burstall, R. M. and Darlington, J.1977. A transformation system for developing recursive programs. Journal of the ACM 24, 1, 44-67. · Zbl 0343.68014 |
| [39] | Casso, I., Morales, J. F., López-Garca, P. and Hermenegildo, M.2019. An integrated approach to assertion-based random testing in Prolog. In LOPSTR 2019. LNCS 12042. Springer, 159-176. · Zbl 1502.68061 |
| [40] | Champion, A., Chiba, T., Kobayashi, N. and Sato, R.2020. ICE-based refinement type discovery for higher-order functional programs. Journal of Automated Reasoning 64, 7, 1393-1418. · Zbl 1468.68059 |
| [41] | Chen, J., Wei, J., Feng, Y., Bastani, O. and Dillig, I.2019. Relational verification using reinforcement learning. Proceedings of the ACM on Programming Languages 3, OOPSLA, 141:1-141:30. |
| [42] | Churchill, B. R., Padon, O., Sharma, R. and Aiken, A.2019. Semantic program alignment for equivalence checking. In PLDI 2019. ACM Press, 1027-1040. |
| [43] | Çiçek, E., Barthe, G., Gaboardi, M., Garg, D. and Hoffmann, J.2017. Relational cost analysis. In POPL 2017. ACM Press, 316-329. · Zbl 1380.68118 |
| [44] | Cimatti, A., Griggio, A., Schaafsma, B. and Sebastiani, R.2013. The MathSAT5 SMT Solver. In TACAS 2013. LNCS 7795. Springer, 93-107. · Zbl 1381.68153 |
| [45] | Claessen, K. and Hughes, J.2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In ICFP 2000. ACM Press, 268-279. |
| [46] | Clark, K. L.1978. Negation as failure. In Logic and Data Bases, Gallaire, H. and Minker, J., Eds. Plenum Press, New York, 293-322. |
| [47] | Clarke, E., Grumberg, O., Jha, S., Lu, Y. and Veith, H.2003. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50, 5, 752-794. · Zbl 1325.68145 |
| [48] | Clarke, E. M., Grumberg, O. and Peled, D.1999. Model Checking. MIT Press. · Zbl 1423.68002 |
| [49] | Codish, M., Bruynooghe, M., Garca De La Banda, M. and Hermenegildo, M.1997. Exploiting goal independence in the analysis of logic programs. Journal of Logic Programming 32, 3, 247-261. · Zbl 0883.68027 |
| [50] | Codish, M., Dams, D. and Yardeni, E.1994. Bottom-up abstract interpretation of logic programs. Theoretical Computer Science 124, 93-125. · Zbl 0795.68038 |
| [51] | Codish, M. and Demoen, B.1995. Analyzing logic programs using “PROP”-ositional logic programs and a magic wand. Journal of Logic Programming 25, 3, 249-274. · Zbl 0871.68049 |
| [52] | Colmerauer, A.1982. Prolog and infinite trees. In Logic Programming, Clark, K. L. and Tärnlund, S.-Å., Eds. Academic Press, 231-251. |
| [53] | Coppit, D., Le, W., Sullivan, K. J., Khurshid, S. and Yang, J.2005. Software assurance by bounded exhaustive testing. IEEE Transactions on Software Engineering 31, 4, 328-339. |
| [54] | Corsini, M.-M., Musumbu, K., Rauzy, A. and Le Charlier, B.1994. Efficient bottom-up abstract interpretation of Prolog by means of constraint solving over symbolic finite domains. In PLILP 1993. LNCS 714. Springer, 75-91. · Zbl 0797.68028 |
| [55] | Cousot, P. and Cousot, R.1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In POPL 1977. ACM Press, 238-252. |
| [56] | Cousot, P. and Cousot, R.1992. Comparing the Galois connection and widening/ narrowing approaches to abstract interpretation. In PLILP 1992. LNCS 631. Springer, 269-295. · Zbl 0776.68024 |
| [57] | Cousot, P. and Halbwachs, N.1978. Automatic discovery of linear restraints among variables of a program. In POPL 1978. ACM Press, 84-96. |
| [58] | Craig, S.-J. and Leuschel, M.2003. A compiler generator for constraint logic programs. In PSI 2003. LNCS 2890. Springer, 148-161. |
| [59] | Craig, W.1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic 22, 3, 269-285. · Zbl 0079.24502 |
| [60] | Cui, B. and Warren, D. S.2000. A system for tabled constraint logic programming. In Computational Logic 2000. LNCS 1861. Springer, 478-492. · Zbl 0983.68600 |
| [61] | De Angelis, E., Fioravanti, F., Meo, M. C., Pettorossi, A. and Proietti, M.2019. Semantics and controllability of time-aware business processes. Fundamenta Informaticae 165, 205-244. · Zbl 1412.68148 |
| [62] | De Angelis, E., Fioravanti, F., Palacios, A., Pettorossi, A. and Proietti, M.2019. Property-based test case generators for free. In Tests and Proofs - TAP@FM 2019. LNCS 11823. Springer, 186-206. |
| [63] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2014a. Program verification via iterated specialization. Science of Computer Programming 95, Part 2, 149-175. |
| [64] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2014b. VeriMAP: A tool for verifying programs through transformations. In TACAS 2014. LNCS 8413. Springer, 568-574. |
| [65] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2015. Semantics-based generation of verification conditions by program specialization. In PPDP 2015. ACM Press, 91-102. |
| [66] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2016. Relational verification through Horn clause transformation. In SAS 2016. LNCS 9837. Springer, 147-169. · Zbl 1394.68227 |
| [67] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2017a. Predicate pairing with abstraction for relational verification. In LOPSTR 2017. LNCS 10855. Springer, 289-305. · Zbl 1508.68058 |
| [68] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2017b. Semantics-based generation of verification conditions via program specialization. Science of Computer Programming 147, 78-108. |
| [69] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2018a. Predicate pairing for program verification. Theory and Practice of Logic Programming 18, 2, 126-166. · Zbl 1478.68153 |
| [70] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2018b. Solving Horn clauses on inductive data types without induction. Theory and Practice of Logic Programming 18, 3-4, 452-469. · Zbl 1451.68172 |
| [71] | De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2020. Removing algebraic data types from constrained Horn clauses using difference predicates. In IJCAR 2020. Lecture Notes in Artificial Intelligence 12166. Springer, 83-102. · Zbl 07614508 |
| [72] | De Moura, L. M. and Bjørner, N.2008. Z3: An efficient SMT solver. In TACAS 2008. LNCS 4963. Springer, 337-340. |
| [73] | De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B. and Sørensen, M. H.1999. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming 41, 2-3, 231-277. · Zbl 0944.68025 |
| [74] | Debray, S. and Ramakrishnan, R.1994. Abstract interpretation of logic programs using magic transformations. Journal of Logic Programming 18, 149-176. · Zbl 0795.68037 |
| [75] | Debray, S. K. and Lin, N. W.1993. Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems 15, 5, 826-875. |
| [76] | Debray, S. K., Lin, N.-W. and Hermenegildo, M.1990. Task granularity analysis in logic programs. In ACM PLDI 1990. ACM Press, 174-188. |
| [77] | Debray, S. K., López-García, P., Hermenegildo, M. and Lin, N.-W.1997. Lower bound cost estimation for logic programs. In International Symposium on Logic Programming 1997. MIT Press, 291-305. |
| [78] | Delzanno, G. and Podelski, A.1999. Model checking in CLP. In TACAS 1999. LNCS 1579. Springer, 223-239. |
| [79] | Delzanno, G. and Podelski, A.2001. Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3, 3, 250-270. · Zbl 0991.68013 |
| [80] | Demyanova, Y., Rümmer, P. and Zuleger, F.2017. Systematic predicate abstraction using variable roles. In NASA Formal Methods. Springer Intl. Publishing, 265-281. |
| [81] | Doménech, J. J., Gallagher, J. P. and Genaim, S.2019. Control-flow refinement by partial evaluation, and its application to termination and cost analysis. Theory and Practice of Logic Programming 19, 5-6, 990-1005. · Zbl 1434.68104 |
| [82] | Donzeau-Gouge, V., Huet, G., Kahn, G. and Lang, B.1984. Programming environments based on structured editors: The MENTOR experience. In Interactive Programming Environments. McGraw-Hill, 128-140. |
| [83] | Dutertre, B.2014. Yices 2.2. In CAV 2014. LNCS 8559. Springer, 737-744. |
| [84] | Een, N., Mishchenko, A. and Brayton, R.2011. Efficient implementation of property directed reachability. In Formal Methods in Computer-Aided Design FMCAD, 125-134. |
| [85] | Enderton, H.1972. A Mathematical Introduction to Logic. Academic Press, New York. · Zbl 0298.02002 |
| [86] | Esparza, J., Kiefer, S. and Luttenberger, M.2010. Newtonian program analysis. Journal of the ACM 57, 6, 33. · Zbl 1327.68079 |
| [87] | Etalle, S. and Gabbrielli, M.1996. Transformations of CLP modules. Theoretical Computer Science 166, 101-146. · Zbl 0872.68021 |
| [88] | Fedyukovich, G., Zhang, Y. and Gupta, A.2018. Syntax-guided termination analysis. In CAV 2018, Part I. LNCS 10981. Springer, 124-143. · Zbl 1511.68076 |
| [89] | Felsing, D., Grebing, S., Klebanov, V., Rümmer, P. and Ulbrich, M.2014. Automating regression verification. In ASE 2014. ACM Press, 349-360. |
| [90] | Filliâtre, J. C. and Paskevich, A.2013. Why3 — Where programs meet provers. In ESOP 2013. LNCS 7792. Springer, 125-128. · Zbl 1435.68366 |
| [91] | Fioravanti, F., Pettorossi, A., Proietti, M. and Senni, V.2013. Controlling polyvariance for specialization-based verification. Fundamenta Informaticae 124, 4, 483-502. · Zbl 1268.68110 |
| [92] | Fioravanti, F., Pettorossi, A. and Proietti, M.2001a. Automated strategies for specializing constraint logic programs. In LOPSTR 2000. LNCS 2042. Springer, 125-146. · Zbl 1018.68502 |
| [93] | Fioravanti, F., Pettorossi, A. and Proietti, M.2001b. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In ACM Workshop VCL 2001. Technical Report DSSE-TR-2001-3. University of Southampton, UK, 85-96. |
| [94] | Fioravanti, F., Pettorossi, A. and Proietti, M.2004. Transformation rules for locally stratified constraint logic programs. In Program Development in Computational Logic. LNCS 3049. Springer, 292-340. · Zbl 1080.68010 |
| [95] | Fioravanti, F., Pettorossi, A., Proietti, M. and Senni, V.2012. Improving reachability analysis of infinite state systems by specialization. Fundamenta Informaticae 119, 3-4, 281-300. · Zbl 1279.68209 |
| [96] | Fioravanti, F., Pettorossi, A., Proietti, M. and Senni, V.2013a. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming 13, 2, 175-199. · Zbl 1267.68080 |
| [97] | Fioravanti, F., Pettorossi, A., Proietti, M. and Senni, V.2013b. Proving theorems by program transformation. Fundamenta Informaticae 127, 1-4, 115-134. · Zbl 1315.03019 |
| [98] | Fioravanti, F., Proietti, M. and Senni, V.2015. Efficient generation of test data structures using constraint logic programming and program transformation. Journal of Logic and Computation 25, 6, 1263-1283. · Zbl 1328.68041 |
| [99] | Flanagan, C. and Godefroid, P.2005. Dynamic partial-order reduction for model checking software. In POPL 2005. ACM Press, 110-121. · Zbl 1369.68135 |
| [100] | Fribourg, L. and Olsén, H.1997. A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2, 3/4, 305-335. · Zbl 0889.68025 |
| [101] | Frühwirth, T.1998. Theory and practice of constraint handling rules. Journal of Logic Programming 37, 1, 95-138. · Zbl 0920.68029 |
| [102] | Futamura, Y.1971. Partial evaluation of computation process – an approach to a compiler-compiler. Systems, Computers, Controls 2(5), 45-50. |
| [103] | Gallagher, J. P.1993. Tutorial on specialisation of logic programs. In PEPM 1993. ACM Press, 88-98. |
| [104] | Gallagher, J. P., Boulanger, D. and Sağlam, H.1995. Practical model-based static analysis for definite logic programs. In International Symposium on Logic Programming MIT Press, 351-365. |
| [105] | Gallagher, J. P. and De Waal, D. A.1994. Fast and precise regular approximation of logic programs. In 11th International Conference on Logic Programming MIT Press, 599-613. |
| [106] | Gallagher, J. P., Hermenegildo, M., Kafle, B., Klemen, M., López-García, P. and Morales, J. F.2020. From big-step to small-step semantics and back with interpreter specialization. In VPT 2020. Electronic Proceedings in Theoretical Computer Science 320, 50-64. · Zbl 07453190 |
| [107] | Gange, G., Navas, J., Schachte, P., Søndergaard, H. and Stuckey, P.2013. Failure tabled constraint logic programming by interpolation. Theory and Practice of Logic Programming 13, 4-5, 593-607. · Zbl 1286.68043 |
| [108] | Gange, G., Navas, J. A., Schachte, P., Søndergaard, H. and Stuckey, P. J.2015. Horn clauses as an intermediate representation for program analysis and transformation. Theory and Practice of Logic Programming 15, 4-5, 526-542. · Zbl 1379.68089 |
| [109] | García-Contreras, I., Morales, J. F. and Hermenegildo, M.2020a. Incremental analysis of logic programs with assertions and open predicates. In LOPSTR 2019. LNCS 12042. Springer, 36-56. · Zbl 1502.68065 |
| [110] | García-Contreras, I., Morales, J. F. and Hermenegildo, M.2020b. Incremental and modular context-sensitive analysis. Theory and Practice of Logic Programming (to appear). |
| [111] | Garca De La Banda, M. and Hermenegildo, M.1993. A practical approach to the global analysis of constraint logic programs. In Logic Programming Symposium MIT Press, 437-455. |
| [112] | Garca De La Banda, M., Hermenegildo, M., Bruynooghe, M., Dumortier, V., Janssens, G. and Simoens, W.1996. Global analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 18, 5, 564-615. |
| [113] | Giannotti, F. and Hermenegildo, M.1991. A technique for recursive invariance detection and selective program specialization. In PLILP 1991. LNCS 528. Springer, 323-335. |
| [114] | Godefroid, P., Klarlund, N. and Sen, K.2005. DART: Directed automated random testing. In PLDI 2005. ACM Press, 213-223. |
| [115] | Godlin, B. and Strichman, O.2008. Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45, 6, 403-439. · Zbl 1161.68013 |
| [116] | Goguen, J. A. and Meseguer, J.1982. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy. 11-20. |
| [117] | Gómez-Zamalloa, M., Albert, E. and Puebla, G.2009. Decompilation of Java bytecode to Prolog by partial evaluation. Information and Software Technology 51, 10, 1409-1427. |
| [118] | Gómez-Zamalloa, M., Albert, E. and Puebla, G.2010. Test case generation for object-oriented imperative languages in CLP. Theory and Practice of Logic Programming 10, 4-6, 659-674. · Zbl 1209.68093 |
| [119] | Gotlieb, A., Botella, B. and Rueher, M.1998. Automatic test data generation using constraint solving techniques. In ACM Software Testing and Analysis Symposium. ACM Press, 53-62. |
| [120] | Graf, S. and Saïdi, H.1997. Construction of abstract state graphs with PVS. In CAV 1997. LNCS 1254. Springer, 72-83. |
| [121] | Grebenshchikov, S., Lopes, N. P., Popeea, C. and Rybalchenko, A.2012. Synthesizing software verifiers from proof rules. In PLDI 2012. ACM Press, 405-416. |
| [122] | Grishchenko, I., Maffei, M. and Schneidewind, C.2018. Foundations and tools for the static analysis of Ethereum smart contracts. In CAV 2018, Part I. LNCS 10981. Springer, 51-78. |
| [123] | Gulwani, S., Jain, S. and Koskinen, E.2009. Control-flow refinement and progress invariants for bound analysis. In PLDI 2009. ACM Press, 375-385. |
| [124] | Gupta, G., Bansal, A., Min, R., Simon, L. and Mallya, A.2007. Coinductive logic programming and its applications. In ICLP 2007. LNCS 4670. Springer, 27-44. · Zbl 1213.68177 |
| [125] | Gurfinkel, A., Kahsai, T., Komuravelli, A. and Navas, J. A.2015. The SeaHorn verification framework. In CAV 2015. LNCS 9206. Springer, 343-361. |
| [126] | Hamza, J., Voirol, N. and Kunčak, V.2019. System FR: Formalized foundations for the Stainless verifier. Proceedings of the ACM on Programming Languages 3, OOPSLA, 166:1-166:30. |
| [127] | Heizmann, M., Hoenicke, J. and Podelski, A.2009. Refinement of trace abstraction. In SAS 2009. LNCS 5673. Springer, 69-85. · Zbl 1248.68146 |
| [128] | Henriksen, K. S. and Gallagher, J. P.2006. Abstract interpretation of PIC programs through logic programming. In SCAM 2006. IEEE Computer Society, 184-196. |
| [129] | Hermenegildo, M., Bueno, F., Carro, M., López-García, P., Mera, E., Morales, J. F. and Puebla, G.2012. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming 12, 1-2, 219-252. · Zbl 1244.68019 |
| [130] | Hermenegildo, M., Puebla, G. and Bueno, F.1999. Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging. In The Logic Programming Paradigm:A 25-Year Perspective. Springer, 161-192. · Zbl 0979.68554 |
| [131] | Hermenegildo, M., Puebla, G., Bueno, F. and López-García, P.2005. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Science of Computer Programming 58, 1-2, 115-140. · Zbl 1076.68540 |
| [132] | Hermenegildo, M., Puebla, G., Marriott, K. and Stuckey, P.2000. Incremental analysis of constraint logic programs. ACM TOPLAS 22, 2, 187-223. |
| [133] | Hermenegildo, M., Warren, R. and Debray, S. K.1992. Global flow analysis as a practical compilation tool. Journal of Logic Programming 13, 4, 349-367. |
| [134] | Hoare, C. A. R.1969. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 583. · Zbl 0179.23105 |
| [135] | Hoder, K. and Bjørner, N.2012. Generalized property directed reachability. In SAT 2012. LNCS 7317. Springer, 157-171. · Zbl 1273.68229 |
| [136] | Hojjat, H. and Rümmer, P.2018. The ELDARICA Horn solver. In Formal Methods in Computer Aided Design 2018. IEEE, 1-7. |
| [137] | Jacobs, D., Langen, A. and Winsborough, W.1990. Multiple specialization of logic programs with run-time tests. In International Conference on Logic Programming. MIT Press, 718-731. |
| [138] | Jaffar, J.1984. Efficient unification over infinite terms. New Gener. Comput. 2, 3, 207-219. |
| [139] | Jaffar, J. and Lassez, J.-L.1987. Constraint logic programming. In POPL 1987. ACM Press, 111-119. |
| [140] | Jaffar, J. and Maher, M.1994. Constraint logic programming: A survey. Journal of Logic Programming 19/20, 503-581. |
| [141] | Jaffar, J., Maher, M., Marriott, K. and Stuckey, P.1998. The semantics of constraint logic programs. Journal of Logic Programming 37, 1-46. · Zbl 0920.68068 |
| [142] | Jaffar, J., Michaylov, S., Stuckey, P. J. and Yap, R. H. C.1992. The CLP(R) language and system. ACM Transactions on Programming Languages and Systems 14, 3, 339-395. |
| [143] | Jaffar, J., Murali, V., Navas, J. A. and Santosa, A. E.2012. TRACER: A symbolic execution tool for verification. In CAV 2012. LNCS 7358. Springer, 758-766. · Zbl 1478.68164 |
| [144] | Jaffar, J., Santosa, A. and Voicu, R.2009. An interpolation method for CLP traversal. In CP 2009. LNCS 5732. Springer, 454-469. |
| [145] | Jaffar, J., Santosa, A. E. and Voicu, R.2004. A CLP proof method for timed automata. In IEEE Real-Time Systems Symposium. IEEE Computer Society, 175-186. |
| [146] | Jeannet, B. and Miné, A.2009. Apron: A library of numerical abstract domains for static analysis. In CAV 2009. LNCS 5643. Springer, 661-667. |
| [147] | Jhala, R. and Majumdar, R.2009. Software model checking. ACM Computing Surveys 41, 4, 21:1-21:54. · Zbl 1507.68188 |
| [148] | Jones, N. D., Gomard, C. K. and Sestoft, P.1993. Partial Evaluation and Automatic Program Generation. Prentice Hall. · Zbl 0875.68290 |
| [149] | Jovanovic, D. and De Moura, L.2012. Solving non-linear arithmetic. In IJCAR 2012. LNCS 7364. Springer, 339-354. · Zbl 1358.68257 |
| [150] | Kafle, B. and Gallagher, J. P.2017a. Constraint specialisation in Horn clause verification. Science of Computer Programming 137, 125-140. |
| [151] | Kafle, B. and Gallagher, J. P.2017b. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems and Structures 47, 2-18. · Zbl 1379.68239 |
| [152] | Kafle, B., Gallagher, J. P., Gange, G., Schachte, P., Søndergaard, H. and Stuckey, P. J.2018. An iterative approach to precondition inference using constrained Horn clauses. Theory and Practice of Logic Programming 18, 3-4, 553-570. · Zbl 1451.68075 |
| [153] | Kafle, B., Gallagher, J. P. and Ganty, P.2018. Tree dimension in verification of constrained Horn clauses. Theory and Practice of Logic Programming 18, 2, 224-251. · Zbl 1478.68165 |
| [154] | Kafle, B., Gallagher, J. P. and Morales, J. F.2016. RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In CAV 2016, Part I. LNCS 9779. Springer, 261-268. |
| [155] | Kahn, G.1987. Natural semantics. LNCS 247. Springer, 22-39. · Zbl 0635.68007 |
| [156] | Kahsai, T., Rümmer, P., Sanchez, H. and Schäf, M.2016. JayHorn: A framework for verifying Java programs. In CAV 2016, Part I. LNCS 9779. Springer, 352-358. |
| [157] | Kalra, S., Goel, S., Dhawan, M. and Sharma, S.2018. Zeus: Analyzing safety of smart contracts. In 25th Network and Distributed System Security Symposium The Internet Society, 1-15. |
| [158] | Kanamori, T.1993. Abstract interpretation based on Alexander templates. Journal of Logic Programming 15, 1&2, 31-54. · Zbl 0787.68020 |
| [159] | Kelly, A., Marriott, K., Søndergaard, H. and Stuckey, P.1998. A practical object-oriented analysis engine for CLP. Software: Practice and Experience 28, 2, 188-224. |
| [160] | Khedker, U. P. and Karkare, B.2008. Efficiency, precision, simplicity, and generality in interprocedural data flow analysis: Resurrecting the classical call strings method. In CC 2008. LNCS 4959. Springer, 213-228. |
| [161] | Kimmig, A., Demoen, B., Raedt, L. D., Costa, V. S. and Rocha, R.2011. On the implementation of the probabilistic logic programming language ProbLog. Theory and Practice of Logic Programming 11, 2-3, 235-262. · Zbl 1220.68037 |
| [162] | Kirkeby, M. H.2019. Probabilistic output analyses for deterministic programs - reusing existing non-probabilistic analyses. Electronic Proceedings in Theoretical Computer Science 312, 43-57. |
| [163] | Klemen, M., Stulova, N., López-García, P., Morales, J. F. and Hermenegildo, M.2018. Static performance guarantees for programs with run-time checks. In PPDP 2018. ACM Press, 1-13. |
| [164] | Komuravelli, A., Gurfinkel, A. and Chaki, S.2016. SMT-based model checking for recursive programs. Formal Methods in System Design 48, 3, 175-205. · Zbl 1358.68072 |
| [165] | Komuravelli, A., Gurfinkel, A., Chaki, S. and Clarke, E. M.2013. Automatic abstraction in SMT-based unbounded software model checking. In CAV 2013. LNCS 8044. Springer, 846-862. |
| [166] | Kowalski, R. and Kuehner, D.1971. Linear resolution with selection function. Artificial Intelligence 2, 227-260. · Zbl 0234.68037 |
| [167] | Lahiri, S. K., Mcmillan, K. L., Sharma, R. and Hawblitzel, C.2013. Differential assertion checking. In ESEC/FSE 2013. ACM Press, 345-355. |
| [168] | Le Charlier, B. and Van Hentenryck, P.1994. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. ACM TOPLAS 16, 1, 35-101. |
| [169] | Leavens, G. T., Baker, A. L. and Ruby, C.2006. Preliminary design of JML: A behavioral interface specification language for Java. Software Engineering Notes 31, 3, 1-38. |
| [170] | Leino, K. R. M.2013. Developing verified programs with Dafny. In International Conference on Software Engineering 2013. IEEE Press, 1488-1490. |
| [171] | Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D. and Vouillon, J.2017. The OCaml system, Release 4.06. Documentation and user’s manual, Institut National de Recherche en Informatique et en Automatique, France. |
| [172] | Leuschel, M. and Bruynooghe, M.2002. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2, 4&5, 461-515. · Zbl 1105.68331 |
| [173] | Leuschel, M. and De Schreye, D.1998. Constrained partial deduction and the preservation of characteristic trees. New Generation Computing 16, 3, 283-342. |
| [174] | Leuschel, M., Elphick, D., Varea, M., Craig, S., and Fontaine, M.2006. The Ecce and Logen partial evaluators and their web interfaces. In PEPM 2006. ACM Press, 88-94. |
| [175] | Leuschel, M. and Lehmann, H.2000. Coverability of reset Petri nets and other well-structured transition systems by partial deduction. In CL 2000. Lecture Notes in Artificial Intelligence 1861. Springer, 101-115. · Zbl 0983.68135 |
| [176] | Leuschel, M., Martens, B. and De Schreye, D.1998. Controlling generalization and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems 20, 1, 208-258. |
| [177] | Leuschel, M. and Massart, T.2000. Infinite state model checking by abstract interpretation and program specialisation. In LOPSTR 1999. LNCS 1817. Springer, 63-82. · Zbl 0964.68086 |
| [178] | Leuschel, M. and Sørensen, M. H.1996. Redundant argument filtering of logic programs. In LOPSTR 1996. LNCS 1207. Springer, 83-103. |
| [179] | Leuschel, M. and Vidal, G.2005. Forward slicing by conjunctive partial deduction and argument filtering. In ESOP 2005. LNCS 3444. Springer, 61-76. · Zbl 1108.68424 |
| [180] | Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C. W. and Deters, M.2016. An efficient SMT solver for string constraints. Formal Methods in System Design 48, 3, 206-234. · Zbl 1404.68135 |
| [181] | Liqat, U., Georgiou, K., Kerrison, S., López-García, P., Hermenegildo, M., Gallagher, J. P., and Eder, K.2016. Inferring parametric energy consumption functions at different software levels: ISA vs. LLVM IR. In FOPARA 2015. LNCS 9964. Springer, 81-100. |
| [182] | Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., López-García, P., Grech, N., Hermenegildo, M. and Eder, K.2014. Energy consumption analysis of programs based on XMOS ISA-level models. In LOPSTR 2013. LNCS 8901. Springer, 72-90. |
| [183] | Lloyd, J.1987. Foundations of Logic Programming. Springer. 2nd Extended Edition. · Zbl 0668.68004 |
| [184] | Lloyd, J. W. and Shepherdson, J. C.1991. Partial evaluation in logic programming. Journal of Logic Programming 11, 217-242. · Zbl 0741.68030 |
| [185] | Lopes, N. P. and Monteiro, J.2016. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. International Journal on Software Tools for Technology Transfer 18, 4, 359-374. |
| [186] | López-García, P., Darmawan, L., Bueno, F. and Hermenegildo, M.2012. Interval-based resource usage verification: Formalization and prototype. In FOPARA 2011. LNCS 7177. Springer, 54-71. · Zbl 1367.68067 |
| [187] | López-García, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F. and Hermenegildo, M.2018. Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption. Theory and Practice of Logic Programming 18, 2, 167-223. · Zbl 1478.68170 |
| [188] | López-García, P., Haemmerlé, R., Klemen, M., Liqat, U. and Hermenegildo, M.2015. Towards energy consumption verification via static analysis. In HIP3ES Workshop. arXiv:1512.09369. · Zbl 1475.68087 |
| [189] | López-García, P., Klemen, M., Liqat, U. and Hermenegildo, M.2016. A general framework for static profiling of parametric resource usage. Theory and Practice of Logic Programming 16, 5-6, 849-865. · Zbl 1379.68097 |
| [190] | Madhusudan, P., Parlato, G. and Qiu, X.2011. Decidable logics combining heap structures and data. In POPL 2011. ACM Press, 611-622. · Zbl 1284.68411 |
| [191] | Marriott, K. and Søndergaard, H.1988. Bottom-up abstract interpretation of logic programs. In Conference and Symposium on Logic Programming. MIT Press, 733-748. |
| [192] | Martens, B. and Gallagher, J. P.1995. Ensuring global termination of partial deduction while allowing flexible polyvariance. In ICLP 1995. MIT Press, 597-611. |
| [193] | Matiyasevich, J. V.1970. Enumerable sets are diophantine. Doklady Akademii Nauk SSSR 191, 279-282. In English: Soviet Mathematics-Doklady, 11 (1970), 354-357. · Zbl 0212.33401 |
| [194] | Mcmillan, K. L.2013. Logic as the lingua franca of software verification. Invited talk at the VMCAI 2013, Rome, Italy. Slides at https://studylib.net/doc/9889611/ |
| [195] | Mcmillan, K. L. and Rybalchenko, A.2013. Solving constrained Horn clauses using interpolation. MSR Tech. Rep. 2013-6, Microsoft Research, Redmond, WA, USA. |
| [196] | Mendelson, E.1997. Introduction to Mathematical Logic. Chapman&Hall. 4th Edition. · Zbl 0915.03002 |
| [197] | Méndez-Lojo, M., Navas, J. and Hermenegildo, M.2007. A flexible (C)LP-based approach to the analysis of object-oriented programs. In LOPSTR 2007. LNCS 4915. Springer, 154-168. · Zbl 1179.68030 |
| [198] | Mesnard, F., Payet, É. and Vidal, G.2020. Concolic testing in CLP. Theory Pract. Log. Program. 20,5, 671-686. · Zbl 1468.68055 |
| [199] | Meudec, C.2001. ATGen: Automatic test data generation using constraint logic programming and symbolic execution. Software Testing, Verification & Reliability 11, 2, 81-96. |
| [200] | Meyer, B.1988. Object-oriented Software Construction. Prentice Hall. |
| [201] | Monniaux, D.2000. Abstract interpretation of probabilistic semantics. In SAS 2000. LNCS 1824. Springer, 322-339. · Zbl 0966.68111 |
| [202] | Mordvinov, D. and Fedyukovich, G.2017. Synchronizing constrained Horn clauses. In LPAR-21. EPiC Series in Computing, vol. 46. EasyChair, 338-355. · Zbl 1403.68243 |
| [203] | Mordvinov, D. and Fedyukovich, G.2019. Property directed inference of relational invariants. In Formal Methods in Computer Aided Design 2019. IEEE, 152-160. |
| [204] | Muthukumar, K. and Hermenegildo, M.1990. Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Techn. Rep. ACT-DC-153-90, MCC, Austin, TX 78759. |
| [205] | Muthukumar, K. and Hermenegildo, M.1992. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming 13, 2/3, 315-347. · Zbl 0776.68032 |
| [206] | Navas, J., Méndez-Lojo, M. and Hermenegildo, M.2008. Safe upper-bounds inference of energy consumption for Java bytecode applications. In NASA Langley Formal Methods Workshop, 29-32. |
| [207] | Navas, J., Méndez-Lojo, M. and Hermenegildo, M.2009. User-definable resource usage bounds analysis for Java bytecode. In BYTECODE 2009 Workshop. Electronic Notes in Theoretical Computer Science 253, 5. Elsevier, 65-82. |
| [208] | Navas, J., Mera, E., López-García, P. and Hermenegildo, M.2007. User-definable resource bounds analysis for logic programs. In ICLP 2007. LNCS 4670. Springer, 348-363. |
| [209] | Nelson, G. and Oppen, D. C.1979. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1, 2, 245-257. · Zbl 0452.68013 |
| [210] | Nielson, H. R. and Nielson, F.1992. Semantics With Applications - A Formal Introduction. Wiley Professional Computing. Wiley. · Zbl 0875.68626 |
| [211] | Nilsson, U.1995. Abstract interpretation: A kind of magic. Theoretical Computer Science 142, 1, 125-139. · Zbl 0873.68046 |
| [212] | Nipkow, T., Wenzel, M. and Paulson, L. C.2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer. · Zbl 0994.68131 |
| [213] | Ochoa, C., Puebla, G. and Hermenegildo, M.2006. Removing superfluous versions in polyvariant specialization of Prolog programs. In LOPSTR 2005. LNCS 3901. Springer, 80-97. · Zbl 1156.68328 |
| [214] | Peralta, J. C. and Gallagher, J. P.2003. Convex hull abstractions in specialization of CLP programs. In LOPSTR 2002. LNCS 2664. Springer, 90-108. · Zbl 1278.68052 |
| [215] | Peralta, J. C., Gallagher, J. P. and Saglam, H.1998. Analysis of imperative programs through analysis of constraint logic programs. In SAS 1998. LNCS 1503. Springer, 246-261. |
| [216] | Pérez-Carrasco, V., Klemen, M., López-García, P., Morales, J. F. and Hermenegildo, M.2020. Cost analysis of smart contracts via parametric resource analysis. In SAS 2020. LNCS 12389. Springer. |
| [217] | Pettorossi, A. and Proietti, M.1994. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming 19-20, 261-320. · Zbl 0942.68528 |
| [218] | Plotkin, G.1981. A structural approach to operational semantics. Technical report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark. |
| [219] | Proietti, M. and Pettorossi, A.1993. The loop absorption and the generalization strategies for the development of logic programs and partial deduction. Journal of Logic Programming 16, 1-2, 123-161. · Zbl 0778.68025 |
| [220] | Proietti, M. and Pettorossi, A.1995. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142, 1, 89-124. · Zbl 0873.68023 |
| [221] | Puebla, G., Albert, E. and Hermenegildo, M.2006. Abstract interpretation with specialized definitions. In SAS 2006. LNCS 4134. Springer, 107-126. · Zbl 1225.68076 |
| [222] | Puebla, G., Bueno, F. and Hermenegildo, M.2000. Combined static and dynamic assertion-based debugging of constraint logic programs. In LOPSTR 1999. LNCS 1817. Springer, 273-292. · Zbl 0964.68016 |
| [223] | Puebla, G. and Hermenegildo, M.1996. Optimized algorithms for the incremental analysis of logic programs. In SAS 1996. LNCS 1145. Springer, 270-284. · Zbl 1482.68075 |
| [224] | Puebla, G. and Hermenegildo, M.1999. Abstract multiple specialization and its application to program parallelization. Journal of Logic Programming 41, 2&3, 279-316. · Zbl 0944.68026 |
| [225] | Puebla, G., Hermenegildo, M. and Gallagher, J. P.1999. An integration of partial evaluation in a generic abstract interpretation framework. In ACM SIGPLAN PEPM 1999. BRISC Series NS-99-1. University of Aarhus, Denmark, 75-85. |
| [226] | Reps, T. W., Horwitz, S. and Sagiv, S.1995. Precise interprocedural dataflow analysis via graph reachability. In POPL 1995. ACM Press, 49-61. · Zbl 1496.68079 |
| [227] | Reynolds, A. and Kunčak, V.2015. Induction for SMT solvers. In VMCAI 2015. LNCS 8931. Springer, 80-98. · Zbl 1432.68418 |
| [228] | Rohmer, J., Lescoeur, R. and Kerisit, J.1986. The Alexander method - A technique for the processing of recursive axioms in deductive databases. New Generation Computing 4, 3, 273-285. · Zbl 0615.68062 |
| [229] | Rosu, G. and Serbanuta, T.2010. An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79, 6, 397-434. · Zbl 1214.68188 |
| [230] | Roychoudhury, A., Kumar, K. N., Ramakrishnan, C. R., and Ramakrishnan, I. V.2002. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal on Foundations of Computer Science 13, 3, 387-403. · Zbl 1066.68016 |
| [231] | Roychoudhury, A., Kumar, K. N., Ramakrishnan, C. R., Ramakrishnan, I. V. and Smolka, S. A.2000. Verification of parameterized systems using logic program transformations. In TACAS 2000. LNCS 1785. Springer, 172-187. · Zbl 0964.68018 |
| [232] | Rümmer, P.2020. Competition Report: CHC-COMP-20. Tech. Rep. Available at https://chc-comp.github.io/report.pdf · Zbl 07453201 |
| [233] | Sahlin, D.1993. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing 12, 7-51. · Zbl 0942.68516 |
| [234] | Sato, T. and Kameya, Y.1997. PRISM: A language for symbolic-statistical modeling. In 15th IJCAI 1997. Morgan Kaufmann, 1330-1339. |
| [235] | Schneidewind, C., Grishchenko, I., Scherer, M. and Maffei, M.2020. eThor: Practical and provably sound static analysis of Ethereum smart contracts. In CCS 2020: ACM Conference on Computer and Communications Security. ACM Press, 621-640. |
| [236] | Schrijver, A.1998. Theory of Linear and Integer Programming. John Wiley & Sons. · Zbl 0970.90052 |
| [237] | Seki, H.1991. Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107-139. · Zbl 0737.68016 |
| [238] | Seki, H.2012. Proving properties of co-logic programs by unfold/fold transformations. In LOPSTR 2011. LNCS 7225. Springer, 205-220. · Zbl 1377.68066 |
| [239] | Senni, V. and Fioravanti, F.2012. Generation of test data structures using constraint logic programming. In Tests and Proofs. LNCS 7305. Springer, 115-131. |
| [240] | Serrano, A., López-García, P. and Hermenegildo, M.2014. Resource usage analysis of logic programs via abstract interpretation using sized types. Theory and Practice of Logic Programming 14, 4-5, 739-754. · Zbl 1307.68022 |
| [241] | Sharir, M. and Pnueli, A.1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Chapter 7, 189-233. |
| [242] | Shemer, R., Gurfinkel, A., Shoham, S. and Vizel, Y.2019. Property directed self composition. In CAV 2019, Part I. LNCS 11561. Springer, 161-179. · Zbl 1533.68176 |
| [243] | Shoenfield, J. R.1967. Mathematical Logic. Addison-Wesley Publishing Company. · Zbl 0155.01102 |
| [244] | Spoto, F., Mesnard, F. and Payet, É.2010. A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems 32, 3, 8:1-8:70. |
| [245] | Suter, P., Köksal, A. S. and Kunčak, V.2011. Satisfiability modulo recursive programs. In SAS 2011. LNCS 6887. Springer, 298-315. |
| [246] | Tamaki, H. and Sato, T.1984. Unfold/fold transformation of logic programs. In ICLP 1984, S.-Å. Tärnlund, Ed. University, Uppsala, Uppsala, Sweden, 127-138. |
| [247] | Tärnlund, S.1977. Horn clause computability. BIT 17, 2, 215-226. · Zbl 0359.02042 |
| [248] | Tarski, A.1955. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285-309. · Zbl 0064.26004 |
| [249] | Thakur, M. and Nandivada, V. K.2020. Mix your contexts well: Opportunities unleashed by recent advances in scaling context-sensitivity. In Conference on Compiler Construction. ACM Press, 27-38. |
| [250] | Tsankov, P., Dan, A. M., Drachsler-Cohen, D., Gervais, A., Bünzli, F. and Vechev, M. T.2018. Securify: Practical security analysis of smart contracts. In ACM Conference on Computer and Communications Security. ACM Press, 67-82. |
| [251] | Unno, H., Torii, S. and Sakamoto, H.2017. Automating induction for solving Horn clauses. In CAV 2017, Part II. LNCS 10427. Springer, 571-591. · Zbl 1494.68064 |
| [252] | Verschaetse, K. and De Schreye, D.1992. Derivation of linear size relations by abstract interpretation. In PLILP 1992. LNCS 631. Springer, 296-310. |
| [253] | Wadler, P. L.1990. Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science 73, 231-248. · Zbl 0701.68013 |
| [254] | Wang, W. and Jiao, L.2016. Trace abstraction refinement for solving Horn clauses. The Computer Journal 59, 8, 1236-1251. |
| [255] | Warren, D. S.1992. Memoing for logic programs. Communications of the ACM 35, 3, 93-111. |
| [256] | Warren, R., Hermenegildo, M. and Debray, S. K.1988. On the practicality of global flow analysis of logic programs. In Conference and Symposium on Logic Programming. MIT Press, 684-699. |
| [257] | Wybraniec-Skardowska, U.2019. On certain axiomatizations of arithmetic of natural and integer numbers. Axioms 8, 3. doi: doi:10.3390/axioms8030103. · Zbl 1432.03124 |
| [258] | Zaks, A. and Pnueli, A.2008. CoVaC: Compiler validation by program analysis of the cross-product. In International Symposium on Formal Methods. LNCS 5014. Springer, 35-51. |
| [259] | Zhou, Q., Heath, D. and Harris, W.2019. Relational verification via invariant-guided synchronization. In HCVS/PERR@ETAPS 2019. Electronic Proceedings in Theoretical Computer Science 296, 28-41. · Zbl 1483.68216 |
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.
