Guannan Wei

Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots

Concolic execution is a variant of symbolic execution that runs a program simultaneously with concrete and symbolic inputs. It records the symbolic constraints encountered along a concrete execution path, then solves those constraints to generate inputs that explore new paths. Ex...

Neurosymbolic code auditing

Code auditing examines whether an implementation satisfies target properties such as reliability, security, performance, and design intent. Classical static analysis provides rigorous foundations for automated auditing, but it remains difficult to apply broadly in real-world soft...