Category Archives: Event

SKLCS seminar on“Program Verification: a 50-Year History”

Title: Program Verification: a 50-Year History

Abstract: The year 2019 sees the 50th anniversary of Tony Hoare’s CACM paper, “An Axiomatic Basis for Compuer Programming”. In that paper, Hoare stated: “When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics.” In this talk, I will review the 50-year history of this vision, describing the obstacles, the controversies, and progress milestones. I will conclude with the description of both impressive progress and dramatic failures exhibited over the past few years.

The talk is accessible to general CS audience.

Moshe Vardi, Bio:

Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association’s Distinguished Scientist Award, and the Church Award. He is the author and co-author of over 500 papers, as well as two books: “Reasoning about Knowledge” and “Finite Model Theory and Its Applications”. He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, UFRGS in Brazil, and the University of Liege in Belgium. He is currently a Senior Editor of of the Communications of the ACM, after having served for a decade as Editor-in-Chief.

Yong Li passed his PhD thesis defense

Congratulations to Yong Li who passed his PhD thesis defense on 1st November.

The title of the PhD thesis is “Novel Learning and Complementation Algorithms for Buchi Automata” .

The comittee members are:

  • Lijun Zhang
  • Moshe Vardi
  • Naijun Zhan
  • Sven Shewe
  • Yih-Kuen Tsay
  • Zhilin Wu













Workshop on Probabilistic and Hybrid System Verification

Local Information




1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 g1 g2 g3 g4 g5 g6

About the Workshop

Formal verification techniques have been successfully applied to complex systems such as Microsoft hardware drivers, airborne software at Airbus and consumer electronic protocols. In this context, the properties a system has to satisfy are often specified in temporal logics. The formal verification approach then verifies whether such property holds on a given system model. As an example, a property could be that the system will never reach a configuration in which two hosts share the same IP address. Formal verification of classical transition systems has received considerable attentions in the past decades: the 2007 Turing award was given to three researchers for their pioneering research in this area.

Quantitative verification is an important extension of the basic approach towards verifying systems involving various quantitative aspects, including randomizations, costs, time, and security metrics. These characteristics are the key ingredients for modeling and analyzing networked, embedded, biological and energy systems.

Verification of probabilistic systems with discrete time and discrete state spaces has first been studied in the nineties by Hansson & Jonsson. Afterwards, researchers have investigated the verification of probabilistic systems with continuous time, with nondeterminism, and various combinations of them. Today there is a very rich body of literature on theories attacking the probabilistic verification problem. Based on these theories many software tools have been developed, which are particularly appealing, as one can use them to model and analyze real life case studies. These tools are at most loosely interconnected, which limits their mutual fertilization.

Hybrid system consists of both discrete components and continuous dynamics: continuous dynamics can represent model the evolution of variables like velocity, distance or temperature, while discrete components are often used to model control effects, like the action of turning on or off the heater. Hybrid systems are very suitable for modeling controllable systems with continuous variables. On the other side, the interplay of random phenomena and continuous real-time control deserves increased attention for instance in wireless sensing and control applications. Thus, probabilistic hybrid systems arise as the genuine modeling formalism for such applications. Recently, probabilistic hybrid systems have been applied to the problem of balancing the energy production and consumption in electric power systems under renewable infeed.

The purpose of this symposium is to identify potential techniques that are the most promising to further pursued for analyzing probabilistic hybrid systems, as well as to coin entirely new techniques. The prospective participants represent the researchers in Germany and China very well, working on the probabilistic hybrid systems spectrum spanning from foundations over algorithms to applications. Due to the selection of invitees, we expect a highly cross-fertilizing atmosphere.

In this workshop, we have altogether 9 institutes from Germany and 12 from China as prospective participants. The central goal of this workshop is to form the nucleus for a research network between China and Germany for researchers in the quantitative verification area. Through the technical program, state-of-the-art knowledge will be exchanged between all the partners. Further, the workshop will create the forum for identifying research topics that both sides are interested in so as to make plans for further collaboration projects.

Local Information

  • Participants outside of Beijing will stay in the hotel Holiday Inn, Building A, No.89 Shuangqing Road, Haidian District, Beijing 100085, P.R. China. A map can be found here. Taking a taxi from the airport to the hotel will cost about 100RMB.
  • The workshop will be held at ISCAS, Institute of Software Chinese Academy of Sciences. Here is information about how to get to ISCAS from the hotel.
  • Organizers: Holger Hermanns, Naijun Zhan and Lijun Zhang.
  • Local Organizers: Please feel free to contact one of the following local organizers for assistence: Ernst Moritz Hahn (+86 132 4019 8152), Naijun Zhan (+86 138 1046 0251), Lijun Zhang (+86 158 0115 0886)


