Hardware Reliability. - Irene Eusgeld; Bernhard Fechner; Felix Salfner; Max Walter; Philipp Limbourg; Lijun Zhang 001 (Dependability Metrics, 2005)

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

Deciding Simulations on Probabilistic Automata. - Lijun Zhang 001; Holger Hermanns (ATVA, 2007)

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)

Probabilistic Model Checking Modulo Theories. - Björn Wachter; Lijun Zhang 001; Holger Hermanns (QEST, 2007)

Probabilistic CEGAR. - Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2008)

On the Minimisation of Acyclic Models. - Pepijn Crouzen; Holger Hermanns; Lijun Zhang 001 (CONCUR, 2008)

A Space-Efficient Probabilistic Simulation Algorithm. - Lijun Zhang 001 (CONCUR, 2008)

An Experimental Evaluation of Probabilistic Simulation. - Jonathan Bogdoll; Holger Hermanns; Lijun Zhang 001 (FORTE, 2008)

Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. - Lijun Zhang 001; Holger Hermanns; Friedrich Eisenbrand; David N. Jansen (Log. Methods Comput. Sci., 2008)

INFAMY: An Infinite-State Markov Model Checker. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2009)

FlowSim Simulation Benchmarking Platform. - Jonathan Bogdoll; Holger Hermanns; Lijun Zhang 001 (QEST, 2009)

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (Fundam. Informaticae, 2009)

Decision algorithms for probabilistic simulations. - Lijun Zhang 001 (2009)

PARAM: A Model Checker for Parametric Markov Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2010)

Concurrency and Composition in a Stochastic World. - Christian Eisentraut; Holger Hermanns; Lijun Zhang 001 (CONCUR, 2010)

On Probabilistic Automata in Continuous Time. - Christian Eisentraut; Holger Hermanns; Lijun Zhang 001 (LICS, 2010)

Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes. - Martin R. Neuhäußer; Lijun Zhang 001 (QEST, 2010)

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. - Georgel Calin; Pepijn Crouzen; Pedro R. D'Argenio; Ernst Moritz Hahn; Lijun Zhang 001 (SPIN, 2010)

PASS: Abstraction Refinement for Infinite Probabilistic Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (TACAS, 2010)

Model Checking Interactive Markov Chains. - Lijun Zhang 001; Martin R. Neuhäußer (TACAS, 2010)

Best Probabilistic Transformers. - Björn Wachter; Lijun Zhang 001 (VMCAI, 2010)

Efficient Approximation of Optimal Control for Markov Games - Markus N. Rabe; Sven Schewe; Lijun Zhang 001 (CoRR, 2010)

Model Checking Algorithms for CTMDPs. - Peter Buchholz 001; Ernst Moritz Hahn; Holger Hermanns; Lijun Zhang 001 (CAV, 2011)

Measurability and safety verification for stochastic hybrid systems. - Martin Fränzle; Ernst Moritz Hahn; Holger Hermanns; Nicolás Wolovick; Lijun Zhang 001 (HSCC, 2011)

On Stabilization in Herman's Algorithm. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; James Worrell 001; Lijun Zhang 001 (ICALP (2), 2011)

Synthesis for PCTL in Parametric Markov Decision Processes. - Ernst Moritz Hahn; Tingting Han 001; Lijun Zhang 001 (NASA Formal Methods, 2011)

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. - Ernst Moritz Hahn; Gethin Norman; David Parker 001; Björn Wachter; Lijun Zhang 001 (QEST, 2011)

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

Probabilistic Logical Characterization. - Holger Hermanns; Augusto Parma; Roberto Segala; Björn Wachter; Lijun Zhang 001 (Inf. Comput., 2011)

Probabilistic reachability for parametric Markov models. - Ernst Moritz Hahn; Holger Hermanns; Lijun Zhang 001 (Int. J. Softw. Tools Technol. Transf., 2011)

From Concurrency Models to Numbers - Performance and Dependability. - Holger Hermanns; Lijun Zhang 001 (Software and Systems Safety - Specification and Verification, 2011)

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

A General Framework for Probabilistic Characterizing Formulae. - Joshua Sack; Lijun Zhang 001 (VMCAI, 2012)

Late Weak Bisimulation for Markov Automata - Lei Song 001; Lijun Zhang 001; Jens Chr. Godskesen (CoRR, 2012)

