METAMOC: Modular Execution Time Analysis using Model Checking. - Andreas Engelbredt Dalsgaard; Mads Chr. Olesen; Martin Toft; René Rydhof Hansen; Kim Guldstrand Larsen (WCET, 2010)

Clang and Coccinelle: Synergising program analysis tools for CERT C Secure Coding Standard certification. - Mads Chr. Olesen; René Rydhof Hansen; Julia L. Lawall; Nicolas Palix (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

opaal: A Lattice Model Checker. - Andreas Engelbredt Dalsgaard; René Rydhof Hansen; Kenneth Yrke Jørgensen; Kim Guldstrand Larsen; Mads Chr. Olesen; Petur Olsen; Jirí Srba (NASA Formal Methods, 2011)

Adaptable Value-Set Analysis for Low-Level Code. - Jörg Brauer; René Rydhof Hansen; Stefan Kowalewski; Kim G. Larsen; Mads Chr. Olesen (SSV, 2011)

Multi-core Reachability for Timed Automata. - Andreas Engelbredt Dalsgaard; Alfons Laarman; Kim G. Larsen; Mads Chr. Olesen; Jaco van de Pol (FORMATS, 2012)

THAPS: Automated Vulnerability Scanning of PHP Applications. - Torben Jensen; Heine Pedersen; Mads Chr. Olesen; René Rydhof Hansen (NordSec, 2012)

What is a Timing Anomaly?. - Franck Cassez; René Rydhof Hansen; Mads Chr. Olesen (WCET, 2012)

Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction. - Alfons Laarman; Mads Chr. Olesen; Andreas Engelbredt Dalsgaard; Kim Guldstrand Larsen; Jaco van de Pol (CAV, 2013)

PtrTracker: Pragmatic pointer analysis. - Sebastian Biallas; Mads Chr. Olesen; Franck Cassez; Ralf Huuck (SCAM, 2013)

Coccinelle: Tool support for automated CERT C Secure Coding Standard certification. - Mads Chr. Olesen; René Rydhof Hansen; Julia L. Lawall; Nicolas Palix (Sci. Comput. Program., 2014)

Formalisation and analysis of Dalvik bytecode. - Erik Ramsgaard Wognsen; Henrik Søndberg Karlsen; Mads Chr. Olesen; René Rydhof Hansen (Sci. Comput. Program., 2014)

Modelling Social-Technical Attacks with Timed Automata. - Nicolas David 002; Alexandre David; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Mads Chr. Olesen; Christian W. Probst (MIST@CCS, 2015)

Formal Methods for Modelling and Analysis of Single-Event Upsets. - René Rydhof Hansen; Kim Guldstrand Larsen; Mads Chr. Olesen; Erik Ramsgaard Wognsen (IRI, 2015)

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 (SIES, 2015)

An Automata-Based Approach to Trace Partitioned Abstract Interpretation. - Mads Christian Olesen; René Rydhof Hansen; Kim Guldstrand Larsen (Semantics, Logics, and Calculi, 2016)

Modelling Attack-defense Trees Using Timed Automata. - Olga Gadyatskaya; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Mads Chr. Olesen; Danny Bøgsted Poulsen (FORMATS, 2016)

Formal modelling and analysis of Bitflips in ARM assembly code. - René Rydhof Hansen; Kim Guldstrand Larsen; Mads Chr. Olesen; Erik Ramsgaard Wognsen (Inf. Syst. Frontiers, 2016)

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation. - Andreas Engelbredt Dalsgaard; Søren Enevoldsen; Peter Fogh; Lasse S. Jensen; Tobias Skovgaard Jepsen; Isabella Kaufmann; Kim G. Larsen; Søren M. Nielsen; Mads Chr. Olesen; Samuel Pastva; Jirí Srba (Petri Nets, 2017)

A Distributed Fixed-Point Algorithm for Extended Dependency Graphs. - Andreas Engelbredt Dalsgaard; Søren Enevoldsen; Peter Fogh; Lasse S. Jensen; Peter Gjøl Jensen; Tobias Skovgaard Jepsen; Isabella Kaufmann; Kim G. Larsen; Søren M. Nielsen; Mads Chr. Olesen; Samuel Pastva; Jirí Srba (Fundam. Informaticae, 2018)