News

• 4/23: Paper on binary intermediate representation for formally verified decompilation is accepted at TAP’23.
• 4/23: Paper on reachability analysis for low-level code is conditionally accepted at TAP’23.
• 2/23: Our PhD student Joshua Bockenek successfully defended his PhD thesis! Josh’s thesis made contributions to projects Luce and FoxDec.
• 9/22: Ghidra/P-Code formalization work has been accepted at VSTTE’22.
• 5/22: Our PhD student Xiaoxin (Cindy) An successfully defended her PhD thesis! Cindy’s thesis made contributions to projects DSV and Renee.
• 3/22: Project DSV’s x86-64 disassembly verifier is accepted at NFM’22!
• 2/22: Project Luce’s verified x86 binary lifting paper has been conditionally accepted at PLDI 2022!
• 9/20: Project FoxDec’s C code decompilation paper has received the Best Paper Award at the SEFM 2020 conference!
• 5/20: Our MS student Abhijith Bharadwaj successfully defended his MS thesis! Abhijith’s thesis developed techniques for verifying concurrent x86-64 assembly code.
• 2/20: :Project Luce’s FMUC’20 paper has been nominated for the TACAS 2020 EASST Award for Systematic and Rigorous Engineering of Software & Systems!
• 2/20: Project Renee’s OCaml-PVS paper has been accepted at the NASA Formal Methods Symposium (NFM’20)!
• 2/20: Project Luce’s FMUC’20 paper has been awarded the TACAS 2020 Artifact Evaluation: Artifact Accepted badge!
• 12/19: Project Luce’s FMUC’20 paper has been accepted at TACAS 2020!
• 9/19: Our PhD student Joshua Bockenek successfully defended his PhD dissertation proposal! Josh’s thesis is making contributions to projects Luce and FoxDec.
• 12/17: Our MS student Joshua Bockenek successfully defended his MS thesis! Josh’s thesis developed extensions to Isabelle/UTP for modular verification.