Stephan van Staden

Overview

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

Research

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

• Software specification
• Formal systems for establishing software correctness
• Semantics
• Concurrency
• Verification of object-oriented programs
• Separation logic
• Refinement and Correctness by Construction
• Proof tools

Publications

2012

• Van Staden, S.: A Framework for Concurrent Imperative Programming. CoRR, abs/1209.2012
• Van Staden, S., Hoare, T.: Algebra Unifies Operational Calculi. In UTP 2012, Volume 7681 of Lecture Notes in Computer Science, Springer, 2013, pp 88-104
• Hoare, T., Van Staden, S.: The Laws of Programming Unify Process Calculi. In MPC 2012, Volume 7342 of Lecture Notes in Computer Science, Springer, pp 7-22
• Hoare, T., Van Staden, S.: In Praise of Algebra. In Formal Aspects of Computing, Volume 24, Number 4-6, 2012, pp 423-431
• 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 2012: the teaching assistant for Software Verification
• Fall 2011: the teaching assistant for Separation Logic
• Fall 2011: the teaching assistant for Software Verification
• Fall 2010: the teaching assistant for Software Verification
• Spring 2010: teaching assisting for Software Architecture
• Fall 2009: the teaching assistant for Software Verification
• Spring 2009: teaching assistant for Software Architecture
• Fall 2008: the teaching assistant for Software Verification
• Fall 2008: the teaching assistant for Eiffel: Analysis, Design and Programming

Internship

I did an internship at Microsoft Research in Cambridge between February and April 2011. I worked on separation logic and sharing in data structures, the verification of object-oriented programs, and algebra.

Summer schools

I attended the following summer schools:

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

Events

Member of the organizing committee of TAP 2009, the third international conference on Tests And Proofs

Talks

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

Slides for several of my research talks are available at Publications.

Goodies

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

Other

Trouble understanding fractional permissions? Maybe this video tutorial helps.