The Branching Time Spectrum for Continuous-time MDPs - Lei Song 001; Lijun Zhang 001; Jens Chr. Godskesen (CoRR, 2012)

On the Relationship between LTL Normal Forms and Buechi Automata - Jianwen Li; Geguang Pu; Lijun Zhang 001; Zheng Wang 005; Jifeng He 001; Kim G. Larsen (CoRR, 2012)

Roadmap Document on Stochastic Analysis - Bo Friis Nielsen; Flemming Nielson; Henrik Pilegaard; Michael James Andrew Smith; Ender Yüksel; Kebin Zeng; Lijun Zhang 001 (CoRR, 2012)

Safety Verification for Probabilistic Hybrid Systems. - Lijun Zhang 001; Zhikun She; Stefan Ratschan; Holger Hermanns; Ernst Moritz Hahn (Eur. J. Control, 2012)

A Semantics for Every GSPN. - Christian Eisentraut; Holger Hermanns; Joost-Pieter Katoen; Lijun Zhang 001 (Petri Nets, 2013)

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. - Yang Gao; Ernst Moritz Hahn; Naijun Zhan; Lijun Zhang 001 (ATVA, 2013)

On the Relationship between LTL Normal Forms and Büchi Automata. - Jianwen Li; Geguang Pu; Lijun Zhang 001; Zheng Wang 005; Jifeng He 001; Kim Guldstrand Larsen (Theories of Programming and Formal Methods, 2013)

Deciding Bisimilarities on Distributions. - Christian Eisentraut; Holger Hermanns; Julia Krämer; Andrea Turrini; Lijun Zhang 001 (QEST, 2013)

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

The Quest for Minimal Quotients for Probabilistic Automata. - Christian Eisentraut; Holger Hermanns; Johann Schuster; Andrea Turrini; Lijun Zhang 001 (TACAS, 2013)

Model Repair for Markov Decision Processes. - Taolue Chen 001; Ernst Moritz Hahn; Tingting Han 001; Marta Z. Kwiatkowska; Hongyang Qu 001; Lijun Zhang 001 (TASE, 2013)

LTL Satisfiability Checking Revisited. - Jianwen Li; Lijun Zhang 001; Geguang Pu; Moshe Y. Vardi; Jifeng He 001 (TIME, 2013)

Lazy Determinisation for Quantitative Model Checking. - Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Lijun Zhang 001 (CoRR, 2013)

Polsat: A Portfolio LTL Satisfiability Solver. - Jianwen Li; Geguang Pu; Lijun Zhang 001; Yinbo Yao; Moshe Y. Vardi; Jifeng He 001 (CoRR, 2013)

Bisimulations Meet PCTL Equivalences for Probabilistic Automata - Lei Song 001; Lijun Zhang 001; Jens Chr. Godskesen (Log. Methods Comput. Sci., 2013)

A tighter bound for the self-stabilization time in Herman's algorithm. - Yuan Feng 001; Lijun Zhang 001 (Inf. Process. Lett., 2013)

Model checking conditional CSL for continuous-time Markov chains. - Yang Gao; Ming Xu 010; Naijun Zhan; Lijun Zhang 001 (Inf. Process. Lett., 2013)

Probably safe or live. - Joost-Pieter Katoen; Lei Song 001; Lijun Zhang 001 (CSL-LICS, 2014)

LTLf Satisfiability Checking. - Jianwen Li; Lijun Zhang 001; Geguang Pu; Moshe Y. Vardi; Jifeng He 001 (ECAI, 2014)

When Equivalence and Bisimulation Join Forces in Probabilistic Automata. - Yuan Feng 001; Lijun Zhang 001 (FM, 2014)

iscasMc: A Web-Based Probabilistic Model Checker. - Ernst Moritz Hahn; Yi Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (FM, 2014)

Aalta: an LTL satisfiability checker over Infinite/Finite traces. - Jianwen Li; Yinbo Yao; Geguang Pu; Lijun Zhang 001; Jifeng He 001 (SIGSOFT FSE, 2014)

Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes. - Lei Song 001; Lijun Zhang 001; Jens Chr. Godskesen (VMCAI, 2014)

Fast LTL Satisfiability Checking by SAT Solvers. - Jianwen Li; Geguang Pu; Lijun Zhang 001; Moshe Y. Vardi; Jifeng He 001 (CoRR, 2014)

