SETTA 2024

Symposium on Dependable Software Engineering

Theories, Tools and Applications

Hong Kong, China, Nov. 26-28, 2024

KEYNOTE SPEAKERS

Keynote 1: MIMOS: A New Paradigm and Tools for Embedded Systems Design and Updates

Speaker: Wang Yi 
(Uppsala University)

Abstract: MIMOS is a tool environment for the design, simulation, verification, scheduling, and code generation of embedded real-time systems on heterogeneous multi-core platforms. MIMOS primarily targets safety-critical applications, where correct functional and timing behaviors are essential. The MIMOS tools provide a seamless approach to safe system development, ensuring that specified functionalities and timing behaviors specified and verified during the design phase are faithfully realized in the final implementation. This allows for customizable embedded real-time systems, enabling modifications to the design model without touching the executables in the final implementation.

Unlike existing tools such as Simulink and SCADE, which are all rooted in the synchronous design paradigms, MIMOS employs an asynchronous yet deterministic semantics model. This model is designed to not only guarantee (1) determinism but also facilitate (2) composability throughout all design stages, from system modeling to final implementation. This allows for dynamic updates for systems in operation. Furthermore, the asynchronous semantics of MIMOS enables pipelined parallel computation for (3) optimal performance with respects to both end-to-end latency and system throughput.

Essentially, a MIMOS model consists of a network of independent components that communicate through two types of channels: FIFO queues and registers. The FIFO queues are designed to support both non-blocking reads where no data is also considered an input, and non-blocking write operations. In contrast, a register is a single-capacity storage location that allows non-blocking read and write operations, overwriting its previous value with any new incoming data. Unlike FIFO queues, the contents of a register remain unchanged after a read operation. More precisely, a MIMOS model is a timed Kahn Process Network (KPN), where each node represents a periodic real-time task computing a mathematical function at a given rate. At the beginning of each period, the task reads its inputs; if the required inputs are available, it must compute the function before the period ends (ensured through schedulability analysis) and deliver the output by the end of the period or at a predetermined time point, such as the worst-case response time. If no inputs are available on the input channels when the period starts, essentially no computation is required. Thanks to the periodic timing behavior of reading, computation, and writing at each node, we can demonstrate that the non-blocking reading of inputs from both registers and FIFO channels is equivalent to a function over timed streams. Consequently, the MIMOS model operates under deterministic timed semantics.

Keynote 2: LLM for Program Specification Generation

Speaker: Shengchao Qin
(Huawei)

Abstract: Program verification often relies on human experts to write a significant amount of auxiliary specifications, such as function contracts and loop invariants, hindering its wider applications in real-world projects. To help alleviate this practical challenge, we present in this talk, AutoSpec, an automated approach to generating specifications with LLM for automated program verification. AutoSpec overcomes the shortcomings of existing work in specification versatility by synthesizing satisfiable and adequate specifications for proof completeness. It leverages the power of LLM, static analysis and program verification. We will also share some of our ongoing efforts aiming to further improve the performance of LLM-driven program specification generation.

Keynote 3: LTL Synthesis with a Few Hints

(Université Libre de Bruxelles)

Abstract: We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against a hostile environment. In this variant, the user provides the high-level LTL specification \(\varphi\) of the system to be designed, along with a set \(E\) of example executions that the solution must produce. Our synthesis algorithm operates in two phases. First, it generalizes the decisions made along the examples in \(E\), using tailored extensions of automata learning algorithms. This phase ensures that the user-provided examples in \(E\) are generalized while maintaining the realizability of \(\varphi\). Second, the algorithm converts the (typically) incomplete Mealy machine obtained from the learning phase into a complete Mealy machine that realizes \(\varphi\). The examples are used to guide the synthesis process.

We provide a completeness result, demonstrating that our procedure can learn any Mealy machine \(M\) that realizes \(\varphi\) with a small (polynomial-sized) set of examples. Furthermore, we show that our problem, which generalizes the classical LTL synthesis problem (i.e., when \(E = \emptyset\)), retains the same worst-case complexity. The additional cost of learning from \(E\) is polynomial in both the size of \(E\) and the size of a symbolic representation of solutions that realize \(\varphi\).

Additionally, we show how this framework can be applied when the reactive system to be synthesized interacts with an oblivious stochastic environment that can be sampled. In this case, we present an algorithm capable of producing complete examples from samples of the environment's behavior, optimized according to a reward function provided to the synthesis procedure. These examples are then incorporated into the synthesis procedure described above.

The proceedings are available here. Free access will be granted until 31 December 2024.

CONFERENCE TECHNICAL PROGRAM (Download Full Program)

All times are given in Beijing time (UTC+08:00)

Day 1 (November 26, 2024)

