Today’s quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to manage and still miss long-distance transformations. We present QSymb, a framework for synthesizing compact and expressive quantum-circuit rewrite rules with formal guarantees. We formalize symbolic rewrite rules in which a symbolic gate represents infinitely many subcircuits. We then define canonical symbolic rules of the form L; S = S; R and prove that they constitute a compact generative core from which general symbolic rules can be derived. On top of this formal foundation, given a gate set, QSymb synthesizes (1) a small, non-derivable concrete rule set that is complete up to chosen size and qubit bounds, and (2) a small but expressive canonical symbolic rule set that captures transformations beyond finite or monomial-only patterns. We further present rule anchoring to derive optimization-effective rules from canonical symbolic rules. Together, these results provide both expressiveness and guarantees: soundness of synthesized rules via validation, non-derivability, and bounded completeness. On the IBM-Eagle gate set, QSymb strictly outperforms state-of-the-art rewrite-based optimizers (Qiskit, Guoq, Quartz, TKET, and Queso) in two-qubit-gate reduction on 90%, 67%, 82%, 85%, and 83% of standard quantum algorithm benchmarks, respectively; on Nam gate set, the corresponding rates are 88%, 74%, 81%, 86%, and 82.9%. It achieves final average two-qubit-gate reductions of 27.44% and 29.95%, respectively.
@article{qsymb,author={Qiang, Wei and Gu, Ronghui},title={Synthesis of Compact and Expressive Quantum-Circuit Optimizations},journal={Proc. ACM Program. Lang.},year={2026},issue_date={October 2026},publisher={Association for Computing Machinery},address={New York, NY, USA},volume={10},number={OOPSLA2},articleno={318},numpages={28},month=oct,url={https://doi.org/10.1145/3839450},doi={10.1145/3839450},keywords={equality saturation, quantum circuit optimization, rewrite-rule inference, symbolic rewriting},}
System software is often complex and hides exploitable security vulnerabilities. Formal verification promises bug-free software but comes with a prohibitive proof cost. We present Spoq2, the first verification framework to highly automate security verification of unmodified system software. Spoq2 is based on the observation that many security properties, such as noninterference, can be reduced to establishing inductive invariants on individual transitions of a transition system that models system software. However, directly verifying such invariants for real system code overwhelms existing SMT solvers. Spoq2 makes this possible by automatically reducing verification complexity. It decomposes transitions into individual execution paths, extends cone-of-influence analysis to the individual transition level, and eliminates irrelevant machine states, clauses, and control-flow paths before invoking the SMT solver. Spoq2 further optimizes how pointer operations are modeled and verified through pointer abstractions that eliminate expensive bit-wise operations from SMT queries. We demonstrate the effectiveness of Spoq2 by verifying security properties of four unmodified, real-world system codebases with minimal manual effort.
@inproceedings{spoq2,author={Yang, Ganxiang and Qiang, Wei and Rong, Yi and Li, Xuheng and Yu, Fanqi and Gu, Ronghui and Nieh, Jason},title={Spoq2: Highly Automated Verification of Security Properties for Unmodified System Software},booktitle={Proceedings of the 31st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2026)},year={2026},address={Pittsburgh, PA},publisher={ACM},month=mar,}
System software is often large and complex, resulting in many vulnerabilities that can potentially be exploited to compromise the security of a system. Formal verification offers a potential solution to creating bug-free software, but a key impediment to its adoption remains proof cost. We present Spoq, a highly automated verification framework to construct machine-checkable proofs in Coq for system software with much less proof cost. Spoq introduces a novel program structure reconstruction technique to leverage LLVM to translate C code into Coq, supporting full C semantics, including C macros, inline assembly, and compiler directives, so that source code no longer has to be manually modified to be verified. Spoq leverages a layering proof strategy and introduces novel Coq tactics and transformation rules to automatically generate layer specifications and refinement proofs to simplify verification of concurrent system software. Spoq also supports easy integration of manually written layer specifications and refinement proofs. We use Spoq to verify a multiprocessor KVM hypervisor implementation. Verification using Spoq required 70% less proof effort than the manually written specifications and proofs to verify an older implementation. Furthermore, the proofs using Spoq hold for the unmodified implementation that is directly compiled and executed.
@inproceedings{spoq,author={Li, Xupeng and Li, Xuheng and Qiang, Wei and Gu, Ronghui and Nieh, Jason},title={Spoq: Scaling Machine-Checkable Systems Verification in Coq},booktitle={17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)},year={2023},isbn={978-1-939133-34-2},address={Boston, MA},pages={851--869},url={https://www.usenix.org/conference/osdi23/presentation/li-xupeng},publisher={USENIX Association},month=jul,}