Naijun Zhan
According to our database^{1},
Naijun Zhan
authored at least 87 papers
between 1999 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepage:

at orcid.org
On csauthors.net:
Bibliography
2019
Editorial.
Formal Asp. Comput., 2019
Quantum Hoare Logic.
Archive of Formal Proofs, 2019
Robust invariant sets generation for stateconstrained perturbed polynomial systems.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019
ARCHCOMP19 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 RealTime Automata.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2018
Reachability Analysis for Solvable Dynamical Systems.
IEEE Trans. Automat. Contr., 2018
Robust Nontermination Analysis of Numerical Software.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018
Model Checking Bounded Continuoustime Extended Linear Duration Invariants.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018
UnderApproximating 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 Multiclock Timed Automata.
Proceedings of the Computer Aided Verification  30th International Conference, 2018
Decidability of the InitialState Opacity of RealTime Automata.
Proceedings of the Symposium on RealTime 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
ARCHCOMP18 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 semialgebraic invariants for nonautonomous 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 HoareStyle Reasoning About Hybrid CSP in the Duration Calculus.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2017
Safe Over and UnderApproximation 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 TwoWay 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 SimulationBased 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 nonterminating inputs for multipath polynomial programs.
J. Systems Science & Complexity, 2014
Hybrid annex: an AADL extension for continuous behavior and cyberphysical 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 continuoustime 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 modelchecking of discrete duration calculus.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013
SuperDense 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 Nonlinear 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 ContinuousTime 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 semialgebraic 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 reanalysed.
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 componentbased modeldriven 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 Semialgebraic Systems Solving.
Proceedings of the Leveraging Applications of Formal Methods, 2008
2007
Discovering Nonlinear Ranking Functions by Solving Semialgebraic Systems.
Proceedings of the Theoretical Aspects of Computing, 2007
A Model of ComponentBased 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 RealTime 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 Nondeterminism from Conjunction and Disjunction.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005
2004
Refinement of Actions for RealTime 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 AsiaPacific Software Engineering Conference (APSEC 2001), 2001
2000
Another formal proof for Deadline Driven Scheduler.
Proceedings of the 7th International Workshop on RealTime Computing and Applications Symposium (RTCSA 2000), 2000
Completeness of HigherOrder 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 RealTime Computing and Applications Symposium (RTCSA '99), 1999