Files in this item



application/pdfSynthesizing Mo ... th Calls and Returns -.pdf (257kB)
(no description provided)PDF


Title:Synthesizing Monitors for Safety Properties - This Time With Calls and Returns -
Author(s):Rosu, Grigore; Chen, Feng; Ball, Thomas
Subject(s):computer science
Abstract:We present an extension of past time LTL with call/return atoms, called ptCaRet, together with a monitor synthesis algorithm for it. ptCaRet includes abstract variants of past temporal operators, which can express properties over traces in which terminated function or procedure executions are abstracted away into a call and a corresponding return. This way, ptCaRet can express safety properties about procedural programs which cannot be expressed using conventional linear temporal logics. The generated monitors contain both a local state and a stack. The local state is encoded on as many bits as concrete temporal operators the original formula has. The stack pushes/pops bit vectors of size the number of abstract temporal operators the original formula has: push on begins, pop on ends of procedure executions. An optimized implementation is also discussed and is available to download.
Issue Date:2007-10
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2007-2908
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-22

This item appears in the following Collection(s)

Item Statistics