General Topics on July 21, 2024

Paper Venue Title of the Presentation Presenter Time Slot
ICFP 2024 Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System Linyu Yang 10:00-10:30
POPL 2024 Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs Sergei Novozhilov 10:30-11:00
OOPSLA 2024 Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach Yutao Sun 11:00-11:30
PLDI 2024 Equivalence and Similarity Refutation for Probabilistic Programs Mingqi Yang 13:00-13:30
OSDI 2023 BWoS: Formally Verified Block-based Work Stealing for Parallel Processing Xiaqing Zhou 13:30-14:00
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Presenter: Linyu Yang Authors: Satoshi Kura and Hiroshi Unno Abstract: Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs.
Jul 21, 2024
BWoS: Formally Verified Block-based Work Stealing for Parallel Processing
Presenter: Xiaqing Zhou Authors: Jiawei Wang, Bohdan Trach, Ming Fu, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig and Haibo Chen Abstract: Work stealing is a widely-used scheduling technique for parallel processing on multicore.
Jul 21, 2024
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
Presenter: Yutao Sun Authors: Haonan Li, Yu Hao, Yizhuo Zhai and Zhiyun Qian Abstract: While static analysis is instrumental in uncovering software bugs, its precision in analyzing large and intricate codebases remains challenging.
Jul 21, 2024
Equivalence and Similarity Refutation for Probabilistic Programs
Presenter: Mingqi Yang Authors: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić Abstract: We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs.
Jul 21, 2024
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Presenter: Sergei Novozhilov Authors: Julian Müllner, Marcel Moosbrugger and Laura Kovács Abstract: We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century.
Jul 21, 2024