Wed 6 Dec 2023 17:30 - 17:45 at Golden Gate C2 - Formal Verification Chair(s): Christoph Treude

Interrupt-driven programs have been widely used in safety-critical areas such as aerospace and embedded systems. However, uncertain interleaving execution of interrupt service routines (ISRs) usually causes concurrency bugs. Specifically, when one or more ISRs attempt to preempt a sequence of instructions which are expected to be atomic, a kind of concurrency bugs namely atomicity violation may occur, and it is challenging to find this kind of bugs precisely and efficiently. In this paper, we propose a static approach for detecting atomicity violations in interrupt-driven programs. First, the program model is constructed with interruption points being selected to determine the possibly influenced ISRs. After that, reachability computation is conducted to build up a whole abstract reachability tree, and a delayed ISR-triggering strategy is employed to reduce the state space. Meanwhile, unserializable interleaving patterns are recognized to achieve the goal of atomicity violation detection. The approach has been implemented as a configurable tool namely CPA4AV. Extensive experiments show that CPA4AV is much more precise than the relative tools available with little extra time overhead. In addition, more complex situations can be dealt with CPA4AV.

Wed 6 Dec

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

16:00 - 18:00
16:00
15m
Talk
State Merging with Quantifiers in Symbolic Execution
Research Papers
David Trabish Tel Aviv University, Noam Rinetzky Tel Aviv University, Sharon Shoham Tel Aviv University, Vaibhav Sharma University of Minnesota
DOI Pre-print Media Attached
16:15
15m
Talk
Towards Strengthening Formal Specifications with Mutation Model Checking
Ideas, Visions and Reflections
Maxime Cordy SnT, University of Luxembourg, Sami Lazreg SnT, University of Luxembourg, Axel Legay Université Catholique de Louvain, Belgium, Pierre Yves Schobbens University of Namur
Media Attached
16:30
15m
Talk
PropProof: Free Model-Checking Harnesses from PBT
Industry Papers
Yoshiki Takashima Carnegie Mellon University
DOI Media Attached
16:45
15m
Talk
Engineering a Formally Verified Automated Bug Finder
Research Papers
Arthur Correnson CISPA Helmholtz Center for Information Security, Dominic Steinhöfel CISPA Helmholtz Center for Information Security
Media Attached
17:00
15m
Talk
LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems
Industry Papers
Yibo Dong East China Normal University; Shanghai Trusted Industrial Control Platform, Xiaoyu Zhang East China Normal University, Yicong Xu East China Normal University, Chang Cai East China Normal University, Yu Chen East China Normal University, Weikai Miao East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University
DOI Media Attached
17:15
15m
Talk
Speeding up SMT Solving via Compiler Optimization
Research Papers
Benjamin Mikek Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
Media Attached
17:30
15m
Talk
[Remote] Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering
Research Papers
Bin Yu School of Computer Science and Technology, Xidian University, Cong Tian Xidian University, Hengrui Xing School of Computer Science and Technology, Xidian University, Zuchao Yang School of Computer Science and Technology, Xidian University, Jie Su School of Computer Science and Technology, Xidian University, Xu Lu School of Computer Science and Technology, Xidian University, Jiyu Yang School of Computer Science and Technology, Xidian University, Liang Zhao School of Computer Science and Technology, Xidian University, Xiaofeng Li Beijing Institute of Control Engineering, Zhenhua Duan Xidian University
Media Attached
17:45
7m
Talk
[Remote] P4b: A Translator from P4 Programs to Boogie
Demonstrations
Chong Ye Tsinghua University, Fei He Tsinghua University
Media Attached