Model Checking CSL for Markov Population Models - David Spieler; Ernst Moritz Hahn; Lijun Zhang 001 (QAPL, 2014)

Incremental Bisimulation Abstraction Refinement. - Lei Song 001; Lijun Zhang 001; Holger Hermanns; Jens Chr. Godskesen (ACM Trans. Embed. Comput. Syst., 2014)

Preference Planning for Markov Decision Processes. - Meilun Li; Zhikun She; Andrea Turrini; Lijun Zhang 001 (AAAI, 2015)

Decentralized Bisimulation for Multiagent Systems. - Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (AAMAS, 2015)

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. - Yu-Fang Chen 001; Chih-Duo Hong; Bow-Yaw Wang; Lijun Zhang 001 (CAV (1), 2015)

Lazy Probabilistic Model Checking without Determinisation. - Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CONCUR, 2015)

Probabilistic Bisimulation for Realistic Schedulers. - Christian Eisentraut; Jens Chr. Godskesen; Holger Hermanns; Lei Song 001; Lijun Zhang 001 (FM, 2015)

QPMC: A Model Checker for Quantum Programs and Protocols. - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Lijun Zhang 001 (FM, 2015)

A Simple Probabilistic Extension of Modal Mu-calculus. - Wanwei Liu; Lei Song 001; Ji Wang 001; Lijun Zhang 001 (IJCAI, 2015)

Planning for Stochastic Games with Co-Safe Objectives. - Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (IJCAI, 2015)

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. - Fei He 001; Xiaowei Gao; Bow-Yaw Wang; Lijun Zhang 001 (POPL, 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)

Extending Hybrid CSP with Probability and Stochasticity. - Yu Peng; Shuling Wang 003; Naijun Zhan; Lijun Zhang 001 (SETTA, 2015)

Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata. - Yuan Feng 001; Lei Song 001; Lijun Zhang 001 (CoRR, 2015)

A nearly optimal upper bound for the self-stabilization time in Herman's algorithm. - Yuan Feng 001; Lijun Zhang 001 (Distributed Comput., 2015)

A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CAV (2), 2016)

GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs. - Zhimin Wu; Ernst Moritz Hahn; Akin Günay; Lijun Zhang 001; Yang Liu 003 (ECAI, 2016)

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. - Yong Li 031; Wanwei Liu; Andrea Turrini; Ernst Moritz Hahn; Lijun Zhang 001 (SETTA, 2016)

Verify LTL with Fairness Assumptions Efficiently. - Yong Li 031; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (TIME, 2016)

Efficient approximation of optimal control for continuous-time Markov games. - John Fearnley; Markus N. Rabe; Sven Schewe; Lijun Zhang 001 (Inf. Comput., 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)

Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. - Fei He 001; Xiaowei Gao; Miaofei Wang; Bow-Yaw Wang; Lijun Zhang 001 (ACM Trans. Softw. Eng. Methodol., 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)

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2017)

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties. - Hongfei Fu 001; Yi Li; Jianlin Li; Lijun Zhang 001 (CoRR, 2017)

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. - Shuling Wang 003; Naijun Zhan; Lijun Zhang 001 (Formal Aspects Comput., 2017)

Precisely deciding CSL formulas through approximate model checking for CTMCs. - Yuan Feng 001; Lijun Zhang 001 (J. Comput. Syst. Sci., 2017)

Model Checking Differentially Private Properties. - Depeng Liu; Bow-Yaw Wang; Lijun Zhang 001 (APLAS, 2018)

Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (IJCAI, 2018)

Advanced automata-based algorithms for program termination checking. - Yu-Fang Chen 001; Matthias Heizmann; Ondrej Lengál; Yong Li 031; Ming-Hsien Tsai 001; Andrea Turrini; Lijun Zhang 001 (PLDI, 2018)

Learning Büchi Automata and Its Applications. - Yong Li 031; Andrea Turrini; Yu-Fang Chen 001; Lijun Zhang 001 (SETSS, 2018)

Learning to Complement Büchi Automata. - Yong Li 031; Andrea Turrini; Lijun Zhang 001; Sven Schewe (VMCAI, 2018)

Preface for the special issue for ATVA 2015. - Bernd Finkbeiner; Geguang Pu; Lijun Zhang 001 (Acta Informatica, 2018)

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 explicit transition system construction approach to LTL satisfiability checking. - Jianwen Li; Lijun Zhang 001; Shufang Zhu 001; Geguang Pu; Moshe Y. Vardi; Jifeng He 001 (Formal Aspects Comput., 2018)

