ASE 2023
Mon 11 - Fri 15 September 2023 Kirchberg, Luxembourg
Wed 13 Sep 2023 14:18 - 14:30 at Room C - Program Verification 1 Chair(s): Nico Rosner

Two-player games are a fruitful way to represent and reason about several important synthesis tasks. These tasks include controller synthesis (where one asks for a controller for a given plant such that the controlled plant satisfies a given temporal specification), program repair (setting values of variables to avoid exceptions), and synchronization synthesis (adding lock/unlock statements in multi-threaded programs to satisfy safety assertions). In all these applications, a solution directly corresponds to a winning strategy for one of the players in the induced game. In turn, \emph{logically-specified} games offer a powerful way to model these tasks for large or infinite-state systems. Much of the techniques proposed for solving such games typically rely on abstraction-refinement or template-based solutions. In this paper, we show how to apply classical fixpoint algorithms, that have hitherto been used in explicit, finite-state, settings, to a symbolic logical setting. We implement our techniques in a tool called GenSys-LTL and show that they are not only effective in synthesizing valid controllers for a variety of challenging benchmarks from the literature, but often compute maximal winning regions and maximally-permissive controllers. We achieve 46.38X speed-up over the state of the art and also scale well for non-trivial LTL specifications.

Wed 13 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Program Verification 1Research Papers / NIER Track / Tool Demonstrations at Room C
Chair(s): Nico Rosner Amazon Web Services
13:30
12m
Talk
CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification
Tool Demonstrations
Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Nian-Ze Lee LMU Munich
Pre-print Media Attached File Attached
13:42
12m
Talk
Demystifying Template-based Invariant Generation for Bit-Vector Programs
Research Papers
Peisen Yao Zhejing University, Jingyu Ke Shanghai Jiao Tong University, Jiahui Sun Zhejiang University, Hongfei Fu Shanghai Jiao Tong University, Rongxin Wu Xiamen University, Kui Ren Zhejiang University
13:54
12m
Talk
PSMT: Satisfiability Modulo Theories Meets Probability Distribution
NIER Track
Fuqi Jia Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Rui Han Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Xutong Ma State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China, Baoquan Cui Institute of Software at Chinese Academy of Sciences, China, Minghao Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Pei Huang Stanford University, Feifei Ma Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jian Zhang Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Pre-print File Attached
14:06
12m
Talk
EndWatch: A Practical Method for Detecting Non-Termination in Real-World SoftwareACM Distinguished Paper
Research Papers
Yao Zhang Tianjin University, Xiaofei Xie Singapore Management University, Yi Li Nanyang Technological University, Sen Chen Tianjin University, Cen Zhang Nanyang Technological University, Xiaohong Li Tianjin University
Pre-print File Attached
14:18
12m
Talk
Symbolic Fixpoint Algorithms for Logical LTL Games
Research Papers
Stanly Samuel Indian Institute of Science, India, Deepak D'Souza IISc Bangalore, Raghavan Komondoor Indian Institute of Science, India
Pre-print Media Attached File Attached
14:30
12m
Talk
SAT-verifiable LTL Satisfiability Checking via Graph Representation LearningRecorded talk
NIER Track
Weilin Luo Sun Yat-Sen University, Yuhang Zheng Sun Yat-Sen University, Rongzhen Ye Sun Yat-Sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Jianfeng Du Guangdong University of Foreign Studies, Pingjia Liang Sun Yat-Sen University, Polong Chen Sun Yat-Sen University
Media Attached