Much of computing now runs on hardware chosen for performance and energy-efficiency but harder to program and to trust — processors with different instruction sets, accelerators and programmable devices, and large bodies of legacy software that no one can fully vouch for.
The group focuses on the software layer underneath: operating systems, compilers, and runtimes that make such hardware usable, fast, and energy-efficient, together with formal methods for reasoning about low-level code.
Shepherded by Binoy Ravindran.
Our current focus
Verifying low-level software
This thrust is building a foundation for reasoning about binaries with no source code: machine-validated instruction semantics for x86-64, results on when disassembly is decidable at all, formally verified lifting of position-independent binaries — to symbolized assembly and to compiler IR — binary-level pointer analysis, and the program logics and satisfiability solvers that make such reasoning scale.
Systems for heterogeneous hardware
This thrust is building operating systems, compilers, and runtimes that let a single application run across machines with different instruction sets — and across CPUs, FPGAs, SmartNICs, and RISC-V — for better performance and energy-efficiency: fused kernels for cache-coherent heterogeneous-ISA platforms, transparent enclave and workload offloading, stateful CPU–FPGA migration, and distributed shared-memory systems.
Alongside these, the group works on a number of related problems — improving the security and reliability of existing software, safely modernizing legacy code, reasoning about concurrent programs, and developing new program-analysis and machine-learning techniques for reasoning about security properties at scale. This draws on the group's roots in concurrency, distributed systems, OS, and real-time computing.
We're recruiting
We have open PhD, postdoc, and research-faculty positions — with no teaching obligations — across two tracks: software engineering, formal methods & programming languages (program analysis, verification, verified compilation), and systems (OS, compilers, and runtimes for emerging heterogeneous hardware).
Prospective students and postdocs: email binoy@vt.edu with a CV. · Full details →
Recent news
Award — Jos Craaijo received the Best Presentation Award at QRS 2026 for "Sem86: A Full-System Emulator without Hard-Coded Semantics," with Freek Verbeek and Binoy Ravindran.
New paper — "Abstract Interpretation for Exception-Aware Function Summaries in Binaries" is accepted at SCAM 2026.
Former Research Assistant Professor Ruslan Nikolaev has been awarded an NSF CAREER grant.
Selected publications
Projects
The group builds a trust stack for low-level software — from validated instruction semantics (libLISA) through formally verified disassembly (FoxDec) to binary tooling — alongside the Popcorn Linux operating system for heterogeneous-ISA hardware.