The quest for minimal quotients for probabilistic and Markov automata. - Christian Eisentraut; Holger Hermanns; Johann Schuster; Andrea Turrini; Lijun Zhang 001 (Inf. Comput., 2018)

Accelerating LTL satisfiability checking by SAT solvers. - Jianwen Li; Geguang Pu; Lijun Zhang 001; Moshe Y. Vardi; Jifeng He 001 (J. Log. Comput., 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)

Synthesizing Nested Ranking Functions for Loop Programs via SVM. - Yi Li; Xuechao Sun; Yong Li 031; Andrea Turrini; Lijun Zhang 001 (ICFEM, 2019)

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

Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. - Jianlin Li; Jiangchao Liu; Pengfei Yang 002; Liqian Chen; Xiaowei Huang 001; Lijun Zhang 001 (SAS, 2019)

SAT-based explicit LTL reasoning and its application to satisfiability checking. - Jianwen Li; Shufang Zhu 001; Geguang Pu; Lijun Zhang 001; Moshe Y. Vardi (Formal Methods Syst. Des., 2019)

Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. - Yong Li 031; Andrea Turrini; Xuechao Sun; Lijun Zhang 001 (ATVA, 2020)

How does Weight Correlation Affect Generalisation Ability of Deep Neural Networks? - Gaojie Jin; Xinping Yi; Liang Zhang; Lijun Zhang 001; Sven Schewe; Xiaowei Huang 001 (NeurIPS, 2020)

PRODeep: a platform for robustness verification of deep neural networks. - Renjue Li; Jianlin Li; Cheng-Chao Huang; Pengfei Yang 002; Xiaowei Huang 001; Lijun Zhang 001; Bai Xue 001; Holger Hermanns (ESEC/SIGSOFT FSE, 2020)

SVMRanker: a general termination analysis framework of loop programs via SVM. - Xie Li; Yi Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (ESEC/SIGSOFT FSE, 2020)

On the Power of Unambiguity in Büchi Complementation. - Yong Li 031; Moshe Y. Vardi; Lijun Zhang 001 (GandALF, 2020)

Preface. - Tao Xie 001; Zhi Jin; Xuandong Li; Gang Huang 001; Hausi A. Müller; Jun Pang 001; Lijun Zhang 001 (J. Comput. Sci. Technol., 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)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (FM, 2021)

Probabilistic Verification of Neural Networks Against Group Fairness. - Bing Sun; Jun Sun 001; Ting Dai; Lijun Zhang 001 (FM, 2021)

Synthesizing Good-Enough Strategies for LTLf Specifications. - Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (IJCAI, 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)

Improving Neural Network Verification through Spurious Region Guided Refinement. - Pengfei Yang 002; Renjue Li; Jianlin Li; Cheng-Chao Huang; Jingyi Wang 004; Jun Sun 001; Bai Xue 001; Lijun Zhang 001 (TACAS (1), 2021)

Probabilistic Robustness Analysis for DNNs based on PAC Learning. - Renjue Li; Pengfei Yang 002; Cheng-Chao Huang; Bai Xue 001; Lijun Zhang 001 (CoRR, 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)

Ensemble Defense with Data Diversity: Weak Correlation Implies Strong Robustness. - Renjue Li; Hanwei Zhang 001; Pengfei Yang 002; Cheng-Chao Huang; Aimin Zhou; Bai Xue 001; Lijun Zhang 001 (CoRR, 2021)

Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation. - Pengfei Yang 002; Jianlin Li; Jiangchao Liu; Cheng-Chao Huang; Renjue Li; Liqian Chen; Xiaowei Huang 001; Lijun Zhang 001 (Formal Aspects Comput., 2021)

A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. - Yong Li 031; Yu-Fang Chen 001; Lijun Zhang 001; Depeng Liu (Inf. Comput., 2021)

Editorial - Special issue on Concurrency Theory (CONCUR 2018). - Sven Schewe; Lijun Zhang 001 (J. Comput. Syst. Sci., 2021)

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (CAV (2), 2022)

Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. - Renjue Li; Pengfei Yang 002; Cheng-Chao Huang; Youcheng Sun; Bai Xue 001; Lijun Zhang 001 (ICSE, 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)

