Reference : Specifying Properties over Inter-Procedural, Source Code Level Behaviour of Programs
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/47852
Specifying Properties over Inter-Procedural, Source Code Level Behaviour of Programs
English
Dawes, Joshua mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Bianculli, Domenico mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
In press
Proceedings of the 21st International Conference on Runtime Verification
Yes
No
International
21st International Conference on Runtime Verification
from 11-10-2021 to 14-10-2021
Virtual
[en] dynamic analysis ; source code ; interprocedural
[en] The problem of verifying a program at runtime with respect to some formal specification has led to the development of a rich collection of specification languages. These languages often have a high level of abstraction and provide sophisticated modal operators, giving a high level of expressiveness. In particular, this makes it possible to express properties concerning the source code level behaviour of programs. However, for many languages, the correspondence between events generated at the source code level and parts of the specification in question would have to be carefully defined.
To enable expressing — using a temporal logic — properties over source code level behaviour without the need for this correspondence, previous work introduced Control-Flow Temporal Logic (CFTL), a specification language with a low level of abstraction with respect to the source code of programs. However, this work focused solely on the intra-procedural setting. In this paper, we address this limitation by introducing Inter-procedural CFTL, a language for expressing source code level, inter-procedural properties of program runs. We evaluate the new language, iCFTL, via application to a real-world case study.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
European Commission - EC
http://hdl.handle.net/10993/47852
H2020 ; 957254 - COSMOS - DevOps for Complex Cyber-Physical Systems

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
main.pdfAuthor postprint224.4 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.