Skip to main content
SpringerLink
Log in

Relational Verification Through Horn Clause Transformation

  • Conference paper
  • First Online:
Static Analysis (SAS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9837))

Included in the following conference series:

Abstract

We present a method for verifying relational program properties, that is, properties that relate the input and the output of two programs. Our verification method is parametric with respect to the definition of the operational semantics of the programming language in which the two programs are written. That definition of the semantics consists of a set Int of constrained Horn clauses (CHCs) that encode the interpreter of the programming language. Then, given the programs and the relational property we want to verify, we generate, by using Int, a set of constrained Horn clauses whose satisfiability is equivalent to the validity of the property. Unfortunately, state-of-the-art solvers for CHCs have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We propose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these transformations, based on unfold/fold rules, preserve satisfiability. Through an experimental evaluation, we show that in many cases CHC solvers are able to prove the satisfiability (or the unsatisfiability) of sets of clauses obtained by applying the transformations we propose, whereas the same solvers are unable to perform those proofs when given as input the original, untransformed sets of CHCs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The sources of the problems are available at http://map.uniroma2.it/relprop.

  2. 2.

    Using the options -horn -hsmt -princess -i -abstract:oct. Running Eldarica in client-server mode could significantly improve its performance, but requires custom modifications for running multiple problems in parallel.

  3. 3.

    http://formal.iti.kit.edu/improve/reve/index.php.

References

  1. Albert, E., Gómez-Zamalloa, M., Hubert, L., Puebla, G.: Verification of java bytecode using analysis and transformation of logic programs. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 124–139. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 15–30. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  3. Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional programs by first-order refinement. In: Proceedings of PEPM 2015, pp. 61–72. ACM (2015)

    Google Scholar 

  4. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of POPL 2004, pp. 14–25. ACM (2004)

    Google Scholar 

  7. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W., Beklemishev, L.D., Beklemishev, L.D. (eds.) Gurevich Festschrift II 2015. LNCS, vol. 9300, pp. 24–51. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  8. Borralleras, C., Lucas, S., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reasoning 48(1), 107–131 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 119–135. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Ciobâcă, Ş., Lucanu, D., Rusu, V., Roşu, G.: A language-independent proof system for mutual program equivalence. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 75–90. Springer, Heidelberg (2014)

    Google Scholar 

  12. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification via iterated specialization. Sci. Comput. Program. 95(Part 2), 149–175 (2014)

    Article  Google Scholar 

  13. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae 140(3–4), 329–355 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  14. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 568–574. Springer, Heidelberg (2014). http://map.uniroma2.it/VeriMAP

    Chapter  Google Scholar 

  15. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Proving correctness of imperative programs by linearizing constrained Horn clauses. Theor. Pract. Logic Program. 15(4–5), 635–650 (2015)

    Article  MathSciNet  Google Scholar 

  16. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: Proceedings of PPDP 2015, pp. 91–102. ACM (2015)

    Google Scholar 

  17. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive partial deduction: foundations, control, algorithms, and experiments. J. Logic Program. 41(2–3), 231–277 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  19. Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theor. Comput. Sci. 166, 101–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  20. Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of ASE 2014, pp. 349–360 (2014)

    Google Scholar 

  21. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Ganty, P., Iosif, R., Konečný, F.: Underapproximation of procedure summaries for integer programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 245–259. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241–258 (2013)

    Article  Google Scholar 

  24. Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 282–299. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  25. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  27. Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Logic Program. 19(20), 503–581 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  28. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  29. Kafle, B., Gallagher, J.P.: Constraint specialisation in Horn clause verification. In: Proceedings of PEPM 2015, pp. 85–90. ACM (2015)

    Google Scholar 

  30. Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Proceedings of ESEC/FSE 2013, pp. 345–355. ACM (2013)

    Google Scholar 

  31. Matijasevic, Y.V.: Enumerable sets are diophantine. Doklady Akademii Nauk SSSR 191, 279–282 (1970). in Russian

    MathSciNet  Google Scholar 

  32. McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical report MSR-TR-2013-6, Microsoft Research, January 2013

    Google Scholar 

  33. Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–265. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  34. Peralta, J.C., Gallagher, J.P., Saglam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246–261. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  35. Pettorossi, A., Proietti, M.: Transformation of logic programs: foundations and techniques. J. Logic Program. 19(20), 261–320 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  36. Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Proceedings of ICLP 1984, pp. 127–138 (1984)

    Google Scholar 

  37. Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3), 11 (2012)

    Article  MATH  Google Scholar 

  38. Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35–51. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgements

We wish to thank A. Gurfinkel, V. Klebanov, Ph. Rümmer and the participants in the HCVS and VPT workshops at ETAPS 2016 for stimulating conversations. We also thank the anonymous referees for their very constructive comments. We acknowledge the financial support of INdAM-GNCS (Italy). E. De Angelis, F. Fioravanti, and A. Pettorossi are research associates at IASI-CNR.

Author information

Authors and Affiliations

  1. DEC, University ‘G. D’Annunzio’, Pescara, Italy

    Emanuele De Angelis & Fabio Fioravanti

  2. DICII, University of Rome Tor Vergata, Rome, Italy

    Alberto Pettorossi

  3. IASI-CNR, Rome, Italy

    Maurizio Proietti

Authors
  1. Emanuele De Angelis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Emanuele De Angelis , Alberto Pettorossi or Maurizio Proietti .

Editor information

Editors and Affiliations

  1. Ecole Normale Supérieure , Paris, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag GmbH Germany

About this paper

Cite this paper

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M. (2016). Relational Verification Through Horn Clause Transformation. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53413-7_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53412-0

  • Online ISBN: 978-3-662-53413-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation