Projects per year
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 | |
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 |
Keywords
- cs.LO
- cs.PL
Fingerprint
Dive into the research topics of 'Advances in Property-Based Testing for αProlog'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Nominal abstract syntax: automata, mechanised metatheory, and type theory
1/10/08 → 15/12/16
Project: Research