Session 1 (08:30–10:00): Hybrid Systems I
Leucker, Martin Runtime Verification of Hybrid Systems
He, Fei (贺飞) Complete and Learning-based Compositional Verification for Probabilistic Systems
Liu, Jiang (刘江) Nonlinear Estimation and Hybrid Verification
Session 2 (10:30–12:00): Probabilistic Verification II
Katoen, Joost-Pieter Automated Analysis of Probabilistic Program
Buchholz, Peter Quantitative Analysis of Systems – Beyond Markov Models
Wu, Peng (吴鹏) Towards Model Checking of Probabilistic Timed Automata with REDLIB
Session 3 (13:30–15:00): Safety and Abstractions
Dong, Wei (董威) Anticipatory Active Monitoring of Safety-Critical Systems
Chen, Liqian (陈立前) Extending octagon abstract domain with absolute value
Liu, Jing (刘静)
Li, Xuandong (李宣东) Hybrid system: modelling and verification
Session 4 (15:30–17:00): Program Verification
Kapur, Deepak Program verification and invariant generation
Kyas, Marcel Verification and Validation of Systems with Uncertain Measurements for Position Estimation
Chen, Zhengbang (陈振邦) Property Guided Dynamic Symbolic Execution
Ying, Mingsheng Floyd-Hoare Logic for Quantum Programs
Feng, Yuan Model Checking quantum Markov chains
Session 1 (08:30–10:00): Hybrid Systems II
Abate, Alessandro Computable analysis and control synthesis over complex dynamical systems via formal verification
She, Zhikun (佘志坤) Discovering Multiple Lyapunov Functions for Switched hybrid Systems
Zhan, Naijun (詹乃军) Hybrid Hoare Logic
Session 2 (10:30–12:00): Markov Chains
Krcál, Jan Compositional Verification and Optimization of Interactive Markov Chains
Jansen, David N. More or less true: DCTL for continuous-time MDPs
Wimmer, Ralf Optimal counterexamples for Markov models
afternoon: excursion (Great Wall)
Session 1 (8:30–10:00): Tools and Applications
Hermanns, Holger From Power Domains to Power Grids
Wolter, Katinka Validating retry mechanisms using queuing systems with signals
Gu, Bin Embedded systems and cybernation in spacecraft
Wang, Haifeng (王海峰) Safety verification of railway train control system
Session 2 (10:30–12:00): Modelling and Verification
Dong, Yunwei (董云卫) On Reliability Analysis for Embedded Systems with AADL Behavior Model
Wang, Zheng (王政) Runtime verification for periodic control systems
Lv, Jidong (吕继东) Model Based safety test case Generation method and its application in train
Sun, Meng (孙猛) Modeling and verification of connectors in complex systems
afternoon: excursion (Hutong tour)
Session 1 (08:30–10:00): Hybrid Systems III
Yang, Shaofa (杨绍发) Modular discrete time approximations of distributed hybrid automata
Hahn, Ernst Moritz Rewarding probabilistic hybrid automata
Abraham, Erika Reachability analysis for hybrid systems
Sesserion 2 (10:30–12:00): Probabilistic Verification II
Siegle, Markus State-of-the-art techniques and tools for performability evaluation
Tribastone, Mirco Efficient State-Space Aggregations for Large-Scale Dynamical Systems
Zhao, Lin (赵琳) Runtime Checking Temporal Properties of System Hybrid Behaviors
Session 3 (13:30–15:00): Bounded Model Checking
Bu, Lei (卜磊) SAT-LP-IIS Joint-Directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata
Zhang, Miaomiao (张苗苗) Bounded model checking of duration calculus
Liu, Wanwei (刘万伟) Bounded Model Checking of Extended Temporal Logic Cooperating Both Finite and Looping Automata Connectives
Session 4 (15:30–17:00): Probabilistic Verification II
Zhang, Lijun (张立军) Probabilistic Model Checking for Linear Temporal Logics
Song, Lei Late Weak Bisimularity for Markov Automata
Turrini, Andrea The Algorithmics of Probabilistic Automata Weak Bisimulation


We are grateful to Sino-German Center for their generous sponsorship of this event.