Kalibera, Tomas and Parizek, Pavel and Haddad, Ghaith and Leavens, Gary T. and Vitek, Jan (2010) Challenge benchmarks for verification of real-time programs. In: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (PLPV).
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://www.cs.kent.ac.uk/pubs/2010/3125 |
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.
| Item Type: | Conference or workshop item (UNSPECIFIED) |
|---|---|
| Uncontrolled keywords: | determinacy analysis, Craig interpolants |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing |
| Depositing User: | Tomas Kalibera |
| Date Deposited: | 21 Sep 2012 09:49 |
| Last Modified: | 21 Sep 2012 09:49 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/30697 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
