Techniques for Reactive System Design: The Tools in TRADE. - Roel J. Wieringa; David N. Jansen (CAiSE, 2001)

A Probabilistic Extension of UML Statecharts. - David N. Jansen; Holger Hermanns; Joost-Pieter Katoen (FTRTFT, 2002)

Extending CTL with Actions and Real Time. - David N. Jansen; Roel J. Wieringa (J. Log. Comput., 2002)

Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts. - Rik Eshuis; David N. Jansen; Roel J. Wieringa (Requir. Eng., 2002)

A QoS-Oriented Extension of UML Statecharts. - David N. Jansen; Holger Hermanns; Joost-Pieter Katoen (UML, 2003)

Extensions of Statecharts with probability, time, and stochastic timing. - David N. Jansen (2003)

An industrial-strength formal method – A Modest survey. - Henrik C. Bohnenkamp; Holger Hermanns; David N. Jansen; Joost-Pieter Katoen; Yaroslav S. Usenko (ISoLA (Preliminary proceedings), 2004)

Dependability Checking with StoCharts: Is Train Radio Reliable Enough for Trains? - David N. Jansen; Holger Hermanns (QEST, 2004)

Logic and Model Checking for Hidden Markov Models. - Lijun Zhang 001; Holger Hermanns; David N. Jansen (FORTE, 2005)

From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. - Holger Hermanns; David N. Jansen; Yaroslav S. Usenko (WOSP, 2005)

QoS modelling and analysis with UML-statecharts: the StoCharts approach. - David N. Jansen; Holger Hermanns (SIGMETRICS Perform. Evaluation Rev., 2005)

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

07101 Working Group Report – Performance Measures Other Than Time. - Lucia Cloth; Pepijn Crouzen; Matthias Fruth; Tingting Han 001; David N. Jansen; Mark Kattenbelt; Gerard J. M. Smit; Lijun Zhang 001 (Quantitative Aspects of Embedded Systems, 2007)

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. - David N. Jansen; Joost-Pieter Katoen; Marcel Oldenkamp; Mariëlle Stoelinga; Ivan S. Zapreev (Haifa Verification Conference, 2007)

Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. - Joost-Pieter Katoen; Tim Kemna; Ivan S. Zapreev; David N. Jansen (TACAS, 2007)

Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. - Lijun Zhang 001; Holger Hermanns; Friedrich Eisenbrand; David N. Jansen (Log. Methods Comput. Sci., 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)

Synthesis and stochastic assessment of cost-optimal schedules. - Angelika Mader; Henrik C. Bohnenkamp; Yaroslav S. Usenko; David N. Jansen; Johann L. Hurink; Holger Hermanns (Int. J. Softw. Tools Technol. Transf., 2010)

Erratum to: Model-checking continuous-time Markov chains by Aziz et al - David N. Jansen (CoRR, 2011)

Automata-Based CSL Model Checking - Lijun Zhang 001; David N. Jansen; Flemming Nielson; Holger Hermanns (Log. Methods Comput. Sci., 2011)

The ins and outs of the probabilistic model checker MRMC. - Joost-Pieter Katoen; Ivan S. Zapreev; Ernst Moritz Hahn; Holger Hermanns; David N. Jansen (Perform. Evaluation, 2011)

Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm. - David N. Jansen; Flemming Nielson; Lijun Zhang 001 (NASA Formal Methods, 2012)

On Abstraction of Probabilistic Systems. - Christian Dehnert; Daniel Gebler; Michele Volpato; David N. Jansen (ROCKS, 2012)

More or Less True DCTL for Continuous-Time MDPs. - David N. Jansen (FORMATS, 2013)

Revisiting Weak Simulation for Substochastic Markov Chains. - David N. Jansen; Lei Song 001; Lijun Zhang 001 (QEST, 2013)

Applying Automata Learning to Embedded Control Software. - Wouter Smeenk; Joshua Moerman; Frits W. Vaandrager; David N. Jansen (ICFEM, 2015)

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. - Tom van Dijk; Ernst Moritz Hahn; David N. Jansen; Yong Li 031; Thomas Neele; Mariëlle Stoelinga; Andrea Turrini; Lijun Zhang 001 (SETTA, 2015)

Minimal Separating Sequences for All Pairs of States. - Rick Smetsers; Joshua Moerman; David N. Jansen (LATA, 2016)

Stuttering equivalence is too slow! - David N. Jansen; Jeroen J. A. Keiren (CoRR, 2016)

A space-efficient simulation algorithm on probabilistic automata. - Lijun Zhang 001; David N. Jansen (Inf. Comput., 2016)