EPMC Gets Knowledge in Multi-agent Systems. - Chen Fu; Ernst Moritz Hahn; Yong Li 031; Sven Schewe; Meng Sun 002; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2022)

Verifying Pufferfish Privacy in Hidden Markov Models. - Depeng Liu; Bow-Yaw Wang; Lijun Zhang 001 (VMCAI, 2022)

Defensive Design of Saturating Counters Based on Differential Privacy. - Depeng Liu; Lutan Zhao; Pengfei Yang 002; Bow-Yaw Wang; Rui Hou 001; Lijun Zhang 001; Naijun Zhan (CoRR, 2022)

Safety Analysis of Autonomous Driving Systems Based on Model Learning. - Renjue Li; Tianhang Qin; Pengfei Yang 002; Cheng-Chao Huang; Youcheng Sun; Lijun Zhang 001 (CoRR, 2022)

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019. - Tomás Vojnar; Lijun Zhang 001 (Int. J. Softw. Tools Technol. Transf., 2022)

Synthesizing ranking functions for loop programs via SVM. - Yi Li; Xie Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (Theor. Comput. Sci., 2022)

Weight Expansion: A New Perspective on Dropout and Generalization. - Gaojie Jin; Xinping Yi; Pengfei Yang 002; Lijun Zhang 001; Sven Schewe; Xiaowei Huang 001 (Trans. Mach. Learn. Res., 2022)

