Flash memory efficient LTL model checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

EDELKAMP Stefan SULEWSKI Damian BARNAT Jiří BRIM Luboš ŠIMEČEK Pavel

Year of publication 2011
Type Article in Periodical
Magazine / Source Science of Computer Programming
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1016/j.scico.2010.03.005
Doi http://dx.doi.org/10.1016/j.scico.2010.03.005
Field Informatics
Keywords Model checking; External memory algorithms; Algorithm engineering
Description So far, large-scale LTL model checking algorithms have been designed to employ external memory optimized for magnetic disks. We propose algorithms optimized for flash memory access. In contrast to approaches relying on the delayed detection of duplicate states, in this work, we design and exploit appropriate hash functions to re-invent immediate duplicate detection.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.