Write a Blog >>
ICSE 2022
Sun 8 - Fri 27 May 2022
Tue 10 May 2022 20:10 - 20:15 at ICSE room 4-even hours - Validation and Verification 4 Chair(s): Ting Su
Wed 11 May 2022 03:15 - 03:20 at ICSE room 4-odd hours - Validation and Verification 2 Chair(s): Grischa Liebel

Deep learning has been increasingly adopted in many application areas. To construct valid deep learning models, developers must conform to certain computational constraints by carefully selecting appropriate neural architectures and hyperparameter values. For example, the kernel size hyperparameter of the 2D convolution operator cannot be overlarge to ensure that the height and width of the output tensor remain positive. Because model construction is largely manual and lacks necessary tooling support, it is possible to violate those constraints and raise type errors of deep learning models, causing either runtime exceptions or wrong output results. In this paper, we propose Refty, a refinement type-based tool for statically checking the validity of deep learning models ahead of job execution. Refty refines each type of deep learning operator with framework-independent logical formulae that describe the computational constraints on both tensors and hyperparameters. Given the neural architecture and hyperparameter domains of a model, Refty visits every operator, generates a set of constraints that the model should satisfy, and utilizes an SMT solver for solving the constraints. We have evaluated Refty on both individual operators and representative real-world models with various hyperparameter values under PyTorch and TensorFlow. We also compare it with an existing shape-checking tool. The experimental results show that Refty finds all the type errors and achieves 100% Precision and Recall, demonstrating its effectiveness.

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