News

• 10/24: Paper on extended incorrectness logic is accepted at POPL’25.
• 07/24: Project FoxDec’s paper on verified x86-64 binary lifting is accepted at CCS’24.
• 06/24: Project libLISA’s paper on x86-64 instruction synthesis is accepted at OOPSLA’24.
• 04/24: Paper on disassembling decidability is accepted at TASE’24.
• 02/24: Paper on exceptional handling CFG is accepted at DIMVA’24.
• 04/23: Paper on binary intermediate representation for verified decompilation is accepted at TAP’23.
• 04/23: Paper on reachability analysis for low-level code is accepted at TAP’23.
• 02/23: Our PhD student Joshua Bockenek successfully defended his PhD thesis. Josh’s thesis made contributions to projects Luce and FoxDec.
• 09/22: Ghidra/P-Code formalization work has been accepted at VSTTE’22.
• 05/22: Our PhD student Xiaoxin (Cindy) An successfully defended her PhD thesis. Cindy’s thesis made contributions to projects DSV and Renee.
• 03/22: Project DSV’s x86-64 disassembly verifier is accepted at NFM’22.
• 02/22: Project Luce’s verified x86 binary lifting paper is accepted at PLDI 2022.
• 09/20: Project FoxDec’s C code decompilation paper has received the Best Paper Award at the SEFM 2020 conference!
• 05/20: Our MS student Abhijith Bharadwaj successfully defended his MS thesis. Abhijith’s thesis developed techniques for verifying concurrent x86-64 assembly code.
• 05/20: Our PhD student Xiaoxin (Cindy) An successfully defended her PhD thesis proposal. Cindy’s thesis is contributing to projects DSV and Renee.
• 02/20: Project Luce’s FMUC’20 paper has been nominated for the TACAS 2020 EASST Award for Systematic and Rigorous Engineering of Software & Systems!
• 02/20: Project Renee’s OCaml-PVS paper has been accepted at the NASA Formal Methods Symposium (NFM’20).
• 02/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.
• 09/19: Our PhD student Joshua Bockenek successfully defended his PhD thesis proposal. Josh’s thesis is contributing 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.