Flash memory efficient LTL model checking

• 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
• 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

• Techniques for automatic verification and validation of software nad hardware systems
• Highly Parallel and Distributed Computing Systems
• Automated software verification