2,246 papers · page 2 of 113
Jan Grünke, Thomas Haas, Roland Meyer
We present a model checking approach for axiomatic memory consistency models written in the language CAT. It can prove properties of single memory models like the monotonicity of barriers, and also compare models like TSO and ARM8. To achieve this expressiveness, our approach sup…
Kevin Guan, Pengyue Jiang, Milos Gligoric, Owolabi Legunsen
Inline tests validate single program statements and were shown to find single-statement bugs or kill mutants that unit tests miss. Inline tests complement unit tests by enabling testing at a finer program granularity level than methods. So, inline tests can more easily find fault…
Zhichao Guan, Tailai Yu, Di Wang, Zhenjiang Hu
Syntactic sugar enhances the usability of a core language by providing intuitive syntax in a surface language; however, its interaction with the core-language type checker often results in error messages that are unclear to surface programmers. Existing techniques, such as type l…
Tobias Gürtler, Benjamin Lucien Kaminski
Probabilistic programming languages (PPLs) are an expressive and intuitive means of representing complex probability distributions. In that realm, languages like Dice target an important class of probabilistic programs: those whose probability distributions are discrete. Discrete…
Haotian Han, Zihang Zhong, Qingan Li, Jingling Xue, Mengting Yuan
As build systems and their scripts grow in size and complexity, detecting bugs in build configurations becomes increasingly challenging due to the rich functionality and weak typing of build scripting languages. This paper introduces CM ake S onar , the first static approach to p…
Mike He, Ankush Desai, Jagarapu Aishwarya, Doug Terry, Sharad Malik, Aarti Gupta
Reasoning about the correctness of distributed systems is a significant challenge, with precise correctness specifications serving as an essential prerequisite to verification. However, identifying and formulating specifications remains a major hurdle for developers in practice. …
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
Statically enforcing safe resource management is challenging due to tensions between flexible lifetime dis-ciplines and expressive sharing patterns. Region-based systems offer lexically scoped regions under a stack discipline, wherein resources are managed in bulk. In many such s…
Yuxuan He, Ruilin Jiang, He Zhang, Qingkai Shi, Huaxun Huang, Rongxin Wu
Sparse Value-Flow Analysis (SVFA) is essential for detecting software bugs such as null pointer dereference and memory leak. However, SVFA heavily relies on path-sensitive pointer analysis, which faces significant scalability challenges when analyzing industrial-scale projects, n…
Jonas Kastberg Hinrichsen, Iwan Quémerais, Lars Birkedal
Mixed choice multiparty message passing is an expressive concurrency programming paradigm where components use non-determinism to choose between concurrent options for sending and receiving messages. This flexibility makes it possible to program advanced algorithms, such as leade…
Shan Jiang, Chenguang Zhu, Sarfraz Khurshid
JavaScript obfuscators are widely deployed to protect intellectual property and resist reverse engineering, yet their correctness has been largely overlooked compared to performance and resilience. Existing evaluations typically measure resistance to deobfuscation, leaving the cr…
Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer
Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic policies that ensure a player following them will not lose. Each deterministic, fi…
Minsu Kim, Sunbeom So, Hakjoo Oh
We present Prunario , a novel technique for effectively testing autonomous driving systems (ADS). Ensuring the safety of ADS is critical, as their failures can lead to severe casualties. While ADS testing methods have advanced in recent years, they remain unsatisfactory in genera…
Mickaël Laurent, Jan Vitek
In this paper, we formalize a type system based on set-theoretic types for dynamic languages that support both functional and imperative programming paradigms. We adapt prior work in the typing of overloaded and generic functions to support an impure λ -calculus, focusing on impe…
Yunjeong Lee, Gokul Rajiv, Ilya Sergey
Context-free grammars (CFGs) are the de-facto formalism for declaratively describing concrete syntax for programming languages and generating parsers. One of the major challenges in defining a desired syntax is ruling out all possible ambiguities in the CFG productions that deter…
Nicholas V. Lewchenko, Kunha Kim, Bor-Yuh Evan Chang, Gowtham Kaki
Decidable automation is a key feature of program verification tools, which makes them easier for non-expert developers to use and understand. Unfortunately, decidable fragments of logic are very restrictive, and not ideal for the expression of idiomatic programs. The decidable Ex…
Wei Li, Wenyao Chen, Jingling Xue
Rust combines high performance with strong memory safety through strict ownership and borrowing rules. However, its unsafe mode reintroduces vulnerabilities by allowing raw-pointer manipulation, a major source of memory-safety bugs. Existing whole-program analyses for Rust often …
Ka Wing Li, Maite Kramarz, Ningning Xie, Jeremy Yallop
Multi-stage programming (MSP) languages such as MetaML have subtle semantics, in which familiar properties often fail to hold and hazardous interactions with other language features such as state or polymorphism abound. The ongoing incorporation of MSP features into general purpo…
Zhen Li, Shenghan Liu, Qiuping Yi, Pengbo Du, Hongliang Liang
Software vulnerabilities pose severe security threats, highlighting the need for effective automated detection. Directed hybrid fuzzing, which combines the rapid exploration of fuzz testing with the precise constraint solving of symbolic execution, has made notable advancements i…
Yanqi Li, Hongliang Liang, Rui Yao, Yang Zhang, Dong Liu, Lei Wang, Qiuping Yi
Real-time systems must simultaneously deliver predictable timing, fault isolation, and memory safety, yet current operating systems expose only low-level primitives that force developers to manually balance concurrency, isolation, and performance. This paper presents LARTS, a lan…
Haoran Lin, Zhenyu Yan, Xin Zhang
Interactive Bayesian program analysis enhances static analysis by modeling derivations as probabilistic dependencies, enabling ranking alarms by calculated confidences, proposing highly likely alarms for user inspection, and updating confidences with inspection results. Existing …