Naijun Zhan

Affiliations:
  • Chinese Academy of Sciences, State Key Laboratory of Computer Science, Beijing, China


According to our database1, Naijun Zhan authored at least 120 papers between 1999 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2021
Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations.
IEEE Trans. Autom. Control., 2021

Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems.
SIAM J. Control. Optim., 2021

Special issue on design of embedded software and systems (SI: ICESS19).
J. Syst. Archit., 2021

Inferring Switched Nonlinear Dynamical Systems.
Formal Aspects Comput., 2021

Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control.
Acta Informatica, 2021

Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander.
Proceedings of the 27th IEEE Real-Time and Embedded Technology and Applications Symposium, 2021

Switching controller synthesis for delay hybrid systems under perturbations.
Proceedings of the HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, 2021

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Reach-avoid Analysis for Stochastic Discrete-time Systems.
Proceedings of the 2021 American Control Conference, 2021

2020
Automatically Generating SystemC Code from HCSP Formal Models.
ACM Trans. Softw. Eng. Methodol., 2020

Safety Verification for Random Ordinary Differential Equations.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020

Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties.
IEEE Trans. Autom. Control., 2020

From model to implementation: a network algorithm programming language.
Sci. China Inf. Sci., 2020

Learning One-Clock Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Probably Approximately Correct Interpolants Generation.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2020

PAC Learning of Deterministic One-Clock Timed Automata.
Proceedings of the Formal Methods and Software Engineering, 2020

Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems.
Proceedings of the 59th IEEE Conference on Decision and Control, 2020

Nonlinear Craig Interpolant Generation.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Unbounded-Time Safety Verification of Stochastic Differential Dynamics.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving.
Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

2019
Editorial.
Formal Aspects Comput., 2019

Synthesizing More Expressive Invariants by Semidefinite Programming.
CoRR, 2019

Nonlinear Craig Interpolant Generation.
CoRR, 2019

Quantum Hoare Logic.
Arch. Formal Proofs, 2019

Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow.
Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

Probably Approximate Safety Verification of Hybrid Dynamical Systems.
Proceedings of the Formal Methods and Software Engineering, 2019

Robust invariant sets generation for state-constrained perturbed polynomial systems.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving.
Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

NIL: Learning Nonlinear Interpolants.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
The Opacity of Real-Time Automata.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018

Reachability Analysis for Solvable Dynamical Systems.
IEEE Trans. Autom. Control., 2018

Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations.
CoRR, 2018

Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems.
CoRR, 2018

Parameter Synthesis Problems for one parametric clock Timed Automata.
CoRR, 2018

Robust Non-termination Analysis of Numerical Software.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018

Model Checking Bounded Continuous-time Extended Linear Duration Invariants.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

Under-Approximating Reach Sets for Polynomial Continuous Systems.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

Monitoring CTMCs by Multi-clock Timed Automata.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Decidability of the Initial-State Opacity of Real-Time Automata.
Proceedings of the Symposium on Real-Time and Hybrid Systems, 2018

What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction.
Proceedings of the Automated Technology for Verification and Analysis, 2018

ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.
Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

2017
Barrier certificates revisited.
J. Symb. Comput., 2017

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems.
J. Syst. Sci. Complex., 2017

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

Modelling and Verifying Communication Failure of Hybrid Systems in HCSP.
Comput. J., 2017

Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2017

Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations.
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

Synthesizing SystemC Code from Delay Hybrid CSP.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems.
Proceedings of the Provably Correct Systems, 2017

2016
A Theorem Prover for Quantum Hoare Logic and Its Applications.
CoRR, 2016

Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}.
CoRR, 2016

A Two-Way Path Between Formal and Informal Design of Embedded Systems.
Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

Approximate Bisimulation and Discretization of Hybrid CSP.
Proceedings of the FM 2016: Formal Methods, 2016

Validated Simulation-Based Verification of Delayed Differential Dynamics.
Proceedings of the FM 2016: Formal Methods, 2016

Computing reachable sets of linear vector fields revisited.
Proceedings of the 15th European Control Conference, 2016

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Termination Analysis of Polynomial Programs with Equality Conditions.
CoRR, 2015

Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL.
Sci. China Inf. Sci., 2015

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

An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems.
Proceedings of the Formal Methods and Software Engineering, 2015

Abstraction of Elementary Hybrid Systems by Variable Transformation.
Proceedings of the FM 2015: Formal Methods, 2015

Automatic Verification of Stability and Safety for Delay Differential Equations.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Formal Verification of Simulink/Stateflow Diagrams.
Proceedings of the Automated Technology for Verification and Analysis, 2015

Decidability of the Reachability for a Family of Linear Vector Fields.
Proceedings of the Automated Technology for Verification and Analysis, 2015

2014
Discovering non-terminating inputs for multi-path polynomial programs.
J. Syst. Sci. Complex., 2014

Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling.
Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

Combining Formal and Informal Methods in the Design of Spacecrafts.
Proceedings of the Engineering Trustworthy Software Systems - First International School, 2014

Formal Verification of a Descent Guidance Control Program of a Lunar Lander.
Proceedings of the FM 2014: Formal Methods, 2014

Adding Formal Meanings to AADL with Hybrid Annex.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

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

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation
CoRR, 2013

Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Modelling, Analysis and Verification of Hybrid Systems.
Proceedings of the Unifying Theories of Programming and Formal Engineering Methods, 2013

An Interface Model of Software Components.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

Bounded model-checking of discrete duration calculus.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Super-Dense Computation in Verification of Hybrid CSP Processes.
Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Towards a Failure Model of Software Components.
Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Verifying Simulink diagrams via a Hybrid Hoare Logic Prover.
Proceedings of the International Conference on Embedded Software, 2013

Generating Non-linear Interpolants by Semidefinite Programming.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants.
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

2012
Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems.
Math. Comput. Sci., 2012

An Assume/Guarantee Based Compositional Calculus for Hybrid CSP.
Proceedings of the Theory and Applications of Models of Computation, 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example.
Proceedings of the FM 2012: Formal Methods, 2012

Unblockable compositions of software components.
Proceedings of the 15th ACM SIGSOFT Symposium on Component Based Software Engineering, 2012

2011
Symbolic decision procedure for termination of linear programs.
Formal Aspects Comput., 2011

A Complete Method to Polynomial Differential Invariant Generation for Hybrid Systems
CoRR, 2011

Computing semi-algebraic invariants for polynomial dynamical systems.
Proceedings of the 11th International Conference on Embedded Software, 2011

2010
Connection between logical and algebraic approaches to concurrent systems.
Math. Struct. Comput. Sci., 2010

Rate monotonic scheduling re-analysed.
Inf. Process. Lett., 2010

On hierarchically developing reactive systems.
Inf. Comput., 2010

Recent advances in program verification through computer algebra.
Frontiers Comput. Sci. China, 2010

Refinement of models of software components.
Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), 2010

A Calculus for Hybrid CSP.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Refinement and verification in component-based model-driven design.
Sci. Comput. Program., 2009

Model Checking Linear Duration Invariants of Networks of Automata.
Proceedings of the Fundamentals of Software Engineering, 2009

2008
Formalising Scheduling Theories in Duration Calculus.
Nord. J. Comput., 2008

Basic research in computer science and software engineering at SKLCS.
Frontiers Comput. Sci. China, 2008

Component Publications and Compositions.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

Program Verification by Reduction to Semi-algebraic Systems Solving.
Proceedings of the Leveraging Applications of Formal Methods, 2008

2007
Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems.
Proceedings of the Theoretical Aspects of Computing, 2007

A Model of Component-Based Programming.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Modelling with Relational Calculus of Object and Component Systems - rCOS.
Proceedings of the Common Component Modeling Example: Comparing Software Component Models [result from the Dagstuhl research seminar for CoCoME, 2007

Generating Polynomial Invariants with DISCOVERER and QEPCAD.
Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006
Connecting Algebraic and Logical Descriptions of Concurrent Systems.
Proceedings of the Leveraging Applications of Formal Methods, 2006

2005
Compositional Properties of Sequential Processes.
Electron. Notes Theor. Comput. Sci., 2005

Program Verification by Using DISCOVERER.
Proceedings of the Verified Software: Theories, 2005

Compositionality of Fixpoint Logic with Chop.
Proceedings of the Theoretical Aspects of Computing, 2005

Deriving Non-determinism from Conjunction and Disjunction.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

2004
Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity.
Proceedings of the Formal Methods and Software Engineering, 2004

2003
Action Refinement from a Logical Point of View.
Proceedings of the Verification, 2003

Combining Hierarchical Specification with Hierarchical Implementation.
Proceedings of the Advances in Computing Science, 2003

2001
An Intuitive Formal Proof for Deadline Driven Scheduler.
J. Comput. Sci. Technol., 2001

Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol.
Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001

2000
Another formal proof for Deadline Driven Scheduler.
Proceedings of the 7th International Workshop on Real-Time Computing and Applications Symposium (RTCSA 2000), 2000

Completeness of Higher-Order Duration Calculus.
Proceedings of the Computer Science Logic, 2000

1999
A Formal Proof of the Rate Monotonic Scheduler.
Proceedings of the 6th International Workshop on Real-Time Computing and Applications Symposium (RTCSA '99), 1999


  Loading...