Advances in Property-Based Testing for \(\alpha \)Prolog

  • James CheneyEmail author
  • Alberto Momigliano
  • Matteo Pessina
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


\(\alpha \)Check is a light-weight property-based testing tool built on top of \(\alpha \)Prolog, a logic programming language based on nominal logic. \(\alpha \)Prolog is particularly suited to the validation of the meta-theory of formal systems, for example correctness of compiler translations involving name-binding, alpha-equivalence and capture-avoiding substitution. In this paper we describe an alternative to the negation elimination algorithm underlying \(\alpha \)Check that substantially improves its effectiveness. To substantiate this claim we compare the checker performances w.r.t. two of its main competitors in the logical framework niche, namely the QuickCheck/Nitpick combination offered by Isabelle/HOL and the random testing facility in PLT-Redex.


Model Check Logic Programming Clause Complementation Prolog Program Logic Programming Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. Electron. Notes Theor. Comput. Sci. 176(3), 37–59 (2007)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.F.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391–397. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. J. Log. Program. 8, 201–228 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Blanchette, J.C., Weber, T., Batty, M., Owens, S., Sarkar, S.: Nitpicking C++ concurrency. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 113–124. ACM (2011)Google Scholar
  7. 7.
    Breitner, J.: Formally proving a compiler transformation safe. In: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, Haskell 2015, pp. 35–46. ACM, New York (2015)Google Scholar
  8. 8.
    Cheney, J.: Equivariant unification. J. Autom. Reasoning 45(3), 267–300 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Cheney, J., Momigliano, A.: Mechanized metatheory model-checking. In: Leuschel, M., Podelski, A. (eds.) PPDP, pp. 75–86. ACM (2007)Google Scholar
  10. 10.
    Cheney, J., Momigliano, A., Pessina, M.: Appendix to Advances in property-based testing for \(\alpha \)Prolog (2016).
  11. 11.
    Cheney, J., Urban, C.: Nominal logic programming. ACM Trans. Program. Lang. Syst. 30(5), 26 (2008)CrossRefGoogle Scholar
  12. 12.
    Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), pp. 268–279. ACM (2000)Google Scholar
  13. 13.
    Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. The MIT Press, Massachusetts (2009)zbMATHGoogle Scholar
  14. 14.
    Fetscher, B., Claessen, K., Pałka, M., Hughes, J., Findler, R.B.: Making random judgments: automatically generating well-typed terms from the definition of a type-system. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 383–405. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  15. 15.
    Harland, J.: Success and failure for hereditary Harrop formulae. J. Log. Program. 17(1), 1–29 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2–3 Aug 2015, vol. 186. EPTCS, pp. 11–26 (2015)Google Scholar
  17. 17.
    Hritcu, C., Hughes, J., Pierce, B.C., Spector-Zabusky, A., Vytiniotis, D., Azevedo de Amorim, A., Lampropoulos, L.: Testing noninterference, quickly. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 455–468. ACM, New York (2013)Google Scholar
  18. 18.
    Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 285–296. ACM, New York (2012)Google Scholar
  19. 19.
    Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reasoning 3(3), 301–318 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Leach, J., Nieva, S., Rodríguez-Artalejo, M.: Constraint logic programming with hereditary Harrop formulas. TPLP 1(4), 409–445 (2001)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  22. 22.
    Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Loveland, W.D., Nadathur, G.: Proof procedures for logic programming. Technical report, Durham, NC, USA (1994)Google Scholar
  24. 24.
    McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100–107 (1998)Google Scholar
  25. 25.
    Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, p. 411. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  27. 27.
    Momigliano, A., Pfenning, F.: Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. 4(4), 493–529 (2003)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Nipkow, T., Klein, G.: Concrete Semantics-with Isabelle/HOL. Springer, Heidelberg (2014)zbMATHGoogle Scholar
  29. 29.
    Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)Google Scholar
  30. 30.
    Palka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an optimising compiler by generating random lambda terms. In: AST 2011, pp. 91–97. ACM (2011)Google Scholar
  31. 31.
    Paraskevopoulou, Z., Hritcu, C., Dénès, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving. LNCS, vol. 9236, pp. 325–343. Springer, Heidelberg (2015)Google Scholar
  32. 32.
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 183, 165–193 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal Isabelle. Log. Methods Comput. Sci. 8(2), 1–35 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996)CrossRefGoogle Scholar
  35. 35.
    Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1–22:50 (2013)MathSciNetzbMATHGoogle Scholar
  36. 36.
    Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in c compilers. In: PLDI 2011, pp. 283–294. ACM, New York (2011)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • James Cheney
    • 1
    Email author
  • Alberto Momigliano
    • 2
  • Matteo Pessina
    • 2
  1. 1.University of EdinburghEdinburghUK
  2. 2.Università degli Studi di MilanoMilanItaly

Personalised recommendations