08:30 – 08:50
Registration
08:50 – 09:00
Opening
Session Chair: Nan Guan (City University of Hong Kong)
09:00 – 10:00
Keynote speaker 1
Wang Yi MIMOS: A New Paradigm and Tools for Embedded Systems Design and Updates
Session Chair: Nan Guan (City University of Hong Kong)
10:00 – 10:30
Coffee Break
10:30 – 12:10
Session I: Dependable CPS and concurrent systems
Session Chair: Mingsong Lv (Northeastern University, China)
10:30 – 10:55
Data-Dependent WAR Analysis for Efficient Task-Based Intermittent Computing
Juxin Niu, Yunlong Yu, Wei zhang and Nan Guan
10:55 – 11:20
Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects
Chao Wang, Peng Wu, Gustavo Petri, Qiaowen Jia, Youlin He, Yi Lv and Zhiming Liu
11:20 – 11:45
Cache Behavior Analysis with SP-relative Addressing for WCET Estimation
Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan and Lei Ju
11:45 – 12:10
Timing Analysis of Cause-Effect Chains for External Events with Finite Validity Intervals
Xiantong Luo, Haochun Liang, Yue Tang, Xu Jiang, Nan Guan and Wang Yi
12:10 – 13:30
Lunch
13:30 – 15:10
Session II: Proving and Verification
Session Chair: Chao Wang (Southwest University, China)
13:30 – 13:55
Formal Verification of RISC-V Processor Chisel Designs
Shidong Shen, Yicheng Liu, Lijun Zhang, Fu Song and Zhilin Wu
13:55 – 14:20
The Principle of Staking: Formal Verification of Staking Smart Contract
Zhongyun Zhang, Kundu Chen, Weiqi Guo and Wenbo Zhang
14:20 – 14:45
A Contract-based Framework for Formal Verification of Embedded Software
Xu Lu, Cong Tian, Bin Gu, Bin Yu, Chen Chen and Zhenhua Duan
14:45 – 15:10
Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness
Jiayi Lu, Shenghao Yuan, David Sanan and Yongwang Zhao
15:10 – 15:40
Coffee Break
15:40 – 16:55
Session III: Testing and Verification of Deep Learning Systems
Session Chair: Wei Zhang (Shandong University)
15:40 – 16:05
Runtime Verification of Neural-Symbolic Systems
Shaojun Deng, Wanwei Liu and Miaomiao Zhang
16:05 – 16:30
Eidos: Efficient, Imperceptible Adversarial 3D Point Clouds
Hanwei Zhang, Luo Cheng, Qisong He, Wei Huang, Renjue Li, Ronan Sicre, Xiaowei Huang, Holger Hermanns and Lijun Zhang
16:30 – 16:55
MILE: A Mutation Testing Framework of In-Context Learning Systems
Zeming Wei, Yihao Zhang and Meng Sun
17:00 – 20:00
Reception

Day 2 (November 27, 2024)

09:00 – 10:00
Keynote speaker 2
Shengchao Qin LLM for Program Specification Generation
Session Chair: Timothy Bourke (INRIA)
10:00 – 10:30
Coffee Break
10:30 – 12:10
Session IV: Program Analysis
Session Chair: Heqing Huang (City University of Hong Kong)
10:30 – 10:55
An Assertion-Based Logic for Local Reasoning about Probabilistic Programs
Huiling Wu, Anran Cui and Yuxin Deng
10:55 – 11:20
Extending Symbolic Heap to Support Shared Ownership
Jiyang Wu and Qinxiang Cao
11:20 – 11:45
Constraint Based Invariant Generation with Modular Operations
Yuchen Li, Hongfei Fu, Haowen Long and Guoqiang Li
11:45 – 12:10
The Design of Intelligent Temperature Control System of Smart House with MARS
Yihao Yin, Hao Wu, Shuling Wang, Xiong Xu, Fanjiang Xu and Naijun Zhan
12:10 – 13:30
Lunch
13:30 – 14:45
Session V: Formal language and LLMs
Session Chair: Naijun Zhan (Peking University, China)
13:30 – 13:55
A Derivative-based Membership Algorithm for Enhanced Regular Expressions
Mengxi Wang, Chunmei Dong, Weihao Su, Chengyao Peng and Haiming Chen
13:55 – 14:20
Enhancing Multi-modal Regular Expression Synthesis via Large Language Models and Semantic Manipulations of Sub-Expressions
Zipan Tang, Yixuan Yan, Rongchen Li, Hanze Dong, Haiming Chen and Hongyu Gao
14:20 – 14:45
Can Language Models Pretend Solvers? Logic Code Simulation with LLMs
Minyu Chen, Guoqiang Li, Ling-I Wu, Ruibang Liu, Yuxin Su, Xi Chang and Jianxin Xue
15:00 – 18:00
Tour
18:00 – 20:00
Banquet

Day 3 (November 28, 2024)

09:00 – 10:00
Keynote speaker 3
Jean-François Raskin LTL Synthesis with a Few Hints
Session Chair: Amir Goharshady (HKUST)
10:00 – 10:30
Coffee Break
10:30 – 11:45
Session VI: Anomaly Detection and Program Optimization
Session Chair: Yue Tang (Northeastern University)
10:30 – 10:55
NanoHook: An Efficient System Call Hooking Technique with One-Byte Invasive
Quan Hong, Jiaqi Li, Wen Zhang and Lidong Zhai
10:55 – 11:20
EDSLog: Efficient Log Anomaly Detection Method Based on Dataset Partitioning
Feng Liang and Jing Liu
11:20 – 11:45
Faster Lifetime-optimal Speculative Partial Redundancy Elimination for Goto-free Programs
Xuran Cai and Amir Goharshady
11:45 – 13:00
Closing & Lunch