Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --

From FSL
Jump to: navigation, search

Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 
Grigore Rosu, Feng Chen and Thomas Ball
RV'08, LNCS 5289, pp 51-68, 2008
PDF, RV'08, BIB


Technical Report

Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
Grigore Rosu,Feng Chen and Thomas Ball
Technical report UIUCDCS-R-2007-2908, October 2007
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.
PDF, BIB

Personal tools
Namespaces

Variants
Actions
Navigation