Category Archives: Event

Jianlin Li Passed His Master Thesis Defense

Congratulations to Jianlin Li who passed his Master thesis defense on 26th May, 2021.

The title of the Master thesis is “Symbolic Propagation Based Local Robustness Verification of Deep Neural Networks and Verification Platform”.

The comittee members are:

  • Yongzhi Cao (Chair)
  • Lijun Zhang
  • Zhilin Wu
  • David N. Jansen

Pengfei Yang Passed His PhD Thesis Defense

Congratulations to Pengfei Yang who passed his PhD thesis defense on 26th May, 2021.

The title of the PhD thesis is “Rubustness Verification of Deep Neurual Networks Based on Abstract Interpretation and Lipschitz Constants” .

The comittee members are:

  • Naijun Zhan (Chair)
  • Lijun Zhang
  • Wenhui Zhang
  • Yongzhi Cao
  • Meng Sun
  • Zhilin Wu

Junnan Xu Passed His Master Thesis Defense

Congratulations to Junnan Xu who passed his Master thesis defense on Aug. 27th, 2020.

The title of his thesis is “An Axiomatisation of the Probabilistic μ-Calculus“.

The committee members are:

  • Yuan Feng (chair)
  • Wanwei Liu
  • Zhilin Wu
  • Naijun Zhan

Xuechao Sun Passed His Master Thesis Defense

Congratulations to Xuechao Sun who passed his Master thesis defense on May 23rd 2020.

The title of his thesis is “Synthesizing Nested Ranking Functions for Loop Programs via SVM“.

The committee members are:

  • Yuan Feng (chair)
  • Yi Li
  • Zhilin Wu
  • Lijun Zhang

SKLCS seminar on“Automata for Profit and Pleasure”

Title:Automata for Profit and Pleasure

Abstract:When admiring the beauty of automata, we look at their basic properties, like optimal transformations between different types and the principle costs they incur. But their beauty shouldn’t allow us to become blind to their usefulness, and when we want to profit, the questions change. For example, finer traits than alternating/nondeterministic/determinstic come to the fore: we want automata that are fit for purpose. The first time that this has been named explicitly was in the discussion of good-for-games automata, but it has occurred much earlier, e.g. (speaking as Lijun’s guest) in using limit determinism in the evaluation of MDPs.
There are more such examples, such as using mild subclasses of unambiguous automata for the evaluation of Markov chains, good-for-MDP automata, and good-for-small-games automata, that allow us to combine pleasure with profit—just like when one works in academia.

Sven Schewe, Bio:
I am a Professor at the Department of Computer Science of the University of Liverpool, where I lead the AI Section. I am a founding member and former leader of our Verification Group and have a secondary affiliation with the Algorithms, Complexity Theory and Optimisation Group. I am also affiliated with the Institute for Risk and Uncertainty.

I gained a Diplom degree in Computer Science (Diplom Informatiker) with a minor in Operations Research and Planning in 1997 from the University of the Federal Armed Forces Munich. Then I worked in the Command and Control Systems Command of the German Navy as a Systems Engineer in different fields of the analysis and construction of safety-critical systems, including the specification and construction of such systems as well as quality assurance and project management. To complement this, I gave myself a treat and studied Math at the FernUniversität in Hagen, earning a degree in Mathematics (Diplom Mathematiker) in 2004. Returning to education, I joined the Reactive Systems Group at the Department of Computer Science of Saarland University in 2004, and obtained a PhD (Dr. rer. nat.) in Computer Science in 2008, moving on to an academic position in Liverpool.

SKLCS seminar on“Conventional Suggestions to the Automata-Theoretic Community”

Title: Conventional Suggestions to the Automata-Theoretic Community

Abstract: For better communications, when presenting existing works or new findings, researchers follow established conventions, including preferred choices among alternative definitions, names, etc. Conventions may change and evolve over time. In this talk, I will suggest and justify three conventional changes to the theory of automata on which the automata-theoretic community heavily relies. The first and the second changes are about the initial setting and the computations of an automaton, while the third is about a complementation construction.

Yih-Kuen Tsay, Bio:

Dr. Yih-Kuen Tsay is a professor in the Department of Information Management at National Taiwan University. Dr. Tsay received his B.S. degree from National Taiwan University in 1984 and his M.S. and Ph.D. degrees from the University of California at Los Angeles in 1989 and 1993, all in Computer Science. In 1995, after two years as a postdoctoral research fellow at Uppsala University in Sweden, Dr. Tsay returned to Taiwan to join his current department. He was the department chair from 2013 to 2017.

Dr. Tsay is generally interested in rigorous methods and practically usable tools that help ensure correctness, safety, and security of computer software. In terms of specific areas, his research interests include formal verification, temporal logic, automata theory, and software security. Further information may be found on his personal homepage at

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