Temporal Logic Verification of Lock-Freedom. - Bogdan Tofan; Simon Bäumler; Gerhard Schellhorn; Wolfgang Reif (MPC, 2010)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Formal Verification of a Lock-Free Stack with Hazard Pointers. - Bogdan Tofan; Gerhard Schellhorn; Wolfgang Reif (ICTAC, 2011)

Interleaved Programs and Rely-Guarantee Reasoning with ITL. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Wolfgang Reif (TIME, 2011)

Proving linearizability with temporal logic. - Simon Bäumler; Gerhard Schellhorn; Bogdan Tofan; Wolfgang Reif (Formal Aspects Comput., 2011)

Compositional Verification of a Lock-Free Stack with RGITL. - Bogdan Tofan; Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Quiescent Consistency: Defining and Verifying Relaxed Linearizability. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Bogdan Tofan; Oleg Travkin; Heike Wehrheim (FM, 2014)

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset. - Bogdan Tofan; Gerhard Schellhorn; Wolfgang Reif (IFM, 2014)

RGITL: A temporal logic framework for compositional reasoning about interleaved programs. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Ann. Math. Artif. Intell., 2014)

Two approaches for proving linearizability of multiset. - Bogdan Tofan; Oleg Travkin; Gerhard Schellhorn; Heike Wehrheim (Sci. Comput. Program., 2014)

Compositional Concurrent Program Verification with RGITL. - Bogdan Tofan (2014)