About me
Since January 2021 I joined ESI (TNO) in Eindhoven as a Research Fellow. There I work on methods and techniques for getting insight into the complex behaviours of industrial cyber-physical systems, and for understanding the impact of software changes on their system behaviour. We recently made a poster and corresponding video about part of our work.
Prior to that I worked at ETH Zurich as a postdoctoral researcher (2019—2020) at the Chair of Programming Methodology led by Peter Muller. At ETH I was involved in the VerifiedSCION project, in which we worked on the full-stack verification of the SCION routing protocol from the high-level design all the way down to the code implementation. In particular I was involved in developing the automated code verifier Gobra for the Go programming language—the implementation language of SCION—as well as techniques for proving properties of SCION and Go programs.
I did my PhD (2015—2019) at the University of Twente in the Formal Methods and Tools research group under supervision of Marieke Huisman. My PhD work investigates how (deductive) verification techniques for code implementations can be combined with (temporal) verification techniques for software designs, in such a way that they complement each other and benefit from each others results. During my PhD I visited the research group of Wolfgang Ahrendt at Chalmers University of Technology in Sweden, to investigate runtime verification of distributed (active) objects.
Research interests
I am interested in methods, techniques and tools for (formally) verifying and validating software-intensive systems, in a broad sense.
I like applying SAT and SMT solving, and automated and interactive theorem proving, for reasoning about algorithms, system/software designs and code implementations. For example I worked on and contributed to the code verifiers Gobra, VerCors and Viper, which translate the problem of establishing program correctness to proof obligations that are ultimately discharged to SMT solvers.
I am particularly interested in combining different specification formalisms and verification techniques (like program logics and model checking) in complementary ways, so that they benefit from each others results. Additionally I am looking into how verification can neatly be integrated in the complete development process of software-intensive systems, in order to increase their effectivity. The different design and engineering phases of system development should go hand-in-hand with their gradual verification, as should the evolution of the system.
Publications
- M. Safari, W. Oortwijn and M. Huisman. Automated Verification of the Parallel Bellman–Ford Algorithm, SAS, 2021.
- F.A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J.C. Pereira, P. Muller. Gobra: Modular Specification and Verification of Go Programs, CAV, 2021.
- W. Oortwijn. FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, 2020.
- W. Oortwijn, D. Gurov and M. Huisman. An Abstraction Technique for Verifying Shared-Memory Concurrency, Applied Sciences, 2020 (sources are on Git).
- M. Safari, W. Oortwijn, S. Joosten and M. Huisman. Formal Verification of Parallel Prefix Sum, NFM, 2020.
- W. Oortwijn, M. Huisman, S. Joosten and J. van de Pol. Automated Verification of Parallel Nested DFS, TACAS, 2020 (with artifact).
- W. Oortwijn, D. Gurov and M. Huisman. Practical Abstractions for Automated Verification of Shared-Memory Concurrency, VMCAI, 2020.
- W. Oortwijn and M. Huisman. Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System, iFM, 2019.
- W. Oortwijn and M. Huisman. Practical Abstractions for Automated Verification of Message Passing Concurrency, iFM, 2019 (sources are on Git). Won the best paper award.
- W. Ahrendt, L. Henrio and W. Oortwijn. Who is to Blame? Runtime Verification of Distributed Objects with Active Monitors, VORTEX, 2018.
- S. Joosten, W. Oortwijn, M. Safari and M. Huisman. An Exercise in Verifying Sequential Programs with VerCors, FTfJP, 2018 (sources are on Git).
- S. Blom, S. Darabi, M. Huisman and W. Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software, iFM, 2017 (sources are on Git).
- W. Oortwijn, S. Blom, D. Gurov, M. Huisman and M. Zaharieva-Stojanovski. An Abstraction Technique for Describing Concurrent Program Behaviour, VSTTE, 2017.
- W. Oortwijn, T. van Dijk and J. van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability, SPIN, 2017 (sources are on Git). Won the best paper award.
- W. Oortwijn and M. Huisman. Model-based Verification of Distributed Software, SEN symposium, 2017.
- W. Oortwijn, S. Blom and M. Huisman. Future-based Static Analysis of Message Passing Programs, PLACES, 2016.
- W. Oortwijn, T. van Dijk and J. van de Pol. A Distributed Hash Table for Shared Memory, PPAM, 2015 (sources are on Git).
Poster presentations
- D. Hendriks, A. van der Meer, W. Oortwijn and B. Huijbrechts. Preventing regressions for software changes, ICT.Open (CompSys track), 2022 (a corresponding pitch video is available here).
- W. Oortwijn and W. Ahrendt. Combined Static and Runtime Verification of Distributed Objects, ICT.Open (VERSEN track), 2018. Won the best IPA poster presentation award.
- W. Oortwijn, S. Blom and M. Huisman. Static Verification of Message Passing Programs, ICT.Open, 2016 (corresponding abstract can be found here). Won the best IPA poster presentation award.
Theses
-
PhD Thesis (December 2019)
Deductive Techniques for Model-Based Concurrency Verification, University of Twente, the Netherlands (sources are on Git). Won the VERSEN PhD Thesis Award 2020, 1st price (see also here). -
MSc Thesis (July 2015)
Distributed Symbolic Reachability Analysis, University of Twente, the Netherlands (sources are on Git). Obtained with Honours distinction. -
BSc Thesis (June 2012)
Project Digitaak, Windesheim University of Applied Sciences, the Netherlands. Obtained with Cum Laude distinction.
Supervised student projects
- Tim Kerkhoven, Extending the Functionality of Sequences in VerCors. BSc Thesis, University of Twente, 2018.
- Janina Torbecke, Symbolic Model Checking with Partitioned BDDs in Distributed Systems. MSc Thesis, University of Twente, 2017.
- Jelte Zeilstra, Reasoning about Active Object Programs. MSc Thesis, University of Twente, 2016.
- Willem Siers, Correct and Efficient Concurrent Hash Tables in Java. BSc Thesis, University of Twente, 2016.
Academic service
- Organisation: FTfJP 2020 (Chair), VerifyThis 2020/2021 (Co-organiser).
- Program committees: FMICS 2022, TACAS 2021 (AEC), WADT 2020, TACAS 2019 (AEC), OOPSLA 2019 (AEC).
- External reviewer: VMCAI 2021, Mathematics 2020, SEFM 2020, 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 Sophie Lathouwers.
- Won the VerifyThis student team—silver award at ETAPS 2018, together with 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.
Software
- TectonicGenerator: Algorithms for generating Tectonic puzzles of various sizes and varying complexity, written as a small hobby project. The algorithms and their implementation are closed source for now, but some generated puzzles can be played here.
- Gobra: A modular automated code verifier for programs written in Go.
- VerCors: An automated and modular verifier that targets concurrent programs written in Java, C, OpenCL and OpenMP.
- DistBDD: A distributed symbolic reachability analysis implementation for high-performance networks of multi-core machines.
Contact
Email: wytseoortwijn at gmail dot com.