David N. Jansen

67 papers A* 1A 3B 5C 6Misc 2Journal 25Unranked 22

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	A Formally Verified Procedure for Width Inference in FIRRTL. ESOP (2) Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen
2026	J	`jnl`	A Formally Verified Procedure for Width Inference in FIRRTL. CoRR Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Taolue Chen, Fu Song, David N. Jansen
2025	B	`conf`	A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. CONCUR Jan Friso Groote, David N. Jansen
2024	—	`conf`	A Scenario Approach for Parametric Markov Decision Processes. Principles of Verification (2) Zhiming Chi, Ying Liu, Andrea Turrini, Lijun Zhang, David N. Jansen
2024	A*	`conf`	Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. DAC Weizhi Feng, Yicheng Liu, Jiaxiang Liu, David N. Jansen, Lijun Zhang, Zhilin Wu
2024	—	`conf`	One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics. EXPRESS/SOS Benjamin Bisping, David N. Jansen
2023	J	`jnl`	Angle of attack prediction using recurrent neural networks in flight conditions with faulty sensors in the case of F-16 fighter jet. Complex Intell. Syst. Mersha Bemnet Wondimagegnehu, David N. Jansen, Hongbin Ma
2023	J	`jnl`	Linear-Time-Branching-Time Spectroscopy Accounting for Silent Steps. CoRR Benjamin Bisping, David N. Jansen
2023	J	`jnl`	Rooted Divergence-Preserving Branching Bisimilarity is a Congruence for Guarded CCS. Formal Aspects Comput. Quan Sun, David N. Jansen, Xinxin Liu, Wei Zhang
2022	B	`conf`	CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). SEFM Shizhen Yu, Yifan Dong, Jiuyang Liu, Yong Li, Zhilin Wu, David N. Jansen, Lijun Zhang
2022	J	`jnl`	Deciding All Behavioral Equivalences at Once: A Game for Linear-Time-Branching-Time Spectroscopy. Log. Methods Comput. Sci. Benjamin Bisping, David N. Jansen, Uwe Nestmann
2022	—	`conf`	Rooted Divergence-Preserving Branching Bisimilarity is a Congruence: A Simpler Proof. A Journey from Process Algebra via Timed Automata to Model Learning David N. Jansen, Xinxin Liu
2021	B	`conf`	Formal Verification of Consensus in the Taurus Distributed Database. FM Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang
2021	—	`conf`	Frontmatter: mining Android user interfaces at scale. ESEC/SIGSOFT FSE Konstantin Kuznetsov, Chen Fu, Song Gao, David N. Jansen, Lijun Zhang, Andreas Zeller
2021	J	`jnl`	What do all these Buttons do? Statically Mining Android User Interfaces at Scale. CoRR Konstantin Kuznetsov, Chen Fu, Song Gao, David N. Jansen, Lijun Zhang, Andreas Zeller
2020	B	`conf`	A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. CONCUR David N. Jansen, Jan Friso Groote, Ferry Timmers, Pengfei Yang
2020	C	`conf`	Accelerated Verification of Parametric Protocols with Decision Trees. ICCD Yongjian Li, Taifeng Cao, David N. Jansen, Jun Pang, Xiaotao Wei
2020	—	`conf`	An O(m log n) algorithm for branching bisimilarity on labelled transition systems. TACAS (2) David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs
2020	—	`ed.`	Quantitative Evaluation of Systems - 17th International Conference, QEST 2020, Vienna, Austria, August 31 - September 3, 2020, Proceedings QEST Marco Gribaudo, David N. Jansen, Anne Remke
2019	J	`jnl`	A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems. CoRR David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs
2019	C	`conf`	An Axiomatisation of the Probabilistic \mu -Calculus. ICFEM Junnan Xu, Wanwei Liu, David N. Jansen, Lijun Zhang
2018	J	`jnl`	An Automatic Proving Approach to Parameterized Verification. ACM Trans. Comput. Log. Yongjian Li, Kaiqiang Duan, David N. Jansen, Jun Pang, Lijun Zhang, Yi Lv, Shaowei Cai
2018	—	`ed.`	Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Beijing, China, September 4-6, 2018, Proceedings FORMATS David N. Jansen, Pavithra Prabhakar
2018	J	`jnl`	Probabilistic bisimulation for realistic schedulers. Acta Informatica Lijun Zhang, Pengfei Yang, Lei Song, Holger Hermanns, Christian Eisentraut, David N. Jansen, Jens Chr. Godskesen
2017	J	`jnl`	An ACM Trans. Comput. Log. Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, Anton Wijs
2017	—	`conf`	Distribution-Based Bisimulation for Labelled Markov Processes. FORMATS Pengfei Yang, David N. Jansen, Lijun Zhang
2017	J	`jnl`	Distribution-based bisimulation for labelled Markov processes. CoRR Pengfei Yang, David N. Jansen, Lijun Zhang
2017	B	`conf`	Finding Polynomial Loop Invariants for Probabilistic Programs. ATVA Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
2017	J	`jnl`	Finding polynomial loop invariants for probabilistic programs. CoRR Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
2017	Misc	`conf`	On Equivalence Checking of Nondeterministic Finite Automata. SETTA Chen Fu, Yuxin Deng, David N. Jansen, Lijun Zhang
2016	J	`jnl`	A space-efficient simulation algorithm on probabilistic automata. Inf. Comput. Lijun Zhang, David N. Jansen
2016	C	`conf`	Minimal Separating Sequences for All Pairs of States. LATA Rick Smetsers, Joshua Moerman, David N. Jansen
2016	J	`jnl`	Multiphase until formulas over Markov reward models: An algebraic approach. Theor. Comput. Sci. Ming Xu, Lijun Zhang, David N. Jansen, Huibiao Zhu, Zongyuan Yang
2016	J	`jnl`	Stuttering equivalence is too slow! CoRR David N. Jansen, Jeroen J. A. Keiren
2015	Misc	`conf`	A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. SETTA Tom van Dijk, Ernst Moritz Hahn, David N. Jansen, Yong Li, Thomas Neele, Mariëlle Stoelinga, Andrea Turrini, Lijun Zhang
2015	C	`conf`	Applying Automata Learning to Embedded Control Software. ICFEM Wouter Smeenk, Joshua Moerman, Frits W. Vaandrager, David N. Jansen
2013	—	`conf`	More or Less True DCTL for Continuous-Time MDPs. FORMATS David N. Jansen
2013	—	`conf`	Revisiting Weak Simulation for Substochastic Markov Chains. QEST David N. Jansen, Lei Song, Lijun Zhang
2012	—	`conf`	Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm. NASA Formal Methods David N. Jansen, Flemming Nielson, Lijun Zhang
2012	—	`conf`	On Abstraction of Probabilistic Systems. ROCKS Christian Dehnert, Daniel Gebler, Michele Volpato, David N. Jansen
2011	J	`jnl`	Automata-Based CSL Model Checking Log. Methods Comput. Sci. Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns
2011	—	`conf`	Automata-Based CSL Model Checking. ICALP (2) Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns
2011	J	`jnl`	Erratum to: Model-checking continuous-time Markov chains by Aziz et al CoRR David N. Jansen
2011	J	`jnl`	The ins and outs of the probabilistic model checker MRMC. Perform. Evaluation Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen
2010	—	`conf`	Fortuna: Model Checking Priced Probabilistic Timed Automata. QEST Jasper Berendsen, David N. Jansen, Frits W. Vaandrager
2010	J	`jnl`	Synthesis and stochastic assessment of cost-optimal schedules. Int. J. Softw. Tools Technol. Transf. Angelika Mader, Henrik C. Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann L. Hurink, Holger Hermanns
2010	J	`jnl`	The axiomatization of override and update. J. Appl. Log. Jasper Berendsen, David N. Jansen, Julien Schmaltz, Frits W. Vaandrager
2009	—	`conf`	The Ins and Outs of the Probabilistic Model Checker MRMC. QEST Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen
2009	C	`conf`	Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata. TAMC Jasper Berendsen, Taolue Chen, David N. Jansen
2008	J	`jnl`	Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations CoRR Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen
2008	J	`jnl`	Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. Log. Methods Comput. Sci. Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen
2007	—	`conf`	07101 Working Group Report -- Performance Measures Other Than Time. Quantitative Aspects of Embedded Systems Lucia Cloth, Pepijn Crouzen, Matthias Fruth, Tingting Han, David N. Jansen, Mark Kattenbelt, Gerard J. M. Smit, Lijun Zhang
2007	A	`conf`	Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. TACAS Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen
2007	A	`conf`	Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. TACAS Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen
2007	—	`conf`	How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. Haifa Verification Conference David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Mariëlle Stoelinga, Ivan S. Zapreev
2006	—	`conf`	Probably on Time and within Budget: On Reachability in Priced Probabilistic Timed Automata. QEST Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen
2005	—	`conf`	From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. WOSP Holger Hermanns, David N. Jansen, Yaroslav S. Usenko
2005	C	`conf`	Logic and Model Checking for Hidden Markov Models. FORTE Lijun Zhang, Holger Hermanns, David N. Jansen
2005	J	`jnl`	QoS modelling and analysis with UML-statecharts: the StoCharts approach. SIGMETRICS Perform. Evaluation Rev. David N. Jansen, Holger Hermanns
2004	—	`conf`	An industrial-strength formal method -- A Modest survey. ISoLA (Preliminary proceedings) Henrik C. Bohnenkamp, Holger Hermanns, David N. Jansen, Joost-Pieter Katoen, Yaroslav S. Usenko
2004	—	`conf`	Dependability Checking with StoCharts: Is Train Radio Reliable Enough for Trains? QEST David N. Jansen, Holger Hermanns
2003	—	`conf`	A QoS-Oriented Extension of UML Statecharts. UML David N. Jansen, Holger Hermanns, Joost-Pieter Katoen
2003	—	`—`	Extensions of Statecharts with probability, time, and stochastic timing. David N. Jansen
2002	—	`conf`	A Probabilistic Extension of UML Statecharts. FTRTFT David N. Jansen, Holger Hermanns, Joost-Pieter Katoen
2002	J	`jnl`	Extending CTL with Actions and Real Time. J. Log. Comput. David N. Jansen, Roel J. Wieringa
2002	J	`jnl`	Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts. Requir. Eng. Rik Eshuis, David N. Jansen, Roel J. Wieringa
2001	A	`conf`	Techniques for Reactive System Design: The Tools in TRADE. CAiSE Roel J. Wieringa, David N. Jansen