Lijun Zhang

Affiliations:
  • Chinese Academy of Sciences, School of Software, Beijing, China
  • Technical University of Denmark (former)
  • Saarland University, Saarbrücken, Germany (former)


According to our database1, Lijun Zhang authored at least 140 papers between 2005 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Model Checking for Probabilistic Multiagent Systems.
J. Comput. Sci. Technol., September, 2023

On the power of finite ambiguity in Büchi complementation.
Inf. Comput., June, 2023

Model checking differentially private properties.
Theor. Comput. Sci., 2023

Quantitative controller synthesis for consumption Markov decision processes.
Inf. Process. Lett., 2023

Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets.
CoRR, 2023

Model Predictive Control with Reach-avoid Analysis.
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023

Scenario Approach for Parametric Markov Models.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition".
Dataset, May, 2022

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition".
Dataset, May, 2022

Probabilistic Preference Planning Problem for Markov Decision Processes.
IEEE Trans. Software Eng., 2022

Weight Expansion: A New Perspective on Dropout and Generalization.
Trans. Mach. Learn. Res., 2022

Synthesizing ranking functions for loop programs via SVM.
Theor. Comput. Sci., 2022

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019.
Int. J. Softw. Tools Technol. Transf., 2022

Safety Analysis of Autonomous Driving Systems Based on Model Learning.
CoRR, 2022

Defensive Design of Saturating Counters Based on Differential Privacy.
CoRR, 2022

Verifying Pufferfish Privacy in Hidden Markov Models.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

EPMC Gets Knowledge in Multi-agent Systems.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper).
Proceedings of the Software Engineering and Formal Methods - 20th International Conference, 2022

Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning.
Proceedings of the 44th IEEE/ACM 44th International Conference on Software Engineering, 2022

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021
Editorial - Special issue on Concurrency Theory (CONCUR 2018).
J. Comput. Syst. Sci., 2021

A novel learning algorithm for Büchi automata based on family of DFAs and classification trees.
Inf. Comput., 2021

Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation.
Formal Aspects Comput., 2021

Ensemble Defense with Data Diversity: Weak Correlation Implies Strong Robustness.
CoRR, 2021

What do all these Buttons do? Statically Mining Android User Interfaces at Scale.
CoRR, 2021

Probabilistic Robustness Analysis for DNNs based on PAC Learning.
CoRR, 2021

Improving Neural Network Verification through Spurious Region Guided Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Frontmatter: mining Android user interfaces at scale.
Proceedings of the ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2021

Synthesizing Good-Enough Strategies for LTLf Specifications.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Congruence Relations for Büchi Automata.
Proceedings of the Formal Methods - 24th International Symposium, 2021

Formal Verification of Consensus in the Taurus Distributed Database.
Proceedings of the Formal Methods - 24th International Symposium, 2021

2020
On the Power of Unambiguity in Büchi Complementation.
Proceedings of the Proceedings 11th International Symposium on Games, 2020

SVMRanker: a general termination analysis framework of loop programs via SVM.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

PRODeep: a platform for robustness verification of deep neural networks.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

How does Weight Correlation Affect Generalisation Ability of Deep Neural Networks?
Proceedings of the Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, 2020

Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
SAT-based explicit LTL reasoning and its application to satisfiability checking.
Formal Methods Syst. Des., 2019

Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification.
Proceedings of the Static Analysis - 26th International Symposium, 2019

An Axiomatisation of the Probabilistic \mu -Calculus.
Proceedings of the Formal Methods and Software Engineering, 2019

Synthesizing Nested Ranking Functions for Loop Programs via SVM.
Proceedings of the Formal Methods and Software Engineering, 2019

2018
An Automatic Proving Approach to Parameterized Verification.
ACM Trans. Comput. Log., 2018

Accelerating LTL satisfiability checking by SAT solvers.
J. Log. Comput., 2018

The quest for minimal quotients for probabilistic and Markov automata.
Inf. Comput., 2018

An explicit transition system construction approach to LTL satisfiability checking.
Formal Aspects Comput., 2018

Probabilistic bisimulation for realistic schedulers.
Acta Informatica, 2018

Preface for the special issue for ATVA 2015.
Acta Informatica, 2018

Learning to Complement Büchi Automata.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Learning Büchi Automata and Its Applications.
Proceedings of the Engineering Trustworthy Software Systems - 4th International School, 2018

Advanced automata-based algorithms for program termination checking.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems.
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Model Checking Differentially Private Properties.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017
Precisely deciding CSL formulas through approximate model checking for CTMCs.
J. Comput. Syst. Sci., 2017

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems.
Formal Aspects Comput., 2017

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties.
CoRR, 2017

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

On Equivalence Checking of Nondeterministic Finite Automata.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2017

Distribution-Based Bisimulation for Labelled Markov Processes.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2017

Finding Polynomial Loop Invariants for Probabilistic Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes.
ACM Trans. Softw. Eng. Methodol., 2016

Multiphase until formulas over Markov reward models: An algebraic approach.
Theor. Comput. Sci., 2016

A space-efficient simulation algorithm on probabilistic automata.
Inf. Comput., 2016

Efficient approximation of optimal control for continuous-time Markov games.
Inf. Comput., 2016

Verify LTL with Fairness Assumptions Efficiently.
Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, 2016

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs.
Proceedings of the ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands, 2016

