« Proof obligations for specification and refinement of liveness properties under weak fairness, 2005. ,
Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants, Lecture Notes in Computer Science, vol.1878, pp.230-245, 2000. ,
DOI : 10.1007/3-540-44525-0_14
« The Temporal Logic of Actions, 1991. ,
Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, 2002. ,