2

A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language …
Cite Code Dataset
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
A Brief History of Formal Methods in China
The development of formal methods (FM) in China dates back to the early 1950s, when several logicians shifted their research focus from …
Cite DOI
A Brief History of Formal Methods in China
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot under Hardware Supply-chain Attacks
Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. In this paper, we …
PDF Cite
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot under Hardware Supply-chain Attacks
AdaptDQC: Adaptive Distributed Quantum Computing with Quantitative Performance Analysis
We present AdaptDQC, an adaptive compiler framework for optimizing distributed quantum computing (DQC) under diverse performance …
Cite
AdaptDQC: Adaptive Distributed Quantum Computing with Quantitative Performance Analysis
Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis
We launch Parf – a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. …
PDF Cite DOI 2nd Prize@ChinaSoft'24
Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis
Fast-USYN: Fast Synthesis from Unitary Matrices to High-Quality Quantum Circuits
Current quantum programs are usually represented as quantum circuits, including various quantum gates. If the program contains gates …
PDF Cite
Fast-USYN: Fast Synthesis from Unitary Matrices to High-Quality Quantum Circuits
A Privacy Policy Text Compliance Reasoning Framework with Large Language Models for Healthcare Services
The advancement of AI-generated content (AIGC) drives the diversification of healthcare services, resulting in increased private …
PDF Cite
A Privacy Policy Text Compliance Reasoning Framework with Large Language Models for Healthcare Services
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring …
PDF Cite Artifact Evaluated
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lower Bounds for Possibly Divergent Probabilistic Programs
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to …
PDF Cite Poster Slides DOI
Lower Bounds for Possibly Divergent Probabilistic Programs
Encoding Inductive Invariants as Barrier Certificates
We present the invariant barrier-certificate condition that witnesses unbounded-time safety of differential dynamical systems. The …
PDF Cite Code Slides DOI
Encoding Inductive Invariants as Barrier Certificates