Publications

2015

• Automated Usable Functional Verification of Object-oriented Programs (pdf)
  Julian Tschannen
  PhD Thesis, ETH Zurich, 2015.

  The thesis presents the Verification Assistant and AutoProof - both tools integrated in the Eiffel Verification Environment (EVE) - from a theoretical and practical point of view. An extensive evaluation of AutoProof on examples taken from verification challenges and other areas show its applicability to object-oriented code. In addition, the thesis presents theoretical advances to verification.

• The AutoProof Verifier: Usability by Non-Experts and on Standard Code (pdf) (bib)
  Carlo A. Furia, Christopher M. Poskitt, and Julian Tschannen
  In Proceedings of the 2nd Workshop on Formal-IDE (F-IDE 2015), 2015.

  This paper discusses how AutoProof was used to support teaching a course on software verification and our efforts of using AutoProof to verify code used to teach programming to beginner students.

• A Fully Verified Container Library (pdf) (bib)
  Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia
  In Proceedings of the 20th International Symposium on Formal Methods (FM 2015), 2015.
  Best paper award

  This paper details the results of the successful verification of a container library with AutoProof. The library can be verified with AutoProof's online interface.

• AutoProof: Auto-active Functional Verification of Object-oriented Programs (pdf) (bib) (arXiv)
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Nadia Polikarpova.
  In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), 2015.

  This paper presents AutoProof's interface, design, and implementation features, and demonstrates AutoProof's performance on a rich collection of benchmark problems. The benchmark problems are available online.

2014

• Flexible Invariants Through Semantic Collaboration (pdf) (bib) (arXiv)
  Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer
  In Proceedings of the 19th International Symposium on Formal Methods (FM 2014), 2014.

  This paper describes a flexible technique for framing and collaborative class invariants. An extended version of the paper and the source code of the problems are available online.

• AutoProof Meets Some Verification Challenges (pdf) (bib)
  Julian Tschannen, Carlo A. Furia, and Martin Nordio
  In International Journal on Software Tools for Technology Transfer (STTT), Special Section on Program Verification, 2014.

  This paper describes how AutoProof fares in solving the verification challenges posed at FM 2012. Note that the current version of AutoProof already removes some of the limitations described in this paper.

• The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel (abstract) (bib)
  Carlo A. Furia, Julian Tschannen, and Bertrand Meyer.
  In Proceedings of the 1st Workshop on Formal-IDE (F-IDE 2014), 2014.

  Invited talk at the F-IDE workshop

• Program Checking With Less Hassle (pdf) (bib)
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  In Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013), 2014.

  This paper describes the two-step verification approach. With this approach, a failed verification is followed by a second verification step using function call inlining and loop unrolling. In case the second verification step succeeds, the verification is more likely to be in need of an improved specification rather then an improved implementation.

2013

2012

• Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach (pdf) (bib)
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  In Tools for Practical Software Verification - LASER 2011, International Summer School, 2012.

  This paper describes techniques to prove object-oriented programs with Eiffel-style exceptions, polymorphism and agents (function objects). The content here subsumes previous publications.

2011

• The COST IC0701 Verification Competition 2011 (pdf) (bib)
  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 Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software< (FoVeOos 2011), 2011.

• Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques (pdf) (bib)
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  In Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011), 2011.

• Verifying Eiffel Programs with Boogie (pdf) (bib) (arXiv)
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  Presented at the 1st International Workshop on Intermediate Verification Languages (BOOGIE 2011), 2011.

  See Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

• How do Distribution and Time Zones affect Software Development? A Case Study on Communication (pdf) (bib)
  Martin Nordio, H.-Christian Estler, Bertrand Meyer, Julian Tschannen, Carlo Ghezzi, and Elisabetta Di Nitto
  In Proceedings of the 6th International Conference on Global Software Engineering (ICGSE 11), 2011.

• Teaching Software Engineering using Globally Distributed Projects: the DOSE course (pdf) (bib)
  Martin Nordio, Carlo Ghezzi, Bertrand Meyer, Elisabetta Di Nitto, Giordano Tamburrelli, Julian Tschannen, Nazareno Aguirre, and Vidya Kulkarni
  In Collaborative Teaching of Globally Distributed Software Development - Community Building Workshop (CTGDSD), 2011.

2010

• Reasoning about Function Objects (pdf) (bib)
  Martin Nordio, Cristiano Calcagno, Bertrand Meyer, Peter Müller, and Julian Tschannen
  In Proceedings of the 48th International Conference on Objects, Models, Components and Patterns (TOOLS-EUROPE 10), 2010.

  See Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

2009

• Automatic Verification of Eiffel Programs (pdf)
  Julian Tschannen
  Master Thesis, ETH Zurich, 2009.