Advances in Property-Based Testing for αProlog

James Cheney; Alberto Momigliano; Matteo Pessina

doi:10.1007/978-3-319-41135-4_3

Advances in Property-Based Testing for αProlog

James Cheney, Alberto Momigliano, Matteo Pessina

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Tests and Proofs
Subtitle of host publication	10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings
Publisher	Springer International Publishing
Pages	37-56
Number of pages	20
ISBN (Electronic)	978-3-319-41135-4
ISBN (Print)	978-3-319-41134-7
DOIs	https://doi.org/10.1007/978-3-319-41135-4_3
Publication status	Published - Jun 2016
Event	10th International Conference on Tests & Proofs - Vienna, Austria Duration: 5 Jul 2016 → 7 Jul 2016 http://tap2016.ist.tugraz.at/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9762
ISSN (Print)	0302-9743

Conference

Conference	10th International Conference on Tests & Proofs
Abbreviated title	TAP 2016
Country/Territory	Austria
City	Vienna
Period	5/07/16 → 7/07/16
Internet address	http://tap2016.ist.tugraz.at/

Keywords

cs.LO
cs.PL

Access to Document

10.1007/978-3-319-41135-4_3

1604.08345v1Accepted author manuscript, 475 KB

http://link.springer.com/chapter/10.1007/978-3-319-41135-4_3

Nominal abstract syntax: automata, mechanised metatheory, and type theory
Cheney, J.
Other (Learned Society)
1/10/08 → 15/12/16
Project: Research

Cite this

Cheney, J., Momigliano, A., & Pessina, M. (2016). Advances in Property-Based Testing for αProlog. In Tests and Proofs: 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings (pp. 37-56). (Lecture Notes in Computer Science; Vol. 9762). Springer International Publishing. https://doi.org/10.1007/978-3-319-41135-4_3

@inproceedings{577900c694844d7298de789079c941be,

title = "Advances in Property-Based Testing for αProlog",

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.",

keywords = "cs.LO, cs.PL",

author = "James Cheney and Alberto Momigliano and Matteo Pessina",

note = "To appear, Tests and Proofs 2016. Accepted April 15, 2016.; 10th International Conference on Tests & Proofs, TAP 2016 ; Conference date: 05-07-2016 Through 07-07-2016",

year = "2016",

month = jun,

doi = "10.1007/978-3-319-41135-4_3",

language = "English",

isbn = "978-3-319-41134-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "37--56",

booktitle = "Tests and Proofs",

url = "http://tap2016.ist.tugraz.at/",

}

Cheney, J, Momigliano, A & Pessina, M 2016, Advances in Property-Based Testing for αProlog. in Tests and Proofs: 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9762, Springer International Publishing, pp. 37-56, 10th International Conference on Tests & Proofs, Vienna, Austria, 5/07/16. https://doi.org/10.1007/978-3-319-41135-4_3

Advances in Property-Based Testing for αProlog. / Cheney, James; Momigliano, Alberto; Pessina, Matteo.

Tests and Proofs: 10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings. Springer International Publishing, 2016. p. 37-56 (Lecture Notes in Computer Science; Vol. 9762).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Advances in Property-Based Testing for αProlog

AU - Cheney, James

AU - Momigliano, Alberto

AU - Pessina, Matteo

N1 - To appear, Tests and Proofs 2016. Accepted April 15, 2016.

PY - 2016/6

Y1 - 2016/6

N2 - α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.

AB - α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.

KW - cs.LO

KW - cs.PL

U2 - 10.1007/978-3-319-41135-4_3

DO - 10.1007/978-3-319-41135-4_3

M3 - Conference contribution

SN - 978-3-319-41134-7

T3 - Lecture Notes in Computer Science

SP - 37

EP - 56

BT - Tests and Proofs

PB - Springer International Publishing

T2 - 10th International Conference on Tests & Proofs

Y2 - 5 July 2016 through 7 July 2016

ER -

Advances in Property-Based Testing for αProlog

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

Nominal abstract syntax: automata, mechanised metatheory, and type theory

Cite this