• Skip the Organizational structure panel
• Organizational structure

  On selecting a constituent part of MU the "Overview of publishing activities" page will be displayed with information relevant to the selected constituent part. The "Overview of publishing activities" page is not available for non-activated items.

  Masaryk University

  • Faculties
  • Law
  • Medicine
  • Science
  • Arts
  • Education
  • Economics
  • Informatics
  • Social Studies
  • Sports Studies

  • Institutes
  • Computer Science
  • CEITEC MU
  • Politica
  • Specialized Units
  • Hostels & Canteens
  • University Press
  • Telč Centre
  • UCB Management

  • Rector`s Office
  • Rectorate
  • Other Units
  • Archive
  • Language Centre
  • International Studies
  • Disabled Students
  • Technology Transfer
  • Biostatistics
  • Mendel Museum
  • CERIT
  • Civic Education
  • Project Team CEITEC

   

Publication details

Flash memory efficient LTL model checking

Further information
Citation:	EDELKAMP, Stefan - SULEWSKI, Damian - BARNAT, Jiří - BRIM, Luboš - ŠIMEČEK, Pavel. Flash memory efficient LTL model checking. Science of Computer Programming, Elsevier, The Nederlands. ISSN 0167-6423, 2011, vol. 76, no. 2, pp. 136--157.
Original language:	English
Field:	Informatika
WWW:	http://dx.doi.org/10.1016/j.scico.2010.03.005
Type:	Article in Periodical
Keywords:	Model checking; External memory algorithms; Algorithm engineering

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