PTCaRetPlugin4

PTCaRet plugin for MOP allows one to synthesize monitors from past time linear temporal logic with call and return (PTCaRet) descriptions. PTCaRet extends the past time linear temporal logic (PTLTL) with call/return atoms. In addition to the standard temporal operators, it also 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.