I am an Honorary Research Associate in the Programming Principles, Logic and Verification research group at University College London.

Before that, I was a Research and Teaching Assistant in the Software Engineering research group at ETH Zurich in Switzerland, where I received my PhD.

Research

My primary interest is in the formal verification of software, which spans several exciting topics:

• Software specification
• Formal systems for establishing software correctness
• Semantics
• Concurrency
• Separation logic
• Algebra of programming
• Correctness by Construction
• Proof tools

My work aims to show that formal reasoning about software can be simple, elegant and fun.

Publications

Journals

HvSM15

Developments in Concurrent Kleene Algebra

T. Hoare, S. van Staden, B. Möller, G. Struth and H. Zhu. Journal of Logical and Algebraic Methods in Programming, to appear, 2015.

HvS14

The laws of programming unify process calculi

T. Hoare and S. van Staden. Science of Computer Programming, Volume 85, pages 102-114, 2014. [Isabelle/HOL proofs]

HvS12a

In Praise of Algebra

T. Hoare and S. van Staden. Formal Aspects of Computing, Volume 24, Number 4-6, pages 423-431, 2012. [Isabelle/HOL proofs]

Conferences

vS15

On Rely-Guarantee Reasoning

S. van Staden. MPC'15, Volume 9129 of LNCS, Springer, pages 30-49, 2015. [PDF | Isabelle/HOL proofs | Slides]

vS14

Constructing the Views Framework

S. van Staden. UTP'14, Volume 8963 of LNCS, Springer, pages 62-83, 2014. [PDF | Isabelle/HOL proofs | Slides]

HvSM14

Developments in Concurrent Kleene Algebra

T. Hoare, S. van Staden, B. Möller, G. Struth, J. Villard, H. Zhu and P. O'Hearn. RAMiCS'14, Volume 8428 of LNCS, Springer, pages 1-18, 2014.

vSH12

Algebra Unifies Operational Calculi

S. van Staden and T. Hoare. UTP'12, Volume 7681 of LNCS, Springer, pages 88-104, 2013. [Isabelle/HOL proofs]

HvS12b

The Laws of Programming Unify Process Calculi

T. Hoare and S. van Staden. MPC'12, Volume 7342 of LNCS, Springer, pages 7-22, 2012. [Isabelle/HOL proofs]

vSCM12

Freefinement

S. van Staden, C. Calcagno and B. Meyer. POPL'12, ACM, New York, NY, USA, pages 7-18, 2012. [PDF]

vSC10a

Reasoning about Multiple Related Abstractions with MultiStar

S. van Staden and C. Calcagno. OOPSLA'10, ACM, New York, NY, USA, pages 504-519, 2010. [PDF | Demo]

vSCM10

Verifying Executable Object-Oriented Specifications with Separation Logic

S. van Staden, C. Calcagno and B. Meyer. ECOOP'10, Volume 6183 of LNCS, Springer, pages 151-174, 2010. [PDF | Demo]

Technical Reports

vS12

A Framework for Concurrent Imperative Programming

S. van Staden. CoRR abs/1209.2012, 2012. [PDF | Isabelle/HOL proofs]

vSC10b

Reasoning about Multiple Related Abstractions with MultiStar

S. van Staden and C. Calcagno. Technical report 666, ETH Zurich, Switzerland, 2010. [PDF]
See [vSC10a] for a later version of this work.

vSC09

Separation, Abstraction, Multiple Inheritance and View Shifting

S. van Staden and C. Calcagno. Technical report 655, ETH Zurich, Switzerland, 2009. [PDF]
See [vSC10a] for a later version of this work.

Thesis

vS13

Enhancing Separation Logic for Object-Orientation

S. van Staden. ETH Zurich, Switzerland, 2013. [PDF]