2,246 papers · page 10 of 113
Angela W. Li, Konstantinos Mamouras
Tokenization (also known as scanning or lexing) is a computational task that has applications in the lexical analysis of programs during compilation and in data extraction and analysis for unstructured or semi-structured data (e.g., data represented using the JSON and CSV data fo…
Yihe Li, Ruijie Meng, Gregory J. Duck
Large Language Models (LLMs) have emerged as a promising alternative to traditional static program analysis methods, such as symbolic execution, offering the ability to reason over code directly without relying on theorem provers or SMT solvers. However, LLMs are also inherently …
Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey
We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates. Implementability asks whether a global protoco…
Zongjie Li, Daoyuan Wu, Shuai Wang, Zhendong Su
Large code models (LCMs), pre-trained on vast code corpora, have demonstrated remarkable performance across a wide array of code-related tasks. Supervised fine-tuning (SFT) plays a vital role in aligning these models with specific requirements and enhancing their performance in p…
Mingyi Li, Junmin Xiao, Siyan Chen, Hui Ma, Xi Chen, Peihua Bao, Liang Yuan, Guangming Tan
We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages within legacy code into semantically equivalent Domain-Specific Language (DSL) implementations. Targeting the efficiency bottlenecks of existing verified lifti…
Tianchi Li, Xin Zhang
We propose a neural-symbolic style of program analysis that systematically incorporates informal information in a Datalog program analysis. The analysis is converted into a probabilistic analysis by attaching probabilities to its rules. And its output becomes a ranking of possibl…
Shangyu Li, Zhaoyang Zhang, Sizhe Zhong, Diyu Zhou, Jiasi Shen
The advances in modern storage technologies necessitate the development of new input/output (I/O) APIs to maximize their performance benefits. However, migrating existing software to use different APIs poses significant challenges due to mismatches in computational models and com…
Qihao Lian, Di Wang
Rust has become a popular system programming language that strikes a balance between memory safety and performance. Rust’s type system ensures the safety of low-level memory controls; however, a well-typed Rust program is not guaranteed to enjoy high performance. This article stu…
Zixi Liu, Yang Feng, Yunbo Ni, Shaohua Li, Xizhe Yin, Qingkai Shi, Baowen Xu, Zhendong Su
Rust is gaining popularity for its well-known memory safety guarantees and high performance, distinguishing it from C/C++ and JVM-based languages. Its compiler, rustc, enforces these guarantees through specialized mechanisms such as trait solving, borrow checking, and specific op…
Lang Liu, Farzaneh Derakhshan, Limin Jia, Gabriel A. Moreno, Mark Klein
Given the high cost of formal verification, a large system may include differently analyzed components: a few are fully verified, and the rest are tested. Currently, there is no reasoning system that can soundly compose these heterogeneous analyses and derive the overall formal g…
Shuyang Liu, Doug Lea, Jens Palsberg
A predictive analysis takes an execution trace as input and discovers concurrency bugs without accessing the program source code. A sound predictive analysis reports no false positives, which sounds like a property that can be defined easily, but which has been defined in many di…
Tianyi Liu, Yi Li, Yiyu Zhang, Zhuangda Wang, Rongxin Wu, Xuandong Li, Zhiqiang Zuo
Despite extensive in-house testing, bugs often escape to deployed software. Whenever a failure occurs in production software, it is desirable to collect as much execution information as possible so as to help developers reproduce, diagnose and fix the bug. To reconcile the tensio…
Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, Yu Feng
Zero-knowledge proof (ZKP) applications require translating high-level programs into arithmetic circuits—a process that demands both correctness and efficiency. While recent DSLs improve usability, they often yield suboptimal circuits, and hand-optimized implementations remain di…
Andreas Lööw
Despite numerous previous formalisation projects targeting Verilog, the semantics of Verilog defined by the Verilog standard -- Verilog's simulation semantics -- has thus far eluded definitive mathematical formalisation. Previous projects on formalising the semantics have made go…
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, Philippa Gardner
Multiple successful compositional symbolic execution (CSE) tools and platforms exploit separation logic (SL) for compositional verification and/or incorrectness separation logic (ISL) for compositional bug-finding, including VeriFast, Viper, Gillian, CN, and Infer-Pulse. Previous…
Sirui Lu, Rastislav Bodík
Modern optimizing compilers generate efficient code but rarely achieve theoretical optimality, often necessitating manual fine-tuning. This is especially the case for processors with vector instructions, which can grow the instruction set by an order of magnitude. Super-optimizer…
Matthew Lutze, Philipp Schuster, Jonathan Immanuel Brachthäuser
Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general forma…
Chenyang Ma, Wei Song, Jeff Huang
Fuzzing is an effective technique to detect vulnerabilities in smart contracts. The challenge of smart contract fuzzing lies in the statefulness of contracts, which indicates that certain vulnerabilities can only be manifested in specific contract states. State-of-the-art fuzzers…
Zhongkui Ma, Zihan Wang, Guangdong Bai
The wide adoption of deep learning in safety-critical domains has driven the need for formally verifying the robustness of neural networks. A critical challenge in this endeavor lies in addressing the inherent non-linearity of activation functions. The convex hull of the activati…
Magnus Madsen, Ondrej Lhoták
We present a comprehensive overview of the Datalog facilities in the Flix programming language. We show how programmers can write functions implemented as Datalog programs and we demonstrate how to build modular and reusable families of Datalog programs using first-class Datalog …