General Topics on June 27, 2025

Presenter: Yucheng Wang Author: Matthew Sotoudeh Abstract: Bespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through the structure.

Presenter: Zhiyang Li Author: Mengyu Zhao, Shaowei Cai, and Yuhang Qian Abstract: Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers.

Presenter: Hengzhi Yu Author: Niklas Kochdumper, Mohammed Aristide Foughali, Peter Habermehl, and Eugene Asarin Abstract: In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems.

Presenter: Linyu Yang Author: Darius Foo, Yahui Song, and Wei-Ngan Chin Abstract: Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters.

Presenter: Yazhou Tang Author: Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte Abstract: Extended Berkeley Packet Filter (BPF) is a language and run-time system that allows non-superusers to extend the Linux and Windows operating systems by downloading user code into the kernel.

Presenter: Xiaqing Zhou Author: Daniel Neider, Rajarshi Roy Abstract: Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously challenging and error-prone.

Presenter: Mingqi Yang Abstract: Reasoning about the robustness of probabilistic programs has become an increasingly important topic. One prominent line of work is formal analysis of probabilistic program sensitivity. Probabilistic program sensitivity, in this context, refers to bounding the distance between the output distributions of two runs of a probabilistic program with similar inputs.