Wed 11 May 2022 03:10 - 03:15 at ICSE room 4-odd hours - Validation and Verification 2 Chair(s): Grischa Liebel
Termination is a fundamental liveness property for program verification. A loop bound is an upper bound of the number of loop iterations for a given program. The existence of a loop bound evidences the termination of the program. This paper employs a reinforced black-box learning approach for termination proving, consisting of a loop bound learner and a validation checker. We present efficient data-driven algorithms for inferring various kinds of loop bounds, including simple loop bounds, conjunctive loop bounds, and lexicographic loop bounds. We also devise an efficient validation checker by integrating a quick bound checking algorithm and a two-way data sharing mechanism. We implemented a prototype tool called dddlTerm. Experiments on publicly accessible benchmarks show that ddlTerm outperforms state-of-the-art termination analysis tools by solving 13-48% more benchmarks and saving 40-77% solving time.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
Wed 11 MayDisplayed time zone: Eastern Time (US & Canada) change
03:00 - 04:00 | Validation and Verification 2Technical Track / Journal-First Papers at ICSE room 4-odd hours Chair(s): Grischa Liebel Reykjavik University | ||
03:00 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
03:05 5mTalk | Verification of ORM-based Controllers by Summary Inference Technical Track Geetam Chawla Indian Insitute of Science, Bangalore, Navneet Aman Indian Institute of Science, Bangalore, Raghavan Komondoor IISc Bengaluru, Ashish Shashikant Bokil Indian Institute of Science, Bangalore, Nilesh Ramesh Kharat Indian Institute of Science, Bangalore Pre-print Media Attached | ||
03:10 5mTalk | Data-Driven Loop Bound Learning for Termination Analysis Technical Track DOI Pre-print Media Attached | ||
03:15 5mTalk | Refty: Refinement Types for Valid Deep Learning Models Technical Track Yanjie Gao Microsoft Research, lizhengxian Microsoft Research, Haoxiang Lin Microsoft Research, Hongyu Zhang University of Newcastle, Ming Wu Shanghai Tree-Graph Blockchain Research Institute, Mao Yang Microsoft Research DOI Pre-print Media Attached | ||
03:20 5mTalk | GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs Technical Track DOI Pre-print Media Attached | ||
03:25 5mTalk | MOREST: Model-based RESTful API Testing with Execution Feedback Technical Track Yi Liu Nanyang Technological University, Yuekang Li Nanyang Technological University, Gelei Deng Nanyang Technological University, Yang Liu Nanyang Technological University, Ruiyuan Wan Huawei Inc., Runchao Wu Huawei Inc., Dandan Ji Huawei Inc., Shiheng Xu Huawei Inc., Minli Bao Huawei Inc. Pre-print Media Attached |