4 papers
Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version)
Dinghong Zhong, Alexander Bai, Mikail Khan +1
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…
Verifying Probabilistic Programs in Rust
Alexander Y. Bai, Joseph Tassarotti
Recent work has developed many techniques for formally verifying probabilistic programs. However, existing verification frameworks for probabilistic programs are restricted to idea…
Tunable Automation in Automated Program Verification
Alexander Y. Bai, Chris Hawblitzel, Andrea Lattuada
Automated verification tools based on SMT solvers have made significant progress in verifying complex software systems. However, these tools face a fundamental tension between auto…
Debugging WebAssembly? Put some Whamm on it!
Elizabeth Gilbert, Matthew Schneider, Zixi An +5
Debugging and monitoring programs are integral to engineering and deploying software. Dynamic analyses monitor applications through source code or IR injection, machine code or byt…