Mona: Monadic Second-Order Logic in Practice. - Jesper G. Henriksen; Jakob L. Jensen; Michael E. Jørgensen; Nils Klarlund; Robert Paige; Theis Rauhe; Anders Sandholm 001 (TACAS, 1995)

Automatic Verification of Pointer Programs using Monadic Second-Order Logic. - Jakob L. Jensen; Michael E. Jørgensen; Nils Klarlund; Michael I. Schwartzbach (PLDI, 1997)