Flash memory efficient LTL model checking

DOI10.1016/J.SCICO.2010.03.005MaRDI QIDQ617930zbMATH OpenOpenAlexFDO

Authors Damian Sulewski, P. Šimeček, Stefan Edelkamp, J. Barnat, Luboš Brim

Publication date 14 January 2011

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2010.03.005

zbMATH Keywords

model checkingalgorithm engineeringexternal memory algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Semi-external LTL Model Checking
• Memory-efficient tactics for randomized LTL model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Software

Cites work

• scientific article; zbMATH DE number 1688373 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3887059 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 1305462 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1982197 (Why is no real title available?)
• scientific article; zbMATH DE number 1875412 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 3303654 (Why is no real title available?)
• A minimized automaton representation of reachable states
• Algorithms for memory hierarchies. Advanced lectures
• Dynamic Perfect Hashing: Upper and Lower Bounds
• Flash memory efficient LTL model checking
• Formal Methods in Computer-Aided Design
• Hash, Displace, and Compress
• KI 2004: Advances in Artificial Intelligence
• Mechanising a formal model of flash memory
• Model Checking Software
• Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking
• Semi-external LTL Model Checking
• Simple and Space-Efficient Minimal Perfect Hash Functions
• Space/time trade-offs in hash coding with allowable errors
• Storing a Sparse Table with 0 (1) Worst Case Access Time
• Storing a sparse table
• Survey on Directed Model Checking
• The Spatial Complexity of Oblivious k-Probe Hash Functions
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Memory-efficient tactics for randomized LTL model checking
• Mechanising a formal model of flash memory
• Flash memory efficient LTL model checking
• How hard is finding shortest counter-example lassos in model checking?
• Tools and Algorithms for the Construction and Analysis of Systems

Describes a project that uses

Uses Software

• Algorithm 360
• Murphi
• BEEM
• STXXL
• DiVinE

This page was built for publication: Flash memory efficient LTL model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q617930)