@article{DBLP:journals/corr/abs-2007-10539,
  author    = {Franck Cassez and
               Peter Gj{\o}l Jensen and
               Kim Guldstrand Larsen},
  title     = {Verification and Parameter Synthesis for Real-Time Programs using
               Refinement of Trace Abstraction},
  journal   = {CoRR},
  abstract = {We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that 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. 
All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.},
  volume    = {abs/2007.10539},
  year      = {2020},
  url       = {https://arxiv.org/abs/2007.10539},
  archivePrefix = {arXiv},
  eprint    = {2007.10539},
  timestamp = {Tue, 28 Jul 2020 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2007-10539.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

{"_id":"wGpn6bFrg4x2JpYFk","bibbaseid":"cassez-jensen-larsen-verificationandparametersynthesisforrealtimeprogramsusingrefinementoftraceabstraction-2020","authorIDs":["aYsqprsgp7HA5GpQ3"],"author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Peter","Gjøl"],"propositions":[],"lastnames":["Jensen"],"suffixes":[]},{"firstnames":["Kim","Guldstrand"],"propositions":[],"lastnames":["Larsen"],"suffixes":[]}],"title":"Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction","journal":"CoRR","abstract":"We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that 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. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.","volume":"abs/2007.10539","year":"2020","url":"https://arxiv.org/abs/2007.10539","archiveprefix":"arXiv","eprint":"2007.10539","timestamp":"Tue, 28 Jul 2020 01:00:00 +0200","biburl":"https://dblp.org/rec/journals/corr/abs-2007-10539.bib","bibsource":"dblp computer science bibliography, https://dblp.org","bibtex":"@article{DBLP:journals/corr/abs-2007-10539,\n author = {Franck Cassez and\n Peter Gj{\\o}l Jensen and\n Kim Guldstrand Larsen},\n title = {Verification and Parameter Synthesis for Real-Time Programs using\n Refinement of Trace Abstraction},\n journal = {CoRR},\n abstract = {We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that 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. \nWe 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. \nAll of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.},\n volume = {abs/2007.10539},\n year = {2020},\n url = {https://arxiv.org/abs/2007.10539},\n archivePrefix = {arXiv},\n eprint = {2007.10539},\n timestamp = {Tue, 28 Jul 2020 01:00:00 +0200},\n biburl = {https://dblp.org/rec/journals/corr/abs-2007-10539.bib},\n bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n","author_short":["Cassez, F.","Jensen, P. G.","Larsen, K. G."],"key":"DBLP:journals/corr/abs-2007-10539","id":"DBLP:journals/corr/abs-2007-10539","bibbaseid":"cassez-jensen-larsen-verificationandparametersynthesisforrealtimeprogramsusingrefinementoftraceabstraction-2020","role":"author","urls":{"Paper":"https://arxiv.org/abs/2007.10539"},"metadata":{"authorlinks":{"cassez, f":"http://science.mq.edu.au/~fcassez/software-verif.html"}},"downloads":4,"html":""},"bibtype":"article","biburl":"https://franck44.github.io/publications/franck-pubs.bib","creationDate":"2020-12-06T22:25:57.178Z","downloads":4,"keywords":[],"search_terms":["verification","parameter","synthesis","real","time","programs","using","refinement","trace","abstraction","cassez","jensen","larsen"],"title":"Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction","year":2020,"dataSources":["8742EsvjQfyP2fYBW"]}