Wed 23 Oct 2024 16:40 - 17:00 at IBR East - Static Analysis and Program Verification 3 Chair(s): Frank Tip

In recent years, there has been an increasing interest in tools that establish incorrectness rather than correctness of program properties. In this work we build on this approach by developing a novel methodology for proving incorrectness of semantic typing properties of functional programs, extending the incorrectness approach to the model theory of functional program typing. We define a semantic type refuter which refutes semantic typings for a simple functional language. We prove our refuter is co-recursively enumerable, and that it is sound and complete with respect to a semantic typing notion. An initial implementation is described which uses symbolic evaluation to efficiently find type errors over a functional language with a rich type system.

Wed 23 Oct

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

16:00 - 17:40
Static Analysis and Program Verification 3OOPSLA 2024 at IBR East
Chair(s): Frank Tip Northeastern University
16:00
20m
Talk
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
OOPSLA 2024
Haonan Li University of California at Riverside, USA, Yu Hao University of California at Riverside, USA, Yizhuo Zhai University of California at Riverside, USA, Zhiyun Qian University of California at Riverside, USA
DOI
16:20
20m
Talk
PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis
OOPSLA 2024
Zhaoyu Wang HKUST, Pingchuan Ma HKUST, Huaijin Wang , Shuai Wang Hong Kong University of Science and Technology
DOI
16:40
20m
Talk
Semantic-Type-Guided Bug Finding
OOPSLA 2024
Kelvin Qian Johns Hopkins University, Scott F. Smith The Johns Hopkins University, Brandon Stride Johns Hopkins University, Shiwei Weng Johns Hopkins University, Ke Wu Johns Hopkins University
DOI
17:00
20m
Talk
Seneca: Taint-Based Call Graph Construction for Java Object Deserialization
OOPSLA 2024
Joanna C. S. Santos University of Notre Dame, Mehdi Mirakhorli Rochester Institute of Technology, Ali Shokri Virginia Tech
DOI
17:20
20m
Talk
VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity ConstraintsOOPSLA 2024 Distinguished Paper Award
OOPSLA 2024
Yang He Simon Fraser University, Pinhan Zhao University of Michigan, Xinyu Wang University of Michigan, Yuepeng Wang Simon Fraser University
DOI Pre-print