Research Interests

• (Multi-core) Model checking (of abstractions/of timed systems/of programs)
• Program analysis using model checking
• (Worst-Case) Execution Time/Energy Analysis

Tools

opaal

I am one of the main developers of the tool opaal, which is a model checker for timed automata, or more generally automata with monotonic behaviour given by a lattice-like structure.

opaal is compatible with UPPAAL.

METAMOC

Modular Execution Time Analysis using MOdel Checking (METAMOC website) is a toolchain that uses model checking of timed automata (UPPAAL) to perform worst-case execution time analysis for ARM7, ARM9 and ATMEL AVR 8-bit binaries.

It is the product of my joint master thesis with Martin Toft and Andreas Dalsgaard, for which we were awarded the Roblon Award of 2009, for an outstanding thesis.

Referencer

Referencer is a program for keeping track of references for Linux. It supports tagging, generating BibTex files and much more. From time to time, I write patches for Referencer.

Publications

My list of publications can be seen below, at VBN, at DBLP or at Google Scholar.

Towards Translating FSM-SADF to Timed Automata

Mladen Skelin, Erik Ramsgaard Wognsen, Mads Chr. Olesen, René Rydhof Hansen, Kim Guldstrand Larsen
In Workshop on Investigating Dataflow in Embedded computing Architectures (IDEA), 2015.

Formal Methods for Modelling and Analysis of Single-Event Upsets

René Rydhof Hansen, Kim Guldstrand Larsen, Mads Chr. Olesen, Erik Ramsgaard Wognsen
In Proceedings of the 3rd IEEE International Workshop on Formal Methods Integration (FMi), 2015, IEEE.

Model Checking of Finite-state Machine-based Scenario-aware Dataflow Using Timed Automata

Mladen Skelin, Erik Ramsgaard Wognsen, Mads Chr. Olesen, René Rydhof Hansen, Kim Guldstrand Larsen
In Proceedings of the 10th IEEE International Symposium on Industrial Embedded Systems (SIES), pages 235--244, 2015, IEEE.

Coccinelle: Tool support for automated CERT C Secure Coding Standard certification

Mads Chr. Olesen, René Rydhof Hansen, Julia L. Lawall, Nicolas Palix
In Science of Computer Programming (SCP), pages 141--160, 2014.

Formalisation and Analysis of Dalvik Bytecode

Erik Ramsgaard Wognsen, Henrik Søndberg Karlsen, Mads Chr. Olesen, René Rydhof Hansen
In Science of Computer Programming (SCP), pages 25--55, 2014.

Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction

Alfons Laarman, Mads Chr. Olesen, Andreas Dalsgaard, Kim G. Larsen, Jaco van de Pol
In Proceedings of the 25th International Conference on Computer Aided Verification (CAV), pages 968-983, 2013, Springer.

PtrTracker: Pragmatic Pointer Analysis

Sebastian Biallas, Mads Chr. Olesen, Franck Cassez, Ralf Huuck
In Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 2013, IEEE Computer Society.

Program Analysis as Model Checking

Mads Chr. Olesen
PhD thesis, Aalborg University, defended Dec. 2013.

Study, Formalisation, and Analysis of Dalvik Bytecode

Henrik Søndberg Karlsen, Erik Ramsgaard Wognsen, Mads Chr. Olesen, René Rydhof Hansen
In Informal Proceedings of the Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode), 2012.

What is a Timing Anomaly?

Franck Cassez, René Rydhof Hansen, Mads Chr. Olesen
In Proceedings of the 12th International Workshop on Worst-Case Execution-Time Analysis (WCET), pages 1-12, 2012, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.

THAPS: Automated Vulnerability Scanning of PHP Applications

Torben Jensen, Heine Pedersen, Mads Chr. Olesen, René Rydhof Hansen
In Proceedings of the 17th Nordic Conference on Secure IT Systems (NordSec), pages 31-46, 2012, Springer.

Multi-core Reachability for Timed Automata

Andreas Engelbredt Dalsgaard, Alfons Laarman, Kim G. Larsen, Mads Chr. Olesen, Jaco van de Pol
In Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 91-106, 2012, Springer.

Adaptable Value-Set Analysis for Low-Level Code

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, Mads Chr. Olesen
In Proceedings of the 6th International Workshop on Systems Software Verification (SSV), pages 32-43, 2011.

opaal: A Lattice Model Checker

Andreas Engelbredt Dalsgaard, René Rydhof Hansen, Kenneth Yrke Jørgensen, Kim Guldstrand Larsen, Mads Chr. Olesen, Petur Olsen, Jiří Srba
In Proceedings of the International Symposium NASA Formal Methods (NFM), pages 487-493, 2011, Springer.

Clang and Coccinelle: Synergising program analysis tools for CERT C Secure Coding Standard certification

Mads Chr. Olesen, René Rydhof Hansen, Julia Lawall, Nicolas Palix
In Pre-proceedings of the 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert), pages 51-69, 2010.

METAMOC: Modular Execution Time Analysis Using Model Checking

Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, Kim G. Larsen
In Proceedings of the 10th International Workshop on Worst-Case Execution Time Analysis (WCET), pages 114-124, 2010.

Modular Execution Time Analysis Using Model Checking (METAMOC)

Andreas Engelbredt Dalsgaard, Mads Christian Olesen, Martin Toft
Masters thesis, Aalborg University, July 2009.

Contact Information

Email: mchro cs.aau.dk

To arrange a meeting and view my available times, you can use my Doodle MeetMe page.