3 papers
cs.FL2026
Harnessing Code Agents for Automatic Software Verification
Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel
Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous e…
cs.PL2026
Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
Shuanglong Kan, Sebastian Ertel
The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compil…
cs.FL2025
Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
Shuanglong Kan, Anthony W. Lin
Finite Automata (FAs) are fundamental components in the domains of programming languages. For instance, regular expressions, which are pivotal in languages such as JavaScript and P…