School of Computing

Challenge benchmarks for verification of real-time programs

Tomas Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, and Jan Vitek

In Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (PLPV), pages 182-196. ACM, January 2010 [doi].

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.

Download publication 147 kbytes (PDF)

Bibtex Record

@inproceedings{3125,
author = {Tomas Kalibera and Pavel Parizek and Ghaith Haddad and Gary T. Leavens and Jan Vitek},
title = {Challenge benchmarks for verification of real-time programs},
month = {January},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1145/1707790.1707800},
url = {http://www.cs.kent.ac.uk/pubs/2010/3125},
    publication_type = {inproceedings},
    submission_id = {6629_1308766093},
    ISBN = {978-1-60558-890-2},
    booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (PLPV)},
    publisher = {ACM},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014