Advances in Property-Based Testing for αProlog

James Cheney, Alberto Momigliano, Matteo Pessina

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationTests and Proofs
Subtitle of host publication10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings
PublisherSpringer International Publishing
Pages37-56
Number of pages20
ISBN (Electronic)978-3-319-41135-4
ISBN (Print)978-3-319-41134-7
DOIs
Publication statusPublished - Jun 2016
Event10th International Conference on Tests & Proofs - Vienna, Austria
Duration: 5 Jul 20167 Jul 2016
http://tap2016.ist.tugraz.at/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9762
ISSN (Print)0302-9743

Conference

Conference10th International Conference on Tests & Proofs
Abbreviated titleTAP 2016
Country/TerritoryAustria
CityVienna
Period5/07/167/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.

Cite this