A Simple Algorithm for Solving Qualitative Probabilistic Parity Games.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
A nearly optimal upper bound for the self-stabilization time in Herman's algorithm.
Distributed Comput., 2015

Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata.
CoRR, 2015

Extending Hybrid CSP with Probability and Stochasticity.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Planning for Stochastic Games with Co-Safe Objectives.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

A Simple Probabilistic Extension of Modal Mu-calculus.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

QPMC: A Model Checker for Quantum Programs and Protocols.
Proceedings of the FM 2015: Formal Methods, 2015

Probabilistic Bisimulation for Realistic Schedulers.
Proceedings of the FM 2015: Formal Methods, 2015

Lazy Probabilistic Model Checking without Determinisation.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Decentralized Bisimulation for Multiagent Systems.
Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, 2015

Preference Planning for Markov Decision Processes.
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014
Incremental Bisimulation Abstraction Refinement.
ACM Trans. Embed. Comput. Syst., 2014

Model Checking CSL for Markov Population Models
Proceedings of the Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, 2014

Fast LTL Satisfiability Checking by SAT Solvers.
CoRR, 2014

Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Aalta: an LTL satisfiability checker over Infinite/Finite traces.
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16, 2014

iscasMc: A Web-Based Probabilistic Model Checker.
Proceedings of the FM 2014: Formal Methods, 2014

When Equivalence and Bisimulation Join Forces in Probabilistic Automata.
Proceedings of the FM 2014: Formal Methods, 2014

LTLf Satisfiability Checking.
Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Probably safe or live.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013
Model checking conditional CSL for continuous-time Markov chains.
Inf. Process. Lett., 2013

A tighter bound for the self-stabilization time in Herman's algorithm.
Inf. Process. Lett., 2013

Bisimulations Meet PCTL Equivalences for Probabilistic Automata
Log. Methods Comput. Sci., 2013

Polsat: A Portfolio LTL Satisfiability Solver.
CoRR, 2013

Lazy Determinisation for Quantitative Model Checking.
CoRR, 2013

LTL Satisfiability Checking Revisited.
Proceedings of the 2013 20th International Symposium on Temporal Representation and Reasoning, 2013

Model Repair for Markov Decision Processes.
Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

The Quest for Minimal Quotients for Probabilistic Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Revisiting Weak Simulation for Substochastic Markov Chains.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Deciding Bisimilarities on Distributions.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

On the Relationship between LTL Normal Forms and Büchi Automata.
Proceedings of the Theories of Programming and Formal Methods, 2013

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains.
Proceedings of the Automated Technology for Verification and Analysis, 2013

A Semantics for Every GSPN.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2013

2012
Safety Verification for Probabilistic Hybrid Systems.
Eur. J. Control, 2012

Roadmap Document on Stochastic Analysis
CoRR, 2012

On the Relationship between LTL Normal Forms and Buechi Automata
CoRR, 2012

The Branching Time Spectrum for Continuous-time MDPs
CoRR, 2012

Late Weak Bisimulation for Markov Automata
CoRR, 2012

A General Framework for Probabilistic Characterizing Formulae.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm.
Proceedings of the NASA Formal Methods, 2012

2011
From Concurrency Models to Numbers - Performance and Dependability.
Proceedings of the Software and Systems Safety - Specification and Verification, 2011

Probabilistic reachability for parametric Markov models.
Int. J. Softw. Tools Technol. Transf., 2011

Probabilistic Logical Characterization.
Inf. Comput., 2011

Automata-Based CSL Model Checking
Log. Methods Comput. Sci., 2011

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

Synthesis for PCTL in Parametric Markov Decision Processes.
Proceedings of the NASA Formal Methods, 2011

On Stabilization in Herman's Algorithm.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

Measurability and safety verification for stochastic hybrid systems.
Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Model Checking Algorithms for CTMDPs.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Efficient Approximation of Optimal Control for Markov Games
CoRR, 2010

Best Probabilistic Transformers.
Proceedings of the Verification, 2010

Model Checking Interactive Markov Chains.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

PASS: Abstraction Refinement for Infinite Probabilistic Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains.
Proceedings of the Model Checking Software, 2010

Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes.
Proceedings of the QEST 2010, 2010

On Probabilistic Automata in Continuous Time.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

Concurrency and Composition in a Stochastic World.
Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

PARAM: A Model Checker for Parametric Markov Models.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Decision algorithms for probabilistic simulations.
PhD thesis, 2009

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains.
Fundam. Informaticae, 2009

FlowSim Simulation Benchmarking Platform.
Proceedings of the QEST 2009, 2009

INFAMY: An Infinite-State Markov Model Checker.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations.
Log. Methods Comput. Sci., 2008

An Experimental Evaluation of Probabilistic Simulation.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

A Space-Efficient Probabilistic Simulation Algorithm.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

On the Minimisation of Acyclic Models.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Probabilistic CEGAR.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Probabilistic Model Checking Modulo Theories.
Proceedings of the Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 2007

07101 Working Group Report -- Performance Measures Other Than Time.
Proceedings of the Quantitative Aspects of Embedded Systems, 04.03. - 09.03.2007, 2007

Deciding Simulations on Probabilistic Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2005
Logic and Model Checking for Hidden Markov Models.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

Hardware Reliability.
Proceedings of the Dependability Metrics: Advanced Lectures [result from a Dagstuhl seminar, October 30, 2005


  Loading...