| Publication | Date of Publication | Type |
|---|
| Runtime enforcement of CPS against signal temporal logic | 2025-11-07 | Paper |
Introduction to the special Section on FM 2021
Formal Aspects of Computing | 2024-09-25 | Paper |
Reach-avoid verification based on convex optimization
IEEE Transactions on Automatic Control | 2024-07-21 | Paper |
Reach-avoid analysis for polynomial stochastic differential equations
IEEE Transactions on Automatic Control | 2024-07-21 | Paper |
Switching controller synthesis for delay hybrid systems under perturbations
Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control | 2024-02-21 | Paper |
Formal verification of quantum algorithms using quantum Hoare logic
Computer Aided Verification | 2024-02-16 | Paper |
Taming delays in dynamical systems. Unbounded verification of delay differential equations
Computer Aided Verification | 2024-02-16 | Paper |
Decidability of the initial-state opacity of real-time automata
Lecture Notes in Computer Science | 2023-08-02 | Paper |
What's to come is still unsure. Synthesizing controllers resilient to delayed interaction
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
Learning deterministic one-clock timed automata via mutation testing
Automated Technology for Verification and Analysis | 2023-06-02 | Paper |
Monitoring CTMCs by multi-clock timed automata
Computer Aided Verification | 2023-05-26 | Paper |
Robust non-termination analysis of numerical software
Dependable Software Engineering. Theories, Tools, and Applications | 2023-05-26 | Paper |
| Lower Bounds for Possibly Divergent Probabilistic Programs | 2023-02-12 | Paper |
Synthesizing SystemC Code from Delay Hybrid CSP
Programming Languages and Systems | 2022-12-09 | Paper |
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
Information and Computation | 2022-12-08 | Paper |
A denotational semantics of simulink with higher-order UTP
Journal of Logical and Algebraic Methods in Programming | 2022-11-16 | Paper |
Compositional Hoare-style reasoning about hybrid CSP in the duration calculus
Dependable Software Engineering. Theories, Tools, and Applications | 2022-11-04 | Paper |
Learning one-clock timed automata
Tools and Algorithms for the Construction and Analysis of Systems | 2022-10-13 | Paper |
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
(available as arXiv preprint) | 2022-09-20 | Paper |
| Probably approximately correct interpolants generation | 2022-09-01 | Paper |
Finding polynomial loop invariants for probabilistic programs
Automated Technology for Verification and Analysis | 2022-08-12 | Paper |
Synthesizing invariant barrier certificates via difference-of-convex programming
(available as arXiv preprint) | 2022-03-25 | Paper |
Switching controller synthesis for time-delayed hybrid systems
SCIENTIA SINICA Mathematica | 2022-03-21 | Paper |
Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems
IEEE Transactions on Automatic Control | 2022-02-24 | Paper |
Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow
Theoretical Computer Science | 2022-02-01 | Paper |
Indecision and delays are the parents of failure -- taming them algorithmically by synthesizing delay-resilient control
Acta Informatica | 2021-09-30 | Paper |
Inferring switched nonlinear dynamical systems
Formal Aspects of Computing | 2021-08-30 | Paper |
Synthesizing robust domains of attraction for state-constrained perturbed polynomial systems
SIAM Journal on Control and Optimization | 2021-04-09 | Paper |
Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations
IEEE Transactions on Automatic Control | 2021-03-12 | Paper |
Unbounded-time safety verification of stochastic differential dynamics
(available as arXiv preprint) | 2021-02-09 | Paper |
Nonlinear Craig interpolant generation
(available as arXiv preprint) | 2021-02-04 | Paper |
Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties
IEEE Transactions on Automatic Control | 2020-10-07 | Paper |
NIL: learning nonlinear interpolants
(available as arXiv preprint) | 2020-03-10 | Paper |
| Unified graphical co-modelling of cyber-physical systems using AADL and Simulink/Stateflow | 2020-02-18 | Paper |
| Validated simulation-based verification of delayed differential dynamics | 2020-01-03 | Paper |
Approximate bisimulation and discretization of hybrid CSP
(available as arXiv preprint) | 2020-01-03 | Paper |
Robust invariant sets generation for state-constrained perturbed polynomial systems
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control | 2019-10-22 | Paper |
| Overview of formal methods | 2019-09-20 | Paper |
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-12-06 | Paper |
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-12-06 | Paper |
| Reach-Avoid Differential Games Based on Invariant Generation | 2018-11-07 | Paper |
Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties
(available as arXiv preprint) | 2018-11-02 | Paper |
| Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems | 2018-10-28 | Paper |
Reachability Analysis for Solvable Dynamical Systems
IEEE Transactions on Automatic Control | 2018-09-18 | Paper |
| Automatic verification of stability and safety for delay differential equations | 2018-03-01 | Paper |
| Safety verification of trajectory planning for multiple robots | 2018-01-29 | Paper |
| Formal Verification of Simulink/Stateflow Diagrams | 2018-01-08 | Paper |
| Safe over- and under-approximation of reachable sets for delay differential equations | 2017-12-01 | Paper |
A compositional modelling and verification framework for stochastic hybrid systems
Formal Aspects of Computing | 2017-09-08 | Paper |
Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
Journal of Systems Science and Complexity | 2017-09-06 | Paper |
Extending hybrid CSP with probability and stochasticity
Dependable Software Engineering: Theories, Tools, and Applications | 2017-08-31 | Paper |
Bounded model-checking of discrete duration calculus
Proceedings of the 16th international conference on Hybrid systems: computation and control | 2017-05-16 | Paper |
A two-way path between formal and informal design of embedded systems
Unifying Theories of Programming | 2017-04-04 | Paper |
Barrier certificates revisited
Journal of Symbolic Computation | 2017-02-06 | Paper |
Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
Automated Reasoning | 2016-09-05 | Paper |
Decidability of the reachability for a family of linear vector fields
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Formal verification of Simulink/Stateflow diagrams
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Formal modelling, analysis and verification of hybrid systems
Lecture Notes in Computer Science | 2015-09-30 | Paper |
Discovering non-terminating inputs for multi-path polynomial programs
Journal of Systems Science and Complexity | 2015-04-27 | Paper |
CCMC: a conditional CSL model checker for continuous-time Markov chains
Automated Technology for Verification and Analysis | 2014-07-08 | Paper |
Generating non-linear interpolants by semidefinite programming
Computer Aided Verification | 2013-11-26 | Paper |
An interface model of software components
Theoretical Aspects of Computing – ICTAC 2013 | 2013-10-04 | Paper |
| Compositional properties of sequential processes | 2013-09-20 | Paper |
Synthesizing switching controllers for hybrid systems by generating invariants
Theories of Programming and Formal Methods | 2013-08-16 | Paper |
Recent advances in program verification through computer algebra
Frontiers of Computer Science in China | 2013-07-04 | Paper |
Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
Mathematics in Computer Science | 2013-04-25 | Paper |
Model checking conditional CSL for continuous-time Markov chains
Information Processing Letters | 2013-03-21 | Paper |
A ``hybrid approach for synthesizing optimal controllers of hybrid systems: a case study of the oil pump industrial example
FM 2012: Formal Methods | 2012-11-08 | Paper |
An assume/guarantee based compositional calculus for hybrid CSP
Lecture Notes in Computer Science | 2012-07-16 | Paper |
Symbolic decision procedure for termination of linear programs
Formal Aspects of Computing | 2011-05-27 | Paper |
Connection between logical and algebraic approaches to concurrent systems
Mathematical Structures in Computer Science | 2010-12-01 | Paper |
On hierarchically developing reactive systems
Information and Computation | 2010-10-07 | Paper |
Rate monotonic scheduling re-analysed
Information Processing Letters | 2010-09-07 | Paper |
Component publications and compositions
Unifying Theories of Programming | 2010-08-31 | Paper |
Model checking linear duration invariants of networks of automata
Fundamentals of Software Engineering | 2010-01-28 | Paper |
| Formalising scheduling theories in duration calculus | 2009-10-12 | Paper |
Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
Lecture Notes in Computer Science | 2009-08-11 | Paper |
Refinement and verification in component-based model-driven design
Science of Computer Programming | 2009-03-02 | Paper |
Generating Polynomial Invariants with DISCOVERER and QEPCAD
Formal Methods and Hybrid Real-Time Systems | 2008-09-25 | Paper |
Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
Theoretical Aspects of Computing – ICTAC 2007 | 2008-09-17 | Paper |
A Model of Component-Based Programming
Lecture Notes in Computer Science | 2008-07-01 | Paper |
A higher-order duration calculus and its completeness
Science in China. Series E | 2007-02-20 | Paper |
Theoretical Aspects of Computing – ICTAC 2005
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Formal Techniques for Networked and Distributed Systems - FORTE 2005
Lecture Notes in Computer Science | 2006-07-07 | Paper |
| scientific article; zbMATH DE number 1953035 (Why is no real title available?) | 2003-07-25 | Paper |
| scientific article; zbMATH DE number 1670495 (Why is no real title available?) | 2001-11-11 | Paper |
An intuitive formal proof for deadline driven scheduler
Journal of Computer Science and Technology | 2001-10-14 | Paper |
