August 21, 2020
Our papers Mohsen Safari and Marieke Huisman - A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms, and Lars van den Haak, Anton Wijs, Mark van den Brand and Marieke Huisman - Formal methods for GPGPU programming: is the demand met? were accepted in iFM 2020. Moreover, the former paper is our first ChEOPS project paper.
June 1, 2020
Two of our ex-master students, Bob Rubbens and Ömer Şakar, have recently graduated (see here and here ) and have decided to join the VerCors team as PhD candidates in the Mercedes project and ChEOPS project respectively. Nice that we have managed to keep them with us!
March 11, 2020
February 21, 2020
Formal Verification of Parallel Prefix Sum written by Mohsen, Wytse, Sebastiaan and Marieke has been accepted for this year edition of NFM .
February 20, 2020
Automated Verification of Parallel Nested DFS written by Wytse, Marieke, Sebastiaan and Jaco has been accepted for this years edition of TACAS.
February 19, 2020
The paper Practical Abstractions for Automated Verification of Message Passing Concurrency written by Wytse Oortwijn and Marieke Huisman got the best paper award at IFM 2019 conference .
February 1, 2020
From February 1st, Petra van den Bos has joined our team as a PostDoc under the Mercedes Project. Petra finished her PhD studies at the Institute for Computing and Information Sciences of the Radboud University in Nijmegen, the Netherlands, under the supervision of Jan Tretmans and Frits Vaandrager. During her work she focussed on topics around model-based testing. However, she also enjoys working on other topics inside formal methods and we are very happy to have her working along us and improving VerCors.
December 12, 2019
On the occasion of Wytse Oortwijn’s PhD defence, a big part of the VerCors (former and current) team members got reunited. We were able to take this very nice picture together:
May 2020 bring even more people into our picture!
November 4, 2019
Anton Wijs and Maciej Wiłkowski present a paper involving VerCors at SEFM 2019
In Modular Indirect Push-Button Formal Verification of Multi-threaded Code Generators, Anton Wijs and Maciej Wiłkowski use VerCors to assist the verification of automated code generation of multi-threaded programs for model-driven development.
FMT member Sophie Lathouwers wins the Greenhost prize of the Koninklijke Hollandsche Maatschappij der Wetenschappen
November 4, 2019
The prize is in the category of Internet & Technical Sciences, it is awarded through the KHMW (Royal Dutch Institute of Sciences), and sponsored by Greenhost. The prize-giving ceremony will take place on Thursday November 7 next at 15:00 in Amsterdam (REC, room C0.01, Nieuwe Achtergracht 166). There, Sophie will give a short presentation on her work. For more information visit here .
November 4, 2019
Wytse Oortwijn PHD thesis defence is approaching
Wytse has contributed to VerCors for several years, during his PhD projects in the FMT group under the supervision of Prof Marieke Huisman. He will be defending his thesis, entitled “Deductive Techniques for Model-Based Concurrency Verification” on Thursday 12th of December, 16:30 to 18:00 at Waaier, 4-G, Berkhoffzaal, University of Twente. For an introduction to his thesis and more information about the defence follow this link.
November 4, 2019
Prof. Marieke Huisman, leader of the FMT group and the VerCors team, was one of the speakers at a public symposium called Verificatie van software: erg complex maar in ieders belang (Software verification: very complex but in everyone’s interest) at the Koninklijke Nederlandse Akademie van Wetenschappen.
She gave an overview of the area of deductive program verification, and how VerCors contributes to this area. Here’s an impression of the evening. A recording of the symposium will be made available via TXT radio.
October 9, 2019
Two papers written by Wytse Oortwijn and Marieke Huisman have been accepted in this year’s edition of iFM.
“Practical Abstractions for Automated Verification of Message Passing Concurrency” presenting a new technique which integrates model based verification and code verification for message passing programs and “Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System”, a case study in the use of VerCors in a critical industrial system, have been accepted at the 15th International Conference on integrated Formal Methods taking place between the 2nd and the 6th of December this year, at Bergen, Norway.
July 10, 2019
Henk Mulder did his Master Thesis at the Formal Methods and Tools group, on identifying and solving bottlenecks in the VerCors tool, under the supervision of Marieke Huisman. The VerCors toolset can be used to verify memory safety and functional correctness of concurrent and parallel programs. By encoding the problem into an intermediate language the power of existing tools is leveraged to support additional concurrency models. However, for certain programs verification takes significant time. Thanks to the work of Henk Mulder, we now know why, and more importantly, what we can do about it.
Henk Mulder got a 9 for his Master project, and graduated Cum laude. Our congratulations go out to Henk Mulder, on this great accomplishment!
June 6, 2019
An advisory board meeting of VerCors was held in University of Twente on June 6, 2019. VerCors Team elaborated main tool features with the board members from different industrial organizations.
The board members have shown a deep interest in the tool and gave valuable feedback to make the VerCors tool more applicable and efficient for industrial projects.
June 3, 2019
May 16, 2019
Two PhD students will be appointed, one in Twente and one in Eindhoven, to make the development and maintenance of software aimed at graphics processing units (GPUs) more insightful and effective in terms of functional correctness and performance.
GPUs have an increasingly big impact on industry and academia, due to their great computational capabilities. However, in practice, one usually needs to have expert knowledge on GPU architectures to optimally gain advantage of those capabilities. At the Eindhoven University of Technology, Wijs will work on modelling GPU applications using a Domain Specific Language, formally verifying the correctness of the models, and automatically generating GPU code. At the University of Twente, Huisman will work on the structured optimisation of GPU code, while ensuring that functional correctness is preserved. Existing formal verification techniques, model checking and code verification, will be combined to create, for the first time, a complete end-to-end development workflow for GPU applications.
To ensure the practical effectiveness of the resulting workflow, a users committee, consisting of SURFsara, the Netherlands eScience Center, Stream HPC, and CodePlay (UK), will provide real-life cases and provide feedback throughout the project.
April 15, 2019
December 3, 2018
November 16, 2018
During the symposium organised for the
60th birthdayof Arnd Poetzsch-Heffter, Marieke Huisman presented a position paper “Towards Reliable Concurrent Software”, co-authored with Sebastiaan Joosten, which outlines the plans of the Mercedes project.
November 5, 2018
ISOLA 2018 features several presentations around VerCors.
Marieke Huisman presents the position paper “On Models and Code - A Unified Approach to Support Large-Scale Deductive Program Verification”.
In this paper, she argues that we need a seamless transition between models and code, and she sketches how the VerCors tool provides a first step towards this goal.
Marieke Huisman also presented the paper Program Correctness by Transformation, co-authored by Stefan Blom, Saeed Darabi and Mohsen Safari, which describes how the VerCors tool can be used to ensure that program transformations and optimisations preserve program correctness.
Finally, Sebastiaan Joosten presented Static Code Verification Through Process Models, co-authored by Marieke Huisman, which sketches an alternative approach for the use of abstractions to reason about concurrent software.
September 1, 2018
Minh Nguyen starts his final Master thesis project, in which he will try to verify functional correctness of a red black tree using VerCors.
July 16, 2018
The workshop FTfFP 2018 (@ECOOP 2018) features several VerCors related presentations. Wytse Oortwijn gives a tool demo of the VerCors tool set, while Sebastiaan Joosten presents the paper An Exercise in Verifying Sequential Programs with VerCors, co-authored by Wytse Oortwijn, Mohsen Safari and Marieke Huisman.
In this paper, we present our solutions to two of the VerifyThis 2018 challenges.
April 14, 2018
February 15, 2018
Mohsen’s project will contribute to further improvement of the verification of GPU programs in VerCors. Fauzia’s project will focus on the effective use of abstractions to reason about concurrent or distributed programs, using VerCors.