Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code

Reliability in terms of functional properties from the safety-liveness spectrum is an indispensable requirement of low-level operating-system (OS) code. However, with evermore complex and thus less predictable hardware, quantitative and probabilistic guarantees become more and more important. Probab...

Full description

Bibliographic Details
Main Authors: Marcus Völp, Steffen Märcker, Hendrik Tews, Hermann Härtig, Sascha Klüppelholz, Benjamin Engel, Marcus Daum, Christel Baier, Joachim Klein
Format: Article
Language:English
Published: Open Publishing Association 2012-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1211.6196v1