.- MoXIchecker: An Extensible Model Checker for MoXI.
.- Towards Verifying Security Policies for Infinite-State Systems.
.- Deductive Verification of Sparse Sets in Why3.
.- PolySAT: Word-level Bit-vector Reasoning in Z3.
.- Proof-Producing Symbolic Execution for P4.
.- Statically Inferring Usage Bounds for Infrastructure as Code.
.- hax: Verifying Security-Critical Rust Software using Multiple Provers.