IRIS Institutional Research Information System - AIR Archivio Istituzionale della Ricerca

IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Milano.

AIR nasce in UNIMI nel 2006 con lo scopo di raccogliere, documentare e conservare le informazioni sulla produzione scientifica dell'Università degli Studi di Milano e costituisce di fatto l'Anagrafe della ricerca dell'Ateneo.

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.

Powered by IRIS-about IRIS-Utilizzo dei cookie

 Copyright © 2019