ePMC is publicly available

ePMC, the Extendible Probabilistic Model Checker, is now available publicly. It can be accessed online on GitHub, at this repository.

ePMC is the successor of IscasMC, from which it keeps all features about Linear Time Logic probabilistic model checking. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker.

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:

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

*** Photos to be added

讨论班小结_0407

This is a summary of the group meetings on 7 April, 2021

L*- Based Learning of Markov Decision Processes

They provide two algorithms to learn a given black-box Markov decision processes based on Angluin’s L* algorithm. They are exact learning and sample-based learning, respectively.

Q: What is for unambiguous?
A: The compatibility relation is not an equivalence relation, and a state may belong to more than one classes, which we call an ambiguous state, so for an unambiguous state, there is only one class whose representation is compatible with it.

Q: How to check equivalence in exact learning?
A: First it checks whether the hypothesis is isomophic to the model. If so, we only need finitely many output distribution queries to determine all the transition probabilities.

Q: Is there a quantitative description of the convergence?
A: Not yet in the paper. In the paper it only gives a convergence description based on Borel-Cantelli Lemma. It is interesting to consider its PAC guarantee description.

Q: Can MDP learning used for model checking and other field in software engineering?
A: There are some experiments in the paper. We need more investigation on this part.

讨论班小结_0324

This is a summary of the group meetings on 24 March, 2021

Efficient Certification of Spatial Robustness

这篇文章提出了一种计算范数约束向量场攻击的紧区间界限的新方法,使神经网络能够对向量场攻击进行验证。 首先是对每个像素的变换计算一个很紧的区间界,然后提出一个方法用线性平面去拟合这个上界和下界,也就是用线性平面计算它的凸松弛。并且展示了如何通过flow constraints来提供一个更紧的凸松弛。这种方法可以收紧对光滑向量场的松弛,并且可以和目前主流的鲁棒性验证器集成。

Questions:

  1. 在二范数的情况下,如何通过平面去约束球体呢?

二范数的时候实际上也是先计算这个球体可能达到最大值和最小值的一些候选集点,通过平面对这些候选集点进行拟合和约束,而不是用平面去约束一个球。

  1. 这个向量场攻击有什么实际意义吗?

向量场攻击包括了对图形的旋转,平移,放大缩小以及改变图像像素值的亮度等,如果攻击方式满足文中提出的流约束,就可以通过这个方法解决神经网络的鲁棒性问题。

  1. 文章有说可以解决什么样的流约束吗?或者这个流约束是怎么定义的?

流约束的直观意义是两个像素的位移向量不能相差太大,也就是像素的变换是“光滑”的。它的标准定义是:

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

JCST Special Section on Software Systems 2020

The Journal of Computer Science & Technology, a CCF B ranked journal, is going to have a special section on software systems. Software systems have played critical roles in scientific research, business and society with research focuses on construction, operation, maintenance, and assessment of software systems. The special section is an effort to encourage and promote research to address challenges from the software systems perspective and its goal is to present the state-of-the-art and high-quality original research papers in the area of software systems.

The JCST’s special section of software systems covers two main themes:

  • Internetware and Beyond, aiming to provide a forum where researchers and professionals from multiple disciplines and domains share ideas to explore and address the challenges brought by Internetware. It solicits submissions describing results of theoretical, empirical, conceptual, and experimental software engineering research related to Internetware.
  • Dependable Software Engineering, soliciting submissions describing theoretical results, tools, and applications, related to applying formal methods in improving the quality of computer software and systems.

Accepted papers to the Dependable Software Engineering theme will be presented and discussed at the SETTA 2020 conference.

Papers need to be submitted before April 10, 2020; for more details about the themes, submission instructions and deadlines, see the official JCST CFP page.

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 http://im.ntu.edu.tw/~tsay/.