License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.15
URN: urn:nbn:de:0030-drops-95531
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9553/
Atig, Mohamed Faouzi ;
Bouajjani, Ahmed ;
Narayan Kumar, K. ;
Saivasan, Prakash
Verifying Quantitative Temporal Properties of Procedural Programs
Abstract
We address the problem of specifying and verifying quantitative properties of procedural programs. These properties typically involve constraints on the relative cumulated costs of executing various tasks (by invoking for instance some particular procedures) within the scope of the execution of some particular procedure. An example of such properties is "within the execution of each invocation of procedure P, the time spent in executing invocations of procedure Q is less than 20 % of the total execution time". We introduce specification formalisms, both automata-based and logic-based, for expressing such properties, and we study the links between these formalisms and their application in model-checking. On one side, we define Constrained Pushdown Systems (CPDS), an extension of pushdown systems with constraints, expressed in Presburger arithmetics, on the numbers of occurrences of each symbol in the alphabet within invocation intervals (subcomputations between matching pushes and pops), and on the other side, we introduce a higher level specification language that is a quantitative extension of CaRet (the Call-Return temporal logic) called QCaRet where nested quantitative constraints over procedure invocation intervals are expressible using Presburger arithmetics. Then, we investigate (1) the decidability of the reachability and repeated reachability problems for CPDS, and (2) the effective reduction of the model-checking problem of procedural programs (modeled as visibly pushdown systems) against QCaRet formulas to these problems on CPDS.
BibTeX - Entry
@InProceedings{atig_et_al:LIPIcs:2018:9553,
author = {Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan},
title = {{Verifying Quantitative Temporal Properties of Procedural Programs}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Sven Schewe and Lijun Zhang},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9553},
URN = {urn:nbn:de:0030-drops-95531},
doi = {10.4230/LIPIcs.CONCUR.2018.15},
annote = {Keywords: Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties}
}
|
Keywords: |
|
Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties |
|
Collection: |
|
29th International Conference on Concurrency Theory (CONCUR 2018) |
|
Issue Date: |
|
2018 |
|
Date of publication: |
|
31.08.2018 |
