Dr. Wytse Oortwijn

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 pageSCION 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 pageGo language, as well as techniques for proving properties of SCION and Go programs.

I did my PhD (20152019) at external pageFormal Methods and Tools research group at the external pageUniversity of Twente, under supervision of external pageMarieke Huisman. My PhD thesis, titled external pageDeductive 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 pageWolfgang Ahrendt at external pageChalmers University of Technology in Sweden, to work on runtime verification of distributed (active) objects.

In my Master's degree at the University of Twente (20122015) 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 pageArtifact]
  • 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 pagePDF]
  • W. Oortwijn and M. Huisman, Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In iFM, 2019. [external pagePDF]
  • W. Oortwijn and M. Huisman, Practical Abstractions for Automated Verification of Message Passing Concurrency. In iFM, 2019. Best paper award. [external pagePDF][external pageGit]
  • W. Ahrendt, L. Henrio and W. Oortwijn, Who is to Blame? Runtime Verification of Distributed Objects with Active Monitors. In VORTEX, 2018. [external pagePDF]
  • 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 pagePDF][external pageGit]
  • S. Blom, S. Darabi, M. Huisman and W. Oortwijn, The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM, 2017. [external pagePDF]
  • W. Oortwijn, S. Blom, D. Gurov, M. Huisman and M. Zaharieva-Stojanovski, An Abstraction Technique for Describing Concurrent Program Behaviour. In VSTTE, 2017. [external pagePDF]
  • W. Oortwijn, T. van Dijk and J. van de Pol, Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN, 2017. Best paper award. [external pagePDF][external pageGit]
  • W. Oortwijn and M. Huisman, Model-based Verification of Distributed Software. In SEN symposium, 2017. [external pagePDF]
  • W. Oortwijn, S. Blom and M. Huisman, Future-based Static Analysis of Message Passing Programs. In PLACES, 2016. [external pagePDF]
  • W. Oortwijn, S. Blom and M. Huisman, Static Verification of Message Passing Programs. In ICTOpen, 2016. Best IPA poster presentation award. [external pagePDF][external pagePoster]
  • W. Oortwijn, T. van Dijk and J. van de Pol, A Distributed Hash Table for Shared Memory. In PPAM, 2015. [external pagePDF][external pageGit]

Theses

Supervised Student Projects

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

Academic Service

  • Organisation: FTfJP 2020 (external pageChair), 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 pageSophie Lathouwers.
  • Won the VerifyThis student team — silver award at ETAPS 2018, together with external pageMohsen 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.

 

JavaScript has been disabled in your browser