Write a Blog >>
ICSE 2022
Sun 8 - Fri 27 May 2022
Tue 10 May 2022 20:05 - 20:10 at ICSE room 4-even hours - Validation and Verification 4 Chair(s): Ting Su
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 May

Displayed time zone: Eastern Time (US & Canada) change

20:00 - 21:00
Validation and Verification 4Technical Track / NIER - New Ideas and Emerging Results at ICSE room 4-even hours
Chair(s): Ting Su East China Normal University
20:00
5m
Talk
Evaluating Commit Message Generation: To BLEU Or Not To BLEU?
NIER - New Ideas and Emerging Results
Samanta Dey Chennai Mathematical Institute, Venkatesh Vinayakarao Chennai Mathematical Institute, Monika Gupta IBM Research India, Sampath Dechu IBM Research
Link to publication DOI Pre-print Media Attached
20:05
5m
Talk
Data-Driven Loop Bound Learning for Termination Analysis
Technical Track
Rongchen Xu Tsinghua University, Jianhui Chen Tsinghua University, Fei He Tsinghua University
DOI Pre-print Media Attached
20:10
5m
Talk
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
20:15
5m
Talk
GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs
Technical Track
Harrison Green ForAllSecure, Thanassis Avgerinos ForAllSecure
DOI Pre-print Media Attached

Wed 11 May

Displayed 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
5m
Talk
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
5m
Talk
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
5m
Talk
Data-Driven Loop Bound Learning for Termination Analysis
Technical Track
Rongchen Xu Tsinghua University, Jianhui Chen Tsinghua University, Fei He Tsinghua University
DOI Pre-print Media Attached
03:15
5m
Talk
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
5m
Talk
GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs
Technical Track
Harrison Green ForAllSecure, Thanassis Avgerinos ForAllSecure
DOI Pre-print Media Attached
03:25
5m
Talk
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

Information for Participants
Tue 10 May 2022 20:00 - 21:00 at ICSE room 4-even hours - Validation and Verification 4 Chair(s): Ting Su
Info for room ICSE room 4-even hours:

Click here to go to the room on Midspace

Wed 11 May 2022 03:00 - 04:00 at ICSE room 4-odd hours - Validation and Verification 2 Chair(s): Grischa Liebel
Info for room ICSE room 4-odd hours:

Click here to go to the room on Midspace