Refinement of Trace Abstraction for Real-Time Programs. Cassez, F., Jensen, P. G., & Larsen, K. G. In Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings, volume 10506, pages 42–58, 2017. Springer.
![Refinement of Trace Abstraction for Real-Time Programs [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper doi abstract bibtex 2 downloads
Paper doi abstract bibtex 2 downloads Real-time programs are made of instructions that can perform assignements 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 the reachability verification 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.
@inproceedings{rp-17,
author = {Franck Cassez and
Peter Gj{\o}l Jensen and
Kim Guldstrand Larsen},
title = {Refinement of Trace Abstraction for Real-Time Programs},
booktitle = {Reachability Problems - 11th International Workshop, {RP} 2017, London,
UK, September 7-9, 2017, Proceedings},
volume = {10506},
pages = {42--58},
year = {2017},
publisher = {Springer},
url = {https://doi.org/10.1007/978-3-319-67089-8_4},
doi = {10.1007/978-3-319-67089-8_4},
timestamp = {Wed, 30 Aug 2017 15:59:47 +0200},
isbn = {978-3-319-67088-1},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/rp/CassezJL17},
bibsource = {dblp computer science bibliography, http://dblp.org},
urlpaper = {papers/rp-17.pdf},
abstract = {Real-time programs are made of instructions that can perform assignements 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 the reachability verification 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.}
}Downloads: 2
{"_id":"TCMiSWemurthQWAAB","bibbaseid":"cassez-jensen-larsen-refinementoftraceabstractionforrealtimeprograms-2017","author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Peter","Gjøl"],"propositions":[],"lastnames":["Jensen"],"suffixes":[]},{"firstnames":["Kim","Guldstrand"],"propositions":[],"lastnames":["Larsen"],"suffixes":[]}],"title":"Refinement of Trace Abstraction for Real-Time Programs","booktitle":"Reachability Problems - 11th International Workshop, RP 2017, London, UK, September 7-9, 2017, Proceedings","volume":"10506","pages":"42–58","year":"2017","publisher":"Springer","url":"https://doi.org/10.1007/978-3-319-67089-8_4","doi":"10.1007/978-3-319-67089-8_4","timestamp":"Wed, 30 Aug 2017 15:59:47 +0200","isbn":"978-3-319-67088-1","biburl":"http://dblp.uni-trier.de/rec/bib/conf/rp/CassezJL17","bibsource":"dblp computer science bibliography, http://dblp.org","urlpaper":"papers/rp-17.pdf","abstract":"Real-time programs are made of instructions that can perform assignements 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 the reachability verification 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.","bibtex":"@inproceedings{rp-17,\n author = {Franck Cassez and\n Peter Gj{\\o}l Jensen and\n Kim Guldstrand Larsen},\n title = {Refinement of Trace Abstraction for Real-Time Programs},\n booktitle = {Reachability Problems - 11th International Workshop, {RP} 2017, London,\n UK, September 7-9, 2017, Proceedings},\n volume = {10506},\n pages = {42--58},\n year = {2017},\n publisher = {Springer},\n url = {https://doi.org/10.1007/978-3-319-67089-8_4},\n doi = {10.1007/978-3-319-67089-8_4},\n timestamp = {Wed, 30 Aug 2017 15:59:47 +0200},\n isbn = {978-3-319-67088-1},\n biburl = {http://dblp.uni-trier.de/rec/bib/conf/rp/CassezJL17},\n bibsource = {dblp computer science bibliography, http://dblp.org},\n urlpaper = {papers/rp-17.pdf},\n abstract = {Real-time programs are made of instructions that can perform assignements to discrete and real-valued variables. \n They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. \n We propose a semi-algorithm using refinement of trace abstractions to solve the reachability verification problem for real-time programs. \n 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.}\n}\n\n\n","author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"key":"rp-17","id":"rp-17","bibbaseid":"cassez-jensen-larsen-refinementoftraceabstractionforrealtimeprograms-2017","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/rp-17.pdf"},"metadata":{"authorlinks":{}},"downloads":2},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F"],"keywords":[],"search_terms":["refinement","trace","abstraction","real","time","programs","cassez","jensen","larsen"],"title":"Refinement of Trace Abstraction for Real-Time Programs","year":2017,"downloads":2}