Probabilistic Preference Planning Problem for Markov Decision Processes. - Meilun Li; Andrea Turrini; Ernst Moritz Hahn; Zhikun She; Lijun Zhang 001 (IEEE Trans. Software Eng., 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Scenario Approach for Parametric Markov Models. - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (ATVA (1), 2023)

TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models. - Liang Zhang; Nathaniel Xu; Pengfei Yang 002; Gaojie Jin; Cheng-Chao Huang; Lijun Zhang 001 (ICCV, 2023)

Model Predictive Control with Reach-avoid Analysis. - Dejin Ren; Wanli Lu; Jidong Lv; Lijun Zhang 001; Bai Xue 001 (IJCAI, 2023)

Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks. - Pengfei Yang 002; Zhiming Chi; Zongxin Liu 001; Mengyu Zhao; Cheng-Chao Huang; Shaowei Cai 001; Lijun Zhang 001 (CoRR, 2023)

Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets. - Jianqiang Ding; Taoran Wu; Yuping Qian; Lijun Zhang 001; Bai Xue 001 (CoRR, 2023)

Quantitative controller synthesis for consumption Markov decision processes. - Jianling Fu; Cheng-Chao Huang; Yong Li 031; Jingyi Mei; Ming Xu 010; Lijun Zhang 001 (Inf. Process. Lett., 2023)

Model checking differentially private properties. - Depeng Liu; Bow-Yaw Wang; Chen Fu; Lijun Zhang 001 (Theor. Comput. Sci., 2023)

On the power of finite ambiguity in Büchi complementation. - Weizhi Feng; Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (Inf. Comput., 2023)

Artifact for the ATVA'23 paper "Scenario Approach for Parametric Markov Models". - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (Zenodo, 2023)

Model Checking for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (J. Comput. Sci. Technol., 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)

Verifying Randomized Consensus Protocols with Common Coins. - Song Gao 014; Bohua Zhan; Zhilin Wu; Lijun Zhang 001 (DSN, 2024)

Out-of-Bounding-Box Triggers: A Stealthy Approach to Cheat Object Detectors. - Tao Lin; Lijia Yu; Gaojie Jin; Renjue Li; Peng Wu; Lijun Zhang 001 (ECCV (66), 2024)

Class-Aware Cross Pseudo Supervision Framework for Semi-Supervised Multi-organ Segmentation in Abdominal CT Scans. - Deqian Yang; Haochen Zhao; Gaojie Jin; Hui Meng; Lijun Zhang 001 (PRCV (14), 2024)

Formal Verification of RISC-V Processor Chisel Designs. - Shidong Shen; Yicheng Liu; Lijun Zhang 001; Fu Song; Zhilin Wu (SETTA, 2024)

Eidos: Efficient, Imperceptible Adversarial 3D Point Clouds. - Hanwei Zhang 001; Luo Cheng; Qisong He; Wei Huang 035; Renjue Li; Ronan Sicre; Xiaowei Huang 001; Holger Hermanns; Lijun Zhang 001 (SETTA, 2024)

DeepCDCL: A CDCL-based Neural Network Verification Framework. - Zongxin Liu 001; Pengfei Yang 002; Lijun Zhang 001; Xiaowei Huang 001 (TASE, 2024)

HFE-Mamba: High-Frequency Enhanced Mamba Network for Efficient Segmentation of Left Ventricle in Pediatric Echocardiograms. - Zi Ye; Tianxiang Chen; Dan Wang; Fangyijie Wang; Lijun Zhang 001 (IEEE Access, 2024)

P-Mamba: Marrying Perona Malik Diffusion with Mamba for Efficient Pediatric Echocardiographic Left Ventricular Segmentation. - Zi Ye; Tianxiang Chen; Fangyijie Wang; Hanwei Zhang 001; Guanxi Li; Lijun Zhang 001 (CoRR, 2024)

DeepCDCL: An CDCL-based Neural Network Verification Framework. - Zongxin Liu 001; Pengfei Yang 002; Lijun Zhang 001; Xiaowei Huang 001 (CoRR, 2024)

ADVREPAIR: Provable Repair of Adversarial Attack. - Zhiming Chi; Jianan Ma; Pengfei Yang 002; Cheng-Chao Huang; Renjue Li; Xiaowei Huang 001; Lijun Zhang 001 (CoRR, 2024)

A Survey on Visual Mamba. - Hanwei Zhang 001; Ying Zhu; Dan Wang; Lijun Zhang 001; Tianxiang Chen; Zi Ye (CoRR, 2024)

Training Verification-Friendly Neural Networks via Neuron Behavior Consistency. - Zongxin Liu 001; Zhe Zhao 007; Fu Song; Jun Sun 001; Pengfei Yang 002; Xiaowei Huang 001; Lijun Zhang 001 (AAAI, 2025)

Towards Large Language Model Guided Kernel Direct Fuzzing. - Xie Li; Zhaoyue Yuan; Zhenduo Zhang; Youcheng Sun; Lijun Zhang 001 (FASE, 2025)

HFE-RWKV: High-Frequency Enhanced RWKV Model for Efficient Left Ventricle Segmentation in Pediatric Echocardiograms. - Zi Ye; Tianxiang Chen; Ziyang Wang; Hanwei Zhang 001; Lijun Zhang 001 (ICASSP, 2025)

Patch Synthesis for Property Repair of Deep Neural Networks. - Zhiming Chi; Jianan Ma; Pengfei Yang 002; Cheng-Chao Huang; Renjue Li; Jingyi Wang 004; Xiaowei Huang 001; Lijun Zhang 001 (ICSE, 2025)

Formal Methods in Industry. - Maurice H. ter Beek; Rod Chapman; Rance Cleaveland; Hubert Garavel; Rong Gu; Ivo ter Horst; Jeroen J. A. Keiren; Thierry Lecomte; Michael Leuschel; Kristin Yvonne Rozier; Augusto Sampaio 001; Cristina Seceleanu; et al. (Formal Aspects Comput., 2025)

QuantiVA: quantitative verification of autonomous driving. - Renjue Li; Tianhang Qin; Pengfei Yang 002; Cheng-Chao Huang; Youcheng Sun; Lijun Zhang 001 (Res. Dir. Cyber Phys. Syst., 2025)

Invariant Correlation of Representation With Label. - Gaojie Jin; Ronghui Mu; Xinping Yi; Xiaowei Huang 001; Lijun Zhang 001 (IEEE Trans. Inf. Forensics Secur., 2025)

Preference Alignment on Diffusion Model: A Comprehensive Survey for Image Generation and Editing. - Sihao Wu; Xiaonan Si; Chi Xing; Jianhong Wang; Gaojie Jin; Guangliang Cheng; Lijun Zhang 001; Xiaowei Huang 001 (CoRR, 2025)

Introduction to the Special Issue on Formal Methods and Models for System Design. - Jens Brandt 001; Indranil Saha; Lijun Zhang 001 (ACM Trans. Embed. Comput. Syst., 2025)

Revisiting Physically Realizable Adversarial Object Attack against LiDAR-based Detection: Clarifying Problem Formulation and Experimental Protocols. - Luo Cheng; Hanwei Zhang 001; Lijun Zhang 001; Holger Hermanns (CoRR, 2025)