5 papers
Prism: Symbolic Superoptimization of Tensor Programs
Mengdi Wu, Xiaoyu Jiang, Oded Padon +1
This paper presents Prism, the first symbolic superoptimizer for tensor programs. The key idea is sGraph, a symbolic, hierarchical representation that compactly encodes large class…
Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
Eden Frenkel, Kenneth L. McMillan, Oded Padon +1
We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines ru…
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
Raz Lotan, Neta Elad, Oded Padon +1
We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT sol…
Mirage: A Multi-Level Superoptimizer for Tensor Programs
Mengdi Wu, Xinhao Cheng, Shengyu Liu +7
We introduce Mirage, the first multi-level superoptimizer for tensor programs. A key idea in Mirage is Graphs, a uniform representation of tensor programs at the kernel, thread…
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
Takeshi Tsukada, Hiroshi Unno, Oded Padon +1
Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an i…