Marieke Huisman – University of Twente

 

Marieke Huisman

Associate Professor in Program Verification

Dr. Huisman is site-leader of the EU project CARP (Correct and Efficient Accelerator Programming, 2011 – 2014). Together with Matej Mihelcic she works in the project on the semantics of a high-level GPGPU programming language (Pencil, currently under development), and on the verification of programs written in Pencil and OpenCL.

In addition, she leads the ERC VerCors project on Verification of Concurrent Data Structures (2011 – 2016), and the NWO project SlaLoM (Security by Logic for Multithreaded Applications). Her research themes are: specification and verification of concurrent software, platform formalisations, formal methods for security, program annotation generation, and algorithmic compositional verification techniques.
She obtained her Phd thesis in 2001 from the Radboud University, Nijmegen on verification of Java programs.

Correct and Effecient Accelerator Programs (CARP project)

The CARP European research project aims at improving the programmability of accelerated systems, particularly systems accelerated with GPUs, at all levels. In particular, it will design

  • novel and attractive methods for constructing system-independent accelerator programs
  • advanced code generation techniques to produce highly optimised system-specific code from system-independent programs; and
  • scalable static techniques for analysing accelerator software both qualitatively and quantitatively.

These methods will provide a unified development flow for accelerated software, reducing cost and time-to-market quotas, increasing energy efficiency (and thus battery life in mobile devices) and improving reliability.

Other partners in the project are: Imperial College London (coordinator), United Kingdom, ARM, United Kingdom, Realeyes, Estonia, RWTH Aachen University, Germany, Monoidics, United Kingdom, ENS, France, and Rightware, Finland.

Within the project, a new high-level GPGPU programming languge will be developed, called Pencil with a compiler to OpenCL. The CARP team at the University of Twente will develop a formal semantics for this language, and it will develop verification techniques for Pencil programs. The verification techniques will be based on permission-based separation logic, an extension of Hoare logic that is particularly suitable for multithreaded programs.

Formal Methods and Tools Group, University of Twente

The research of the Formal Methods and Tools Group (FMT), led by Prof.Dr. Jaco van de Pol focuses on the development of mathematical theories, methods, algorithms and high-performance tools for the design of software-intensive embedded systems, facilitating the modelling, analysis and prediction of their functional and quantitative aspects.

They build on extensive experience in concurrency theory (in particular process algebra and graph rewriting), theorem proving and model checking algorithms. Also, automated model-based testing plays an important role. Our focus areas are:

  • applications to complex object-oriented models and software (UML, Java);
  • modelling and analysis of quantitative aspects for embedded and hybrid systems;
  • high-performance analysis tools.

Relevant URLs:
Marieke Huisman: http://wwwhome.ewi.utwente.nl/~marieke/
CARP website: http://www.carpproject.eu/
CARP@UTwente: http://fmt.ewi.utwente.nl/research/projects/CARP/
FMT website: http://fmt.ewi.utwente.nl/

 

Talk: Correct and Efficient Accelerator Programming