Skip navigation
Skip navigation

Greedy pebbling for proof space compression

Fellner, Andreas; Woltzenlogel Paleo, Bruno


Automated reasoning tools for the verification and synthesis of software often produce proofs to allow independent certification of the correctness of the produced solutions. As proofs can be large, this paper considers the problem of compressing proofs with respect to their space, which is approximately proportional to the memory necessary to check them. Proof checking with a small amount of available memory is analogous to playing a pebbling game with a small number of pebbles. This paper...[Show more]

CollectionsANU Research Publications
Date published: 2017
Type: Journal article
Source: International Journal on Software Tools for Technology Transfer
DOI: 10.1007/s10009-017-0459-0


There are no files associated with this item.

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator