Jianan Yao

26 papers A* 8Journal 15Unranked 2
YearRankTypeTitle / Venue / Authors
2026 J jnl
ExVerus: Verus Proof Repair via Counterexample Reasoning.
CoRR
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
2025 J jnl
A Neurosymbolic Approach to Natural Language Formalization and Verification.
CoRR
Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Marc Hudak, Dejan Jovanovic, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamaric, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao
2025 J jnl
AutoVerus: Automated Proof Generation for Rust Code.
Proc. ACM Program. Lang.
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
2025 — —
Automated Verification of Safety and Liveness Properties for Distributed Protocols
Jianan Yao
2025 A* conf
Quantum Virtual Machines.
OSDI
Runzhou Tao, Hongzheng Zhu, Jason Nieh, Jianan Yao, Ronghui Gu
2024 J jnl
A Robust and High Precision Algorithm for Elastic Scattering Problems from Cornered Domains.
J. Sci. Comput.
Jianan Yao, Baoling Xie, Jun Lai
2024 J jnl
AutoVerus: Automated Proof Generation for Rust Code.
CoRR
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
2024 J jnl
Detecting Buggy Contracts via Smart Testing.
CoRR
Sally Junsong Wang, Jianan Yao, Kexin Pei, Hideaki Takahashi, Junfeng Yang
2024 J jnl
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions.
Proc. ACM Program. Lang.
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh
2024 J jnl
Pinpointing Moisture: The Capacitive Detection for Standing Tree Health.
Sensors
Jianan Yao, Zonglin Zhen, Huadong Xu, Liming Zhao, Yuying Duan, Xuhui Guo
2023 J jnl
A robust and high precision algorithm for elastic scattering problems from cornered domains.
CoRR
Jianan Yao, Baoling Xie, Jun Lai
2023 J jnl
Leveraging Large Language Models for Automated Proof Synthesis in Rust.
CoRR
Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
2022 A* conf
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols.
OSDI
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh
2022 J jnl
Giallar: Push-Button Verification for the Qiskit Quantum Compiler.
CoRR
Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
2022 A* conf
Giallar: push-button verification for the qiskit Quantum compiler.
PLDI
Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
2021 A* conf
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols.
OSDI
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan
2021 A* conf
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware.
SOSP
Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, Ronghui Gu
2021 J jnl
Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version).
CoRR
Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu
2021 A* conf
Gleipnir: toward practical error analysis for Quantum programs.
PLDI
Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu
2021 J jnl
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts.
CoRR
Shaokai Lin, Xinyuan Sun, Jianan Yao, Ronghui Gu
2020 A* conf
CLN2INV: Learning Loop Invariants with Continuous Logic Networks.
ICLR
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana
2020 J jnl
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks.
CoRR
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
2020 A* conf
Learning nonlinear loop invariants with gated continuous logic networks.
PLDI
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
2019 — conf
A Three-Dimensional Quasi-static Ultrasound Strain Imaging System Using A 6-DoF Robotic Arm.
ICARM
Jianan Yao, Qinghua Huang, Xuelong Li
2019 J jnl
CLN2INV: Learning Loop Invariants with Continuous Logic Networks.
CoRR
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana
2018 — conf
News Recommendation and Filter Bubble.
CIKM Workshops
Jianan Yao, Alexander G. Hauptmann