This program is tentative and subject to change.

Wed 17 Jul 2024 16:36 - 16:54 at Baobá 4 - Program Analysis and Performance 1

Comprehensive verification/falsification of embedded software is challenging and often impossible mainly due to the typical characteristics of embedded software, such as the use of global variables, reactive behaviors, and its (soft or hard) real-time requirements, to name but a few. Abstraction is one of the major solutions to this problem, but existing proven abstraction techniques are not effective in this domain as they are uniformly applied to the entire program and often require a large number of refinements to find true alarms. This work proposes a domain-specific solution for efficient property falsification based on the observation that embedded software typically consists of a number of user-defined auxiliary functions, many of which may be loosely coupled with the main control logic. Our approach selectively abstracts auxiliary functions using function summaries synthesized by Programming-By-Example (PBE), which reduces falsification complexity as well as the number of refinements. The drawbacks of using PBE-based function summaries, which are neither sound nor complete, for abstraction are counteracted by symbolic alarm filtering and novel PBE-based refinements for function summaries. We demonstrate that the proposed approach has comparable performance to the state-of-the-art model checkers on SV-COMP benchmark programs and outperforms them on a set of typical embedded software in terms of both falsification efficiency and scalability.

This program is tentative and subject to change.

Wed 17 Jul

Displayed time zone: Brasilia, Distrito Federal, Brazil change

16:00 - 18:00
16:00
18m
Talk
DyPyBench: A Benchmark of Executable Python Software
Research Papers
Islem BOUZENIA University of Stuttgart, Bajaj Piyush Krishan University of Stuttgart, Michael Pradel University of Stuttgart
16:18
18m
Talk
Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point Slicing
Research Papers
16:36
18m
Talk
PBE-based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded Software
Research Papers
Yoel Kim Kyungpook National University, Yunja Choi Kyungpook National University
Pre-print
16:54
18m
Talk
Predictive Program Slicing via Execution Knowledge-Guided Dynamic Dependence Learning
Research Papers
Aashish Yadavally University of Texas at Dallas, Yi Li University of Texas at Dallas, Tien N. Nguyen University of Texas at Dallas
Pre-print
17:12
18m
Talk
Checking Complex Source Code-level Constraints using Runtime Verification
Industry Papers
Joshua Heneage Dawes University of Luxembourg, Domenico Bianculli University of Luxembourg
17:30
9m
Talk
XGuard: Detecting Inconsistency Behaviors of Crosschain Bridges
Demonstrations
Ke Wang Peking University, Yue Li Peking University, Che Wang Peking University, China, Jianbo Gao Peking University, Zhi Guan Peking University, Zhong Chen
17:39
9m
Talk
Rapid Taint Assisted Concolic Execution (TACE)
Demonstrations
Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Norbert Tihanyi Technology Innovation Institute, Mthandazo Ndhlovu Technology Innovation Institute, Mohamed Amine Ferrag Technology Innovation Institute, Lucas C. Cordeiro University of Manchester, UK
17:48
9m
Talk
Verification of Programs with Common Fragments
Ideas, Visions and Reflections
Ivan Postolski University of Buenos Aires, Víctor Braberman ICC (UBA-CONICET), Diego Garbervetsky Departamento de Computación, FCEyN, UBA, Sebastian Uchitel Imperial College and University of Buenos Aires