verification

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
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
Preguss: It Analyzes, It Specifies, It Verifies
Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language …
PDF Cite DOI
Preguss: It Analyzes, It Specifies, It Verifies
On the Almost-Sure Termination of Probabilistic Counter Programs
This paper introduces $k$-d PCPs – the class of probabilistic counter programs with $k \in \mathbb{N}$ counter variables inducing …
PDF Cite DOI Artifact Evaluated
On the Almost-Sure Termination of Probabilistic Counter Programs
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
A Unified Framework for Quantitative Analysis of Probabilistic Programs
Verifying probabilistic programs requires reasoning about various probabilistic behaviors, e.g., random sampling, nondeterminism, and …
PDF Cite DOI
A Unified Framework for Quantitative Analysis of Probabilistic Programs
Parf: Adaptive Parameter Refining for Abstract Interpretation
Abstract interpretation is a key formal method for the static analysis of programs. The core challenge in applying abstract …
PDF Cite Code Slides Video DOI 2nd Prize@ChinaSoft'24
Parf: Adaptive Parameter Refining for Abstract Interpretation
Proving Functional Program Equivalence via Directed Lemma Synthesis
Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning …
PDF Cite DOI Artifact Evaluated
Proving Functional Program Equivalence via Directed Lemma Synthesis
MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification
Unlike classical computing, quantum program verification (QPV) is much more challenging due to the non-duplicability of quantum states …
PDF Cite Code DOI Artifact Evaluated
MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification
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