News

07/25: Our postdoc, Ali Shokri has joined University of Houston’s Computer Science Department as an Assistant Professor.
02/25: Our PhD student, Md Syadus Sefat, defended his PhD thesis. Sefat’s thesis contributed to extended incorrectness logic. Sefat has joined AMD in Austin, TX.
01/25: Paper on formally verified binary pointer analysis is accepted at ICSE’25.
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: Paper on formalization of Ghidra/P-Code 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 paper on verifying x86-64 disassemblers is accepted at NFM’22.
02/22: Project Luce’s paper on verified x86 binary lifting is accepted at PLDI’22.
09/20: Project FoxDec’s paper on C code decompilation 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 paper on computing formal memory usage certificates has been nominated for the TACAS 2020 EASST Award for Systematic and Rigorous Engineering of Software & Systems!
02/20: Project Renee’s paper on validating OCaml-to-PVS translation has been accepted at NFM’20.
02/20: Project Luce’s paper on computing formal memory usage certificates has been awarded the TACAS 2020 Artifact Evaluation: Artifact Accepted badge.
12/19: Project Luce’s paper on computing formal memory usage certificates has been accepted at TACAS’20.
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.