Suche

Publications


    2014

  • A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset
    B. Tofan, G. Schellhorn, W. Reif
    In Proc. of Integrated Formal Methods (iFM), vol. 8739 LNCS, pp.357-372 , Springer
    abstract;

     
  • Quiescent Consistency: Defining and Verifying Relaxed Linearizability
    J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, H. Wehrheim
    In Proc. of Formal Methods (FM), Springer, LNCS, vol. 8442, pp. 200 - 214
    abstract;

     
  • Two Approaches for Proving Linearizability of Multiset
    B. Tofan, O. Travkin, G. Schellhorn, H. Wehrheim
    Science of Computer Programming Journal, vol. 96, Part 3, pp. 297–314, Elsevier
    abstract;

     
  • RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs
    G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif
    Annals of Mathematics and Artificial Intelligence (AMAI) Journal, vol. 71, issue 1-3, pp. 131-174, Springer
    abstract;

     
  • 2013

  • Compositional Verification of a Lock-Free Stack with RGITL
    B. Tofan, G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif
    ECEASST Journal, vol. 66
    abstract;

     
  • 2012

  • 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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen and Mattias Ulbrich
    In Proc. of Formal Verification of Object-Oriented Software (FoVeOOS), pp 3-21, Springer (LNCS)
    abstract;

     
  • 2011

  • Interleaved Programs and Rely-Guarantee Reasoning with ITL
    G. Schellhorn, B.Tofan, G. Ernst, and W. Reif
    In Proc. of International Symposium on Temporal Representation and Reasoning in AI (TIME), IEEE (CPS), P4508, pp. 99 - 106
    abstract; Interleaved Programs and Rely-Guarantee Reasoning with ITL (285 KB);

     
  • Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom
    B.Tofan, G. Schellhorn, and W. Reif
    In Pre-Proceedings of Conference on Formal Verification of Object Oriented Software (FoVeOOS), Karlsruhe Reports in Informatics, vol. 26, pp. 342 - 359
    abstract; Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom (218 KB);

     
  • Formal Verification of a Lock-Free Stack with Hazard Pointers
    B. Tofan, G. Schellhorn, and W. Reif
    In Proc. of International Colloquium on Theoretical Aspects of Computing (ICTAC), Springer, LNCS, vol. 6916, pp. 239 - 255
    abstract; Formal Verification of a Lock-Free Stack with Hazard Pointers (195 KB);

     
  • Proving Linearizability with Temporal Logic
    S. Bäumler, G. Schellhorn, B. Tofan and W. Reif
    Journal of Formal Aspects of Computing (FAC), Springer, 23(1), pp. 91 - 112
    abstract;

     
  • 2010

  • Temporal Logic Verification of Lock-Freedom
    B. Tofan, S. Bäumler, G. Schellhorn, and W. Reif
    In Proc. of Mathematics of Program Construction (MPC), Springer, LNCS, vol. 6120, pp. 377 - 396
    abstract; Temporal Logic Verification of Lock-Freedom (211 KB);