Dr. Wytse Oortwijn

I am a postdoctoral researcher at the Chair of Programming Methodology led by Peter Müller at ETH Zürich, since September 2019. My main research interests lie in program verification; more specifically in concurrency verification, code verification using SMT-based tools, program logics (including concurrent separation logic), interactive theorem proving using assistants like Coq, runtime verification, process algebra, and (explicit/symbolic) model checking. I am particularly interested in combinations of these areas.

Currently I work on the VerifiedSCION project, whose goal is verifying the external page SCION routing protocol from the high-​level design all the way down to the implementation. I am currently involved in developing an automated code verifier for the external page Go language, as well as techniques for proving properties of SCION and Go programs.

I did my PhD (2015—2019) at external page Formal Methods and Tools research group at the external page University of Twente, under supervision of external page Marieke Huisman. My PhD thesis, titled external page Deductive Techniques for Model-​Based Concurrency Verification, combines program logics with model-based reasoning with the aim to verify global behavioural properties of real-world concurrent software. During my PhD I visited the group of external page Wolfgang Ahrendt at external page Chalmers University of Technology in Sweden, to work on runtime verification of distributed (active) objects.

In my Master's degree at the University of Twente (2012—2015) I studied symbolic model checking algorithms as well as algorithms and data-structures for high-performance computing on compute clusters.
 

Publications

• M. Safari, W. Oortwijn, S. Joosten and M. Huisman, Formal Verification of Parallel Prefix Sum. In NFM, 2020.
  
• W. Oortwijn, M. Huisman, S. Joosten and J. van de Pol, Automated Verification of Parallel Nested DFS. In TACAS, 2020. [PDF][external page Artifact]
  
• W. Oortwijn, Verifying Distributed Systems by Abstracting Channel Interaction. In WADT, 2020.
  
• W. Oortwijn, D. Gurov and M. Huisman, Practical Abstractions for Automated Verification of Shared-Memory Concurrency. In VMCAI, 2020. [external page PDF]
  
• W. Oortwijn and M. Huisman, Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In iFM, 2019. [external page PDF]
  
• W. Oortwijn and M. Huisman, Practical Abstractions for Automated Verification of Message Passing Concurrency. In iFM, 2019. Best paper award. [external page PDF][external page Git]
  
• W. Ahrendt, L. Henrio and W. Oortwijn, Who is to Blame? Runtime Verification of Distributed Objects with Active Monitors. In VORTEX, 2018. [external page PDF]
  
• W. Oortwijn and W. Ahrendt, Combined Static and Runtime Verification of Distributed Objects. In ICTopen (VERSEN track), 2018. Best IPA poster presentation award.
  
• S. Joosten, W. Oortwijn, M. Safari and M. Huisman, An Exercise in Verifying Sequential Programs with VerCors. In FTfJP, 2018. [external page PDF][external page Git]
• S. Blom, S. Darabi, M. Huisman and W. Oortwijn, The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM, 2017. [external page PDF]
• W. Oortwijn, S. Blom, D. Gurov, M. Huisman and M. Zaharieva-Stojanovski, An Abstraction Technique for Describing Concurrent Program Behaviour. In VSTTE, 2017. [external page PDF]
• W. Oortwijn, T. van Dijk and J. van de Pol, Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN, 2017. Best paper award. [external page PDF][external page Git]
• W. Oortwijn and M. Huisman, Model-based Verification of Distributed Software. In SEN symposium, 2017. [external page PDF]
• W. Oortwijn, S. Blom and M. Huisman, Future-based Static Analysis of Message Passing Programs. In PLACES, 2016. [external page PDF]
• W. Oortwijn, S. Blom and M. Huisman, Static Verification of Message Passing Programs. In ICTOpen, 2016. Best IPA poster presentation award. [external page PDF][external page Poster]
• W. Oortwijn, T. van Dijk and J. van de Pol, A Distributed Hash Table for Shared Memory. In PPAM, 2015. [external page PDF][external page Git]

Theses

• PhD Thesis (December 2019)
  Deductive Techniques for Model-Based Concurrency Verification, University of Twente, the Netherlands. [external page PDF][external page Git]
• MSc Thesis (July 2015)
  Distributed Symbolic Reachability Analysis, University of Twente, the Netherlands. With Honours. [external page PDF][external page Git]
• BSc Thesis (June 2012)
  Project Digitaak, Windesheim University of Applied Sciences, the Netherlands. Cum Laude.

Supervised Student Projects

• Tim Kerkhoven, Extending the Functionality of Sequences in VerCors. BSc Thesis, University of Twente, 2018. [external page PDF]
  
• Janina Torbecke, Symbolic Model Checking with Partitioned BDDs in Distributed Systems. MSC Thesis, University of Twente, 2017. [external page PDF]
• Jelte Zeilstra, Reasoning about Active Object Programs. MSc Thesis, University of Twente, 2016. [external page PDF]
  
• Willem Siers, Correct and Efficient Concurrent Hash Tables in Java. BSc Thesis, University of Twente, 2016. [external page PDF]
  

Academic Service

• Organisation: FTfJP 2020 (external page Chair), VerifyThis 2020 (Co-organiser).
• Program committees: WADT 2020, TACAS 2019 (AEC), OOPSLA 2019 (AEC).
  
• External reviewer: VMCAI 2020, RV 2019, SEFM 2019, CONCUR 2019, FASE 2019, FoSSaCS 2019, FM 2018, TACAS 2018, CPP 2017, ESSoS 2016, FTSCS 2016, iFM 2016, FASE 2016.
  

Other Accomplishments

• Won the VerifyThis best student team award at ETAPS 2019, together with external page Sophie Lathouwers.
  
• Won the VerifyThis student team — silver award at ETAPS 2018, together with external page Mohsen Safari.
  
• Received my BSc degree cum laude in 2012 at Windesheim University of Applied Sciences, and managed to finish the four-year computer science programme within three years.