Contrary to Dijkstra's diktat, testing, and more in general validation has found an increasing niche in formal verification, prior or even in alternative to theorem proving. In particular, property-based testing (PBT) is quite effective in mechanized meta-theory of programming languages, where theorems have shallow but tedious proofs that may go wrong for fairly banal mistakes. In this report, we abandon the comfort of high-level object languages and address the validation of abstract machines and typed assembly languages. We concentrate on Appel et al.'s list-machine benchmark [ADL12], which we tackle with αCheck, the simple model-checker on top of the nominal logic programming αProlog. We uncover one major bug in the published version of the paper plus several typos and ambiguities thereof. This is particularly striking, as the paper is accompanied by two full formalizations, in Coq and Twelf. Finally, we carry out some mutation testing on the given model, to asses the trade-off between exhaustive and randomized data generation, using for the latter the PBT library FSCheck for F#. Spoiler alert: aProlog performs better. © Copyright 2018 for the individual papers by the papers' authors.

Property-based testing of the meta-theory of abstract machines: An experience report / F. Komauli, A. Momigliano (CEUR WORKSHOP PROCEEDINGS). - In: Italian Conference on Computational Logic CILC 2018 / [a cura di] P. Felli, M. Montali. - [s.l] : CEUR, 2018 Oct. - pp. 22-39 (( Intervento presentato al 33. convegno Italian Conference on Computational Logic tenutosi a Bolzano nel 2018.

Property-based testing of the meta-theory of abstract machines: An experience report

A. Momigliano
2018

Abstract

Contrary to Dijkstra's diktat, testing, and more in general validation has found an increasing niche in formal verification, prior or even in alternative to theorem proving. In particular, property-based testing (PBT) is quite effective in mechanized meta-theory of programming languages, where theorems have shallow but tedious proofs that may go wrong for fairly banal mistakes. In this report, we abandon the comfort of high-level object languages and address the validation of abstract machines and typed assembly languages. We concentrate on Appel et al.'s list-machine benchmark [ADL12], which we tackle with αCheck, the simple model-checker on top of the nominal logic programming αProlog. We uncover one major bug in the published version of the paper plus several typos and ambiguities thereof. This is particularly striking, as the paper is accompanied by two full formalizations, in Coq and Twelf. Finally, we carry out some mutation testing on the given model, to asses the trade-off between exhaustive and randomized data generation, using for the latter the PBT library FSCheck for F#. Spoiler alert: aProlog performs better. © Copyright 2018 for the individual papers by the papers' authors.
Settore INF/01 - Informatica
ott-2018
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
pbtam.pdf

accesso riservato

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 340.11 kB
Formato Adobe PDF
340.11 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
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: https://hdl.handle.net/2434/595260
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact