Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer: Model Checking Security Properties of Control Flow Graphs. J. Comput. Secur. 9(3): 217-250 (2001)