VMCAI 09 : Reducing Behavioural to Structural Properties of Programs with Procedures

This paper try to figure out structrue information from behavior, just reverse the traditinal working direction. One of his sentense best describe the difference between behaviour and structure:
-------------------------------
Both program structure and behaviour can be specied by temporal logicformulae: structural properties concern the textual sequencing of instructions ina program, while behavioural properties consider their executional sequencing.
-------------------------------
In it definition if structure and behavior in section 2, I notice that the behaviour model record the state of stack, while the structure model only contain flow graph.

It major application is in compositional verification, in another word, to synthesis the invaraint of outer world.

BTW: it remind me of the "path invariant" paper on PLDI07, which represent the counterexample as a program. Can this be think of as another form of behavior(counterexample) to structure(program)???