News

Two papers accepted at iFM 2019

October 09, 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.

Blind Henk Mulder now receives a master degree

July 10, 2019

On July 10th, 2019, Henk Mulder got his Master degree at University of Twente.

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.

Thesis document

Henk Mulder got a 9 for his Master project, and graduated Cum laude. Our congratulations go out to Henk Mulder, on this great accomplishment!

VERCORS Advisory Board Meeting

June 06, 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 include people from BetterBe , Thales group, Rosen group, Polder Valley and Technolution.

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.

New PostDoc in Mercedes Project

June 03, 2019

Raúl E. Monti joined VerCors Team and started as a PostDoc on the Mercedes project.

NWO OTP grant for ChEOPS (verified Construction of corrEct and Optimised Parallel Software) Project

May 16, 2019

Prof.dr. Marieke Huisman and dr. Anton Wijs received an NWO OTP grant for the project “ChEOPS: verified Construction of corrEct and Optimised Parallel Software”.

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.

VerifyThis2019

April 15, 2019

VerCors Team participated in ETAPS 2019 conference for VerifyThis competition, held in Parague and have won two awards.

Sophie Lathouwers and Wytse Oortwijn won the Best Student Team award!

Marieke Huisman and Sebastiaan Joosten won the “Most Distinguished Tool Feature Award” for their usage of ghost method parameters to model sparse matrices!

New PhD Candidate in Mercedes

December 03, 2018

Sophie Lathouwers started as a PhD student on the Mercedes project. Sophie will investigate the automated generation of auxiliary annotations, which are needed for program verification in VerCors.

Symposium Paper

November 16, 2018

During the symposium organised for the 60th birthday of 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.

ISoLA 2018

November 05, 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.

New Master Student

September 01, 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.

Marieke Huisman, Stefan Blom (BetterBe) and Sebastiaan Joosten will supervise the project.

FTfFP 2018

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.

VerifyThis2018

April 14, 2018

Two VerCors teams participated in this year’s VerifyThis program verification competition, held in Thessaloniki as part of ETAPS 2018.

Wytse Oortwijn and Mohsen Safari won the 2nd prize for the best student team.

New PhD Students in Mercedes Project

February 15, 2018

Two new PhD students started on the Mercedes project: Mohsen Safari and Fauzia Ehsan.

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.

Marieke Huisman Inaugural Lecture

January 25, 2018

Marieke Huisman gives her inaugural lecture, entitled “Software Reliability for Everyone”.

In this lecture, she presents her view on the future of software verification research.

Booklet inaugural lecture

>