Probably on Time and within Budget: On Reachability in Priced Probabilistic Timed Automata. - Jasper Berendsen; David N. Jansen; Joost-Pieter Katoen (QEST, 2006)

Compositional Abstraction in Real-Time Model Checking. - Jasper Berendsen; Frits W. Vaandrager (FORMATS, 2008)

Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata. - Jasper Berendsen; Taolue Chen 001; David N. Jansen (TAMC, 2009)

Fortuna: Model Checking Priced Probabilistic Timed Automata. - Jasper Berendsen; David N. Jansen; Frits W. Vaandrager (QEST, 2010)

The axiomatization of override and update. - Jasper Berendsen; David N. Jansen; Julien Schmaltz; Frits W. Vaandrager (J. Appl. Log., 2010)

Formal specification and analysis of zeroconf using uppaalS. - Jasper Berendsen; Biniam Gebremichael; Frits W. Vaandrager; Miaomiao Zhang (ACM Trans. Embed. Comput. Syst., 2011)