General Topics on February 26, 2025

Presenter: Jie An Abstract: Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL).

Presenter: Linyu Yang Author: Damien Pous Abstract: We revisit coinductive proof principles from a lattice theoretic point of view. By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski’s seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques).

Presenter: Hengzhi Yu Bohan Ma Abstract: In the domain of cyber-physical systems, there is an increasing relevance of data-driven approaches for the learning of hybrid system dynamics. In particular, accurate models have been successfully abstracted from continuous (real-valued) traces and applied for various goals.

Presenter: Zhiyang Li Authors: Ehud Hrushovski, Oxford University; Jo{"e}l Ouaknine, Max Planck Institute for Software Systems; Amaury Pouly, Universit'{e} de Paris, IRIF, CNRS; James Worrell, Oxford University Abstract: A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional).

Presenter: Mingqi Yang Authors: Sergei Novozhilov, Hong Kong University of Science and Technology; Mingqi Yang, Zhejiang University; Mingshuai Chen, Zhejiang University; Zhiyang Li, Zhejiang University; Jianwei Yin, Zhejiang University Abstract: This paper introduces $k$-d PCPs – the class of probabilistic counter programs with $k \in \mathbb{N}$ counter variables inducing possibly infinite-state Markov chains.

Presenter: Shenghua Feng Abstract: Formal verification is the only proven method for ensuring that a system is completely free of programming errors. By providing a mathematical proof, it guarantees that an OS kernel performs as expected under all possible conditions.

Presenter: Zhongyi Wang Abstract: Formal verification offers a rigorous approach to ensuring the correctness and reliability of software systems. However, constructing full specifications for verification requires domain expertise and considerable effort.

Presenter: Yutao Sun Authors: Yutao Sun, Zhejiang University; Mingshuai Chen, Zhejiang University; Tiancheng Zhao, Binjiang Institute of Zhejiang University; Ruochen Xu, Om AI Research; Zilun Zhang, Zhejiang University; Jianwei Yin, Zhejiang University

Presenter: Xiaqing Zhou Abstract: First, we introduce Unikernels, a lightweight operating system architecture that compiles application logic with minimal library dependencies into a single address space, contrasting it with traditional monolithic and modular OS designs.