Stephan van Staden

Overview

I am a research assistant at the Chair of Software Engineering at ETH Zurich under the supervision of Prof. Bertrand Meyer.

Research

My primary interest is formal verification of programs. I'm therefore interested in:

• Language semantics
• Proof systems, esp. separation logic systems
• Program specification
• Proofs of program correctness
• Refinement and Correctness by Construction
• Proof tools. Check out the basic demo of ProveIt! It can also verify whether executable specifications will always hold at runtime: take a look at this demo. As time went by, ProveIt! evolved into MultiStar. Be sure to check out the MultiStar demo!

Publications

2012

• Van Staden, S., Calcagno, C., Meyer, B.: Freefinement. In POPL 2012, Philadelphia, Pennsylvania, ACM, New York, NY, USA, pp 7-18 [pdf] [slides]

2010

• Van Staden, S., Calcagno, C.: Reasoning about Multiple Related Abstractions with MultiStar. OOPSLA/SPLASH 2010, ACM, New York, NY, USA, pp 504-519 [pdf] [slides] [demo]
• Van Staden, S., Calcagno, C.: Reasoning about Multiple Related Abstractions with MultiStar. Technical report 666, ETH Zurich, 2010 [pdf] Note: This paper is listed only for historical reasons. Please consult the OOPSLA MultiStar paper if you are interested in this work.
• Van Staden, S., Calcagno, C., Meyer, B.: Verifying Executable Object-Oriented Specifications with Separation Logic. ECOOP, Volume 6183 of Lecture Notes in Computer Science., Springer (June 2010) 151-174 [pdf] [slides] [demo]

2009

• Van Staden, S., Calcagno, C.: Separation, Abstraction, Multiple Inheritance and View Shifting. Technical report 655, ETH Zurich, 2009 [pdf] Note: This paper is listed only for historical reasons. Please consult the OOPSLA MultiStar paper if you are interested in this work.

Teaching

• Fall 2011: head assistant for Separation Logic (Dr Cristiano Calcagno)
• Fall 2011: head assistant for Software Verification (Prof. Bertrand Meyer)
• Fall 2010: head assistant for Software Verification (Prof. Bertrand Meyer)
• Spring 2010: teaching assisting for Software Architecture (Prof. Bertrand Meyer, Dr Michela Pedroni)
• Fall 2009: head assistant for Software Verification (Prof. Bertrand Meyer)
• Spring 2009: teaching assistant for Software Architecture (Prof. Bertrand Meyer)
• Fall 2008: head assistant for Software Verification (Prof. Bertrand Meyer)
• Fall 2008: head assistant for Eiffel: Analysis, Design and Programming (Prof. Bertrand Meyer)

Internship

I did an internship at Microsoft Research in Cambridge between February and April 2011. I worked with Matthew Parkinson on verification of object-oriented programs.

Summer schools I attended

• LASER 2011 Summer School on Software Engineering
  September 4-10, 2011, Isola d'Elba, Italy
  Tools for Practical Software Verification
  
• LASER 2010 Summer School on Software Engineering
  September 5-11, 2010, Isola d'Elba, Italy
  Empirical Software Engineering
  
• LASER 2008 Summer School on Software Engineering
  September 7-13, 2008, Isola d'Elba, Italy
  Concurrency and Correctness
  

Events

• TAP 2009 (Tests And Proofs) 2 & 3 July 2009, ETH Zurich, Switzerland
  Member of the organizing committee

Talk

Slides about separation logic for Object-Orientation (presented in the Separation Logic course): PDF PPTX

Goodies

Information about Boogie (syntax highlighting, the reference manual, general tips) is available here.

Other

Trouble understanding fractional permissions? Maybe this video tutorial helps.