7,482 papers · page 15 of 375
Haoran Xu, Fredrik Kjolstad
Building a high-performance JIT-capable VM for a dynamic language has traditionally required a tremendous amount of time, money, and expertise. We present Deegen, a meta-compiler that allows users to generate a high-performance JIT-capable VM for their own language at an engineer…
Han Xu, Zachary Kincaid, Ratul Mahajan, David Walker
Relational NetKAT (RN) is a new specification language for network change validation. Engineers use RN to specify intended changes by providing a trace relation R, which maps existing packet traces in the pre-change network to intended packet traces in the post-change network. Th…
Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li, Conrad Watt
Neural Theorem Proving (NTP) employs Large Language Models (LLMs) to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using natural languages, the transition to mechanized formal theorem proving present…
Gengyang Xu, Dongwei Xiao, Yiteng Peng, Shuai Wang
An embodied agent is an intelligent entity that interacts with its environment through a physical body. Currently, the evaluation of embodied agents primarily relies on two paradigms: (1) manually annotated Visual Question Answering (VQA) pairs and (2) high-level task completion …
Jin Xu, Miaomiao Zhang, Bowen Du
Complete formal verification of neural networks is crucial for their deployment in safety-critical domains. A key bottleneck stems from encoding complexity: traditional methods assign one binary variable per unstable ReLU neuron. We propose the Sign-Absolute Reformulation Theory …
Jianhao Xu, Kunbo Zhang, Mathias Payer, Kangjie Lu, Bing Mao
Compilers are expected to generate optimized code, but they sometimes introduce pessimizations, quality-degrading redundant instructions. These bugs not only incur performance overhead but also, critically, expand the attack surface by introducing unexpected side effects (e.g., r…
Xu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira
Type inference is essential for programming languages, yet complete and global inference quickly becomes undecidable in the presence of rich type systems like System F. Pierce and Turner proposed local type inference (LTI) as a scalable, partially annotated alternative by relying…
Zhen Yan, Yuanliang Chen, Fuchen Ma, Zehong Yu, Dalong Shi, Yu Jiang
Verilog simulators and synthesizers play a critical role in chip design and verification. However, due to the complexity of simulation and synthesis processes, they easily introduce various types of bugs. Among them, Behavioral Deviation Bugs (BDBs) are particularly severe, as th…
Tengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan, Jingyu Ke, Shiyang Wu
In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not …
Ganxiang Yang, Paige Raun, Runzhou Tao, Ronghui Gu
Optimizing a quantum circuit is hard because it requires exploring a vast space of functionally equivalent circuits, produced by applying local circuit rewrites such as gate cancellation and commutation. Each additional rewrite can exponentially expand the space of equivalent cir…
Zhixuan Yang, Nicolas Wu
This paper studies the design of programming languages with handlers of higher-order effectful operations – effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative po…
Zhentao Ye, Ruyi Ji, Yingfei Xiong, Xin Zhang
Syntax-guided program synthesis relies on domain-specific languages (DSLs) to constrain the search space and improve efficiency. However, manually designing optimal DSLs is challenging and often results in suboptimal performance. In this paper, we propose AMaze, a novel framework…
Zijian Yi, Cheng Ding, August Shi, Milos Gligoric
Just-in-time (JIT) compilers are key components for many popular programming languages with managed runtimes (e.g., Java and JavaScript). JIT compilers perform optimizations and generate native code at runtime based on dynamic profiling data, to improve the execution performance …
Mingsheng Ying, Zhicheng Zhang
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively def…
Nazanin Yousefian, Kasra Jamshidi, Keval Vora, Anders Miltner
Graph pattern mining is important for analyzing graph data. Graph mining systems typically require answering pattern matching queries, which involve solving the NP-complete subgraph isomorphism problem. To address this, domain experts often develop custom pattern matching query o…
Nengkun Yu, Jens Palsberg, Thomas Reps
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient—even for quantum circuits, a deliberately restricted model that lacks classical control, but still un…
Charles Yuan
Quantum algorithms for computational linear algebra promise up to exponential speedups for applications such as simulation and regression, making them prime candidates for hardware realization. But these algorithms execute in a model that cannot efficiently store matrices in memo…
Hengchen Yuan, Jiefang Lin, August Shi
Regression testing is an essential part of software development to ensure high-quality software; but the presence of flaky tests makes the testing outcomes unreliable. It is essential to proactively detect flaky tests, so developers are aware of them early on and can react approp…
Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, Alexander K. Lew
Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it is crucial that expensive intermediate results are shared across these many evaluations, rather tha…
Robert Zhang, Eric Hayden Campbell, Dixin Tang, Isil Dillig
Predicate pushdown is a long-standing performance optimization that filters data as early as possible in a computational workflow. In modern data pipelines, this transformation is especially important because much of the computation occurs inside user-defined functions (UDFs) wri…