Challenge benchmarks for verification of real-time programs

Page Content

Author

Jan Vitek

Tech report number

CERIAS TR 2010-21

Entry type

article

Abstract

Real-time systems, and in particular safety-critical systems, are a rich source of challenges for the program verification community as software errors can have catastrophic consequences. Unfortunately, it is nearly impossible to find representative safety-critical programs in the public domain. This has been significant impediment to research in the field, as it is very difficult to validate new ideas or techniques experimentally. This paper presents open challenges for verification of real-time systems in the context of the Real-time Specification for Java. But, our main contribution is a family of programs, called CDx, which we present as an open source benchmark for the verification community.

Date

2010 – 1 – 1

URL

http://portal.acm.org/citation.cfm?id=1707800

Key alpha

Vitek

Publication Date

2010-01-01

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.