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 pageSCIONcall_made 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 pageGocall_made language, as well as techniques for proving properties of SCION and Go programs.
I did my PhD (2015—2019) at external pageFormal Methods and Toolscall_made research group at the external pageUniversity of Twentecall_made, under supervision of external pageMarieke Huismancall_made. My PhD thesis, titled external pageDeductive Techniques for Model-Based Concurrency Verificationcall_made, 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 Ahrendtcall_made at external pageChalmers University of Technologycall_made 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 pageArtifactcall_made]
- 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 pagePDFcall_made]
- W. Oortwijn and M. Huisman, Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In iFM, 2019. [external pagePDFcall_made]
- W. Oortwijn and M. Huisman, Practical Abstractions for Automated Verification of Message Passing Concurrency. In iFM, 2019. Best paper award. [external pagePDFcall_made][external pageGitcall_made]
- W. Ahrendt, L. Henrio and W. Oortwijn, Who is to Blame? Runtime Verification of Distributed Objects with Active Monitors. In VORTEX, 2018. [external pagePDFcall_made]
- 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 pagePDFcall_made][external pageGitcall_made]
- S. Blom, S. Darabi, M. Huisman and W. Oortwijn, The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM, 2017. [external pagePDFcall_made]
- W. Oortwijn, S. Blom, D. Gurov, M. Huisman and M. Zaharieva-Stojanovski, An Abstraction Technique for Describing Concurrent Program Behaviour. In VSTTE, 2017. [external pagePDFcall_made]
- W. Oortwijn, T. van Dijk and J. van de Pol, Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN, 2017. Best paper award. [external pagePDFcall_made][external pageGitcall_made]
- W. Oortwijn and M. Huisman, Model-based Verification of Distributed Software. In SEN symposium, 2017. [external pagePDFcall_made]
- W. Oortwijn, S. Blom and M. Huisman, Future-based Static Analysis of Message Passing Programs. In PLACES, 2016. [external pagePDFcall_made]
- W. Oortwijn, S. Blom and M. Huisman, Static Verification of Message Passing Programs. In ICTOpen, 2016. Best IPA poster presentation award. [external pagePDFcall_made][external pagePostercall_made]
- W. Oortwijn, T. van Dijk and J. van de Pol, A Distributed Hash Table for Shared Memory. In PPAM, 2015. [external pagePDFcall_made][external pageGitcall_made]
Theses
- PhD Thesis (December 2019)
Deductive Techniques for Model-Based Concurrency Verification, University of Twente, the Netherlands. [external pagePDFcall_made][external pageGitcall_made] - MSc Thesis (July 2015)
Distributed Symbolic Reachability Analysis, University of Twente, the Netherlands. With Honours. [external pagePDFcall_made][external pageGitcall_made] - 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 pagePDFcall_made]
- Janina Torbecke, Symbolic Model Checking with Partitioned BDDs in Distributed Systems. MSC Thesis, University of Twente, 2017. [external pagePDFcall_made]
- Jelte Zeilstra, Reasoning about Active Object Programs. MSc Thesis, University of Twente, 2016. [external pagePDFcall_made]
- Willem Siers, Correct and Efficient Concurrent Hash Tables in Java. BSc Thesis, University of Twente, 2016. [external pagePDFcall_made]
Academic Service
- Organisation: FTfJP 2020 (external pageChaircall_made), 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 Lathouwerscall_made.
- Won the VerifyThis student team — silver award at ETAPS 2018, together with external pageMohsen Safaricall_made.
- 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.