ααCheck is a light-weight property-based testing tool built on top of ααProlog, a logic programming language based on nominal logic. αα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 αα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.

Advances in property-based testing for alpha prolog / J. Cheney, A. Momigliano, M. Pessina (LECTURE NOTES IN COMPUTER SCIENCE). - In: Tests and proof / [a cura di] B.K. Aichernig, C.A. Furia. - Prima edizione. - [s.l] : Springer International Publishing, 2016. - ISBN 9783319411354. - pp. 37-56 [10.1007/978-3-319-41135-4_3]

Advances in property-based testing for alpha prolog

A. Momigliano;
2016

Abstract

ααCheck is a light-weight property-based testing tool built on top of ααProlog, a logic programming language based on nominal logic. αα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 αα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.
nominal logic; model checking; counterexample search; negation elimination
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
long-tap.pdf

accesso aperto

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 425.87 kB
Formato Adobe PDF
425.87 kB Adobe PDF Visualizza/Apri
chp%3A10.1007%2F978-3-319-41135-4_3.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 432.29 kB
Formato Adobe PDF
432.29 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/411297
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 4
social impact