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

Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.

Slides (CPA-DF_ASE_slides.pdf)1.45MiB

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