Modelling and analysis of a collision avoidance protocol using Spin and Uppaal. - Henrik Ejersbo Jensen; Kim G. Larsen; Arne Skou (The Spin Verification System, 1996)

A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction. - Henrik Ejersbo Jensen; Nancy A. Lynch (TACAS, 1998)

Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction. - Henrik Ejersbo Jensen; Kim Guldstrand Larsen; Arne Skou (FTRTFT, 2000)

Reachability Analysis of Probabilistic Systems by Successive Refinements. - Pedro R. D'Argenio; Bertrand Jeannet; Henrik Ejersbo Jensen; Kim Guldstrand Larsen (PAPM-PROBMIV, 2001)

Reduction and Refinement Strategies for Probabilistic Analysis. - Pedro R. D'Argenio; Bertrand Jeannet; Henrik Ejersbo Jensen; Kim Guldstrand Larsen (PAPM-PROBMIV, 2002)