Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
From FSL
- Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
- Grigore Rosu, Feng Chen and Thomas Ball
RV'08, to appear.
PDF, RV'08, BIB
[edit] 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.
