Refinement of trace abstraction for real-time programs

Franck Cassez, Peter Gjøl Jensen*, Kim Guldstrand Larsen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

7 Citations (Scopus)


Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

Original languageEnglish
Title of host publicationReachability Problems
Subtitle of host publication11th International Workshop, RP 2017, Proceedings
EditorsMatthew Hague, Igor Potapov
Place of PublicationCham, Switzerland
PublisherSpringer, Springer Nature
Number of pages17
ISBN (Electronic)9783319670898
ISBN (Print)9783319670881
Publication statusPublished - 2017
Event11th International Workshop on Reachability Problems, RP 2017 - London, United Kingdom
Duration: 7 Sept 20179 Sept 2017

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Workshop on Reachability Problems, RP 2017
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Refinement of trace abstraction for real-time programs'. Together they form a unique fingerprint.

Cite this