Multiphase until formulas over Markov reward models: An algebraic approach. - Ming Xu 010; Lijun Zhang 001; David N. Jansen; Huibiao Zhu; Zongyuan Yang (Theor. Comput. Sci., 2016)

Finding Polynomial Loop Invariants for Probabilistic Programs. - Yijun Feng; Lijun Zhang 001; David N. Jansen; Naijun Zhan; Bican Xia (ATVA, 2017)

Distribution-Based Bisimulation for Labelled Markov Processes. - Pengfei Yang 002; David N. Jansen; Lijun Zhang 001 (FORMATS, 2017)

On Equivalence Checking of Nondeterministic Finite Automata. - Chen Fu; Yuxin Deng; David N. Jansen; Lijun Zhang 001 (SETTA, 2017)

An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation. - Jan Friso Groote; David N. Jansen; Jeroen J. A. Keiren; Anton Wijs (ACM Trans. Comput. Log., 2017)

Probabilistic bisimulation for realistic schedulers. - Lijun Zhang 001; Pengfei Yang 002; Lei Song 001; Holger Hermanns; Christian Eisentraut; David N. Jansen; Jens Chr. Godskesen (Acta Informatica, 2018)

An Automatic Proving Approach to Parameterized Verification. - Yongjian Li; Kaiqiang Duan; David N. Jansen; Jun Pang 001; Lijun Zhang 001; Yi Lv; Shaowei Cai 001 (ACM Trans. Comput. Log., 2018)

An Axiomatisation of the Probabilistic mu -Calculus. - Junnan Xu; Wanwei Liu; David N. Jansen; Lijun Zhang 001 (ICFEM, 2019)

A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems. - David N. Jansen; Jan Friso Groote; Jeroen J. A. Keiren; Anton Wijs (CoRR, 2019)

A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. - David N. Jansen; Jan Friso Groote; Ferry Timmers; Pengfei Yang 002 (CONCUR, 2020)

Accelerated Verification of Parametric Protocols with Decision Trees. - Yongjian Li; Taifeng Cao; David N. Jansen; Jun Pang 001; Xiaotao Wei (ICCD, 2020)

An O(m log n) algorithm for branching bisimilarity on labelled transition systems. - David N. Jansen; Jan Friso Groote; Jeroen J. A. Keiren; Anton Wijs (TACAS (2), 2020)

Formal Verification of Consensus in the Taurus Distributed Database. - Song Gao 014; Bohua Zhan; Depeng Liu; Xuechao Sun; Yanan Zhi; David N. Jansen; Lijun Zhang 001 (FM, 2021)

Frontmatter: mining Android user interfaces at scale. - Konstantin Kuznetsov 001; Chen Fu; Song Gao 014; David N. Jansen; Lijun Zhang 001; Andreas Zeller (ESEC/SIGSOFT FSE, 2021)

What do all these Buttons do? Statically Mining Android User Interfaces at Scale. - Konstantin Kuznetsov 001; Chen Fu; Song Gao 014; David N. Jansen; Lijun Zhang 001; Andreas Zeller (CoRR, 2021)

Rooted Divergence-Preserving Branching Bisimilarity is a Congruence: A Simpler Proof. - David N. Jansen; Xinxin Liu (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). - Shizhen Yu; Yifan Dong; Jiuyang Liu; Yong Li 031; Zhilin Wu; David N. Jansen; Lijun Zhang 001 (SEFM, 2022)

Deciding All Behavioral Equivalences at Once: A Game for Linear-Time-Branching-Time Spectroscopy. - Benjamin Bisping; David N. Jansen; Uwe Nestmann (Log. Methods Comput. Sci., 2022)

Linear-Time-Branching-Time Spectroscopy Accounting for Silent Steps. - Benjamin Bisping; David N. Jansen (CoRR, 2023)

Rooted Divergence-Preserving Branching Bisimilarity is a Congruence for Guarded CCS. - Quan Sun; David N. Jansen; Xinxin Liu; Wei Zhang (Formal Aspects Comput., 2023)

A Scenario Approach for Parametric Markov Decision Processes. - Zhiming Chi; Ying Liu 048; Andrea Turrini; Lijun Zhang 001; David N. Jansen (Principles of Verification (2), 2024)

Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. - Weizhi Feng; Yicheng Liu; Jiaxiang Liu 001; David N. Jansen; Lijun Zhang 001; Zhilin Wu (DAC, 2024)

One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics. - Benjamin Bisping; David N. Jansen (EXPRESS/SOS, 2024)

A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. - Jan Friso Groote; David N. Jansen (CONCUR, 2025)