Naijun Zhan

According to our database1, Naijun Zhan authored at least 87 papers between 1999 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2019
Editorial.
Formal Asp. Comput., 2019

Quantum Hoare Logic.
Archive of Formal Proofs, 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

2018
The Opacity of Real-Time Automata.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2018

Reachability Analysis for Solvable Dynamical Systems.
IEEE Trans. Automat. Contr., 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. Systems Science & Complexity, 2017

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems.
Formal Asp. 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 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 2016 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
Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL.
SCIENCE CHINA Information Sciences, 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. Systems Science & Complexity, 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

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.
Mathematics in Computer Science, 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 Asp. Comput., 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.
Mathematical Structures in Computer Science, 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.
Electr. 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...