Binoy Ravindran
Binoy Ravindran
Professor & Bradley Senior Faculty Fellow · ECE · Virginia Tech
binoy@vt.edu · Bio · Scholar · DBLP · ORCID · ACM

Publications

2026

ATC
MBCheck: Practical Static Analysis Framework for Detecting Memory Ordering Violations under WMM
J. Shastri, B. Ravindran (ACM Artifacts Evaluated - Functional, Reproduced, Available)
Middleware
Rethinking Virtual Machine Monitors for Better Security in Clouds
A. K. M. F. Mehrab, R. Nikolaev, B. Ravindran
SCAM
Abstract Interpretation for Exception-Aware Function Summaries in Binaries
D. Engel, F. Verbeek, B. Ravindran
QRS
Adding Compilation Metadata To Binaries To Make Disassembly Decidable
D. Engel, F. Verbeek, P. Kumar, B. Ravindran
QRS
Sem86: A Full-System Emulator Without Hard-coded Semantics
J. Craaijo, F. Verbeek, B. Ravindran
ISMM
Stretch: A Fault-Driven DSM Runtime for Distributed Multithreaded Applications
E. D'Alessio, M. Husain, X. Wang, B. Ravindran
PLDI
Scalable Floating-Point Satisfiability via Staged Optimization
Y. Zhang, Z. Fu, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Available)
MIDDLEWARE
Hares: A Framework for Transparent and Cross-Architecture Enclave Offloading
A. Sundarasamy, X. Wang, C. Bilbao, B. Ravindran
ACM TACO
Stateful HW-SW Migration: An Architecture-agnostic Checkpointing-Rollback Toolchain
M. France-Pillois, Z. Huang, J. Yang, E. Horta, B. Ravindran, A. Barbalace
EuroLLVM
Adding Compilation Metadata To Binaries To Make Disassembly Decidable
D. Engel, F. Verbeek, P. Kumar, B. Ravindran

2025

SoCC
Scalable and Fault-Tolerant Storage and File System Services with Non-Blocking Synchronization for Private Clouds
M. Sung, R. Nikolaev, B. Ravindran
KISV/SOSP
reInstruct: Toward OS-aware CPU Microcode Reprogramming
Y. Wang, R. Nikolaev, B. Ravindran
ASPLOS
Stramash: A Fused-kernel Operating System for Cache-Coherent, Heterogeneous-ISA Platforms
T. Xing, C. Xiong, T. Wei, A. Sanchez, B. Ravindran, J. Balkind, A. Barbalace (ACM Artifacts Evaluated - Functional, Available)
ICSE
Formally Verified Binary-level Pointer Analysis
F. Verbeek, A. Shokri, D. Engel, B. Ravindran
POPL
On Extending Incorrectness Logic with Backwards Reasoning
F. Verbeek, M. Sefat, Z. Fu, B. Ravindran
FCCM
SmartNIC-Based Distributed Shared Memory
H. Ramesh, N. R. VSathish, E. Horta, A. Barbalace, B. Ravindran
TCC
HEXO: Offloading Long-Running Compute- and Memory-Intensive Workloads on Low-Cost, Low-Power Embedded Systems
P. Olivier, A. K. M. F. Mehrab, S. Errabelly, S. Lankes, M. L. Karaoui, R. Lyerly, S-H. Kim, A. Barbalace, B. Ravindran

2024

SYSTOR
Offloading Datacenter Jobs to RISC-V Hardware for Improved Performance and Power Efficiency
B. Heerekar, C. Philippidis, H-R. Chuang, P. Olivier, A. Barbalace, B. Ravindran
CCS
Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly
F. Verbeek, N. Naus, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Available)
CCS
Poster: Formally Verified Binary Lifting to P-Code
N. Naus, F. Verbeek, S. Atla, B. Ravindran
OOPSLA
libLISA: Instruction Discovery and Analysis on x86-64
J. Craaijo, F. Verbeek, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Reproduced, Available)
PLDI
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
R. Nikolaev, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Available)
ICDCS
Dapper: A Lightweight and Extensible Framework for Live Program State Rewriting
A. Bapat, J. Shastri, X. Wang, A. Sundarasamy, B. Ravindran
TASE
On the Decidability of Disassembling Binaries
D. Engel, F. Verbeek, B. Ravindran
MIDDLEWARE
sMVX: Multi-Variant Execution on Selected Code Paths
S. Yeoh, X. Wang, J-W. Jang, B. Ravindran
DIMVA
Exceptional Interprocedural Control Flow Graphs for x86-64 Binaries
J. Bockenek, F. Verbeek, B. Ravindran

2023

MIDDLEWARE
DynaCut: A Framework for Dynamic and Adaptive Program Customization
A. Mahurkar, X. Wang, H. Zhang, B. Ravindran
APSys
Understanding the Security of Linux eBPF Subsystem
M. Husain, X. Wang, B. Ravindran
TAP
BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of x86-64 Binaries
D. Engel, F. Verbeek, B. Ravindran
TAP
Low-level Reachability Analysis based on Formal Logic
N. Naus, F. Verbeek, M. Schoolderman, B. Ravindran
EuroSys
Aggregate VM: Why Reduce or Evict VM’s Resources When You Can Borrow Them From Other Nodes?
H. Chuang, K. Manaouil, T. Xing, A. Barbalace, P. Olivier, B. Heerekar, B. Ravindran

2022

VSTTE
A Formal Semantics for P-Code
N. Naus, F. Verbeek, B. Ravindran
MTD/CCS
Rave: A Modular and Extensible Framework for Program State Re-Randomization
C. Blackburn, X. Wang, B. Ravindran
SPAA
wCQ: A Fast Wait-Free Queue with Bounded Memory Usage
R. Nikolaev, B. Ravindran
VLDB
Scalable Byzantine Fault Tolerance via Partial Decentralization
B. Arun, B. Ravindran
NFM
DSV: Disassembly Soundness Validation without Assuming a Ground Truth
X. An, F. Verbeek, B. Ravindran
PLDI
Formally Verified Lifting of C-compiled x86-64 Binaries
F. Verbeek, J. Bockenek, Z. Fu, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Available)
ACM TOCS
H-Container: Enabling Heterogeneous-ISA Container Migration in Edge Computing
T. Xing, A. Barbalace, P. Olivier, M. Karaoui, W. Wang, B. Ravindran
SysTEX/ASPLOS
Transparent, Cross-ISA Enclave Offloading
X. Wang, C. Bilbao, B. Ravindran
EuroSys
Kite: Lightweight Critical Service Domains
A. Mehrab, R. Nikolaev, B. Ravindran (ACM Artifacts Evaluated - Functional, Reproduced, Available)
ASPLOS
Continuous Address Space Layout Re-Randomization for Linux Drivers
R. Nikolaev, H. Nadeem, C. Stone, B. Ravindran (ACM Artifacts Evaluated - Functional, Reproduced, Available)
PPoPP
Poster: wCQ: A Fast Wait-Free Queue with Bounded Memory Usage
R. Nikolaev, B. Ravindran
ACM TOCS
An OpenMP Runtime for Transparent Work Sharing Across Cache-Incoherent Heterogeneous Nodes
R. Lyerly, C. Bilbao, C. Min, C. Rossbach, B. Ravindran

2021

PLDI
Snapshot-Free, Transparent, and Robust Memory Reclamation for Lock-Free Data Structures
R. Nikolaev, B. Ravindran (ACM Artifacts Evaluated - Functional, Reusable, Available)
AFP
x86 Instruction Semantics and Basic Block Symbolic Execution
F. Verbeek, A. Bharadwaj, J. Bockenek, I. Roessle, T. Weerwag, B. Ravindran
IEEE TC
A Syscall-Level Binary-Compatible Unikernel
P. Olivier, H. Lefeuvre, D. Chiba, S. Lankes, C. Min, B. Ravindran
MIDDLEWARE
Xar-Trek: Run-time Execution Migration among FPGAs and Heterogeneous-ISA CPUs
E. Horta, H-R. Chuang, N. VSathish, C. Philippidis, A. Barbalace, P. Olivier, B. Ravindran (ACM Artifacts Evaluated - Functional, Available)
DISC
Brief Announcement: Crystalline: Fast and Memory Efficient Wait-Free Reclamation
R. Nikolaev, B. Ravindran
NFM
Verification of Functional Correctness of Code Diversification Techniques
J-W. Jang, F. Verbeek, B. Ravindran

2020

MIDDLEWARE
An OpenMP Runtime for Transparent Work Sharing Across Cache-Incoherent Heterogeneous Nodes
R. Lyerly, C. Min, C. Rossbach, B. Ravindran (ACM Artifacts Evaluated - Functional, Available)
SEFM
Sound C Code Decompilation for a Subset of x86-64 BinariesBest paper
F. Verbeek, P. Olivier, B. Ravindran
ESORICS
Dynamic and Secure Memory Transformation in Userspace
R. Lyerly, X. Wang, B. Ravindran
RAID
A Framework for Software Diversification with ISA Heterogeneity
X. Wang, S. Yeoh, R. Lyerly, P. Olivier, S-H. Kim, B. Ravindran
SYSTOR
Scaling Shared Memory Multiprocessing Applications in Non-cache-coherent Domains
H-R. Chuang, R. Lyerly, S. Lankes, B. Ravindran
NFM
A Validation Methodology for OCaml-to-PVS Translation
X. An, A. Tahat, B. Ravindran
EuroSec/EuroSys
Secure and Efficient In-process Monitor (and Library) Protection with Intel MPK
X. Wang, S. Yeoh, P. Olivier, B. Ravindran
SPMA/EuroSys
The Case for Intra-Unikernel Isolation
P. Olivier, A. Barbalace, B. Ravindran
ICDCS
DEX: Scaling Applications Beyond Machine Boundaries
S-H. Kim, H-R. Chuang, R. Lyerly, P. Olivier, C. Min, B. Ravindran
VEE
Edge Compute — the Case for Heterogeneous-ISA Container Migration
A. Barbalace, M. Karaoui, W. Wang, T. Xing, P. Olivier, B. Ravindran
VEE
LibrettOS: A Dynamically Adaptable Multiserver-Library OS
R. Nikolaev, M. Sung, B. Ravindran
VEE
Intra-Unikernel Isolation with Intel Memory Protection Keys
M. Sung, P. Olivier, S. Lankes, B. Ravindran
TACAS
Highly Automated Formal Proofs over Memory Usage of Assembly Code
F. Verbeek, J. Bockenek, B. Ravindran (TACAS Artifact Evaluation: Artifact Accepted)
PPoPP
Universal Wait-Free Memory Reclamation
R. Nikolaev, B. Ravindran (ACM Artifacts Evaluated - Functional, Available, Results Replicated)
IEEE TDSC
Taming the Contention in Consensus-based Distributed Systems
B. Arun, S. Peluso, R. Palmieri, G. Losa, B. Ravindran

2019

MICRO
Quantifying Memory Underutilization in HPC Systems and Using it to Improve Performance via Architecture Support
G. Panwar, Y. Pang, D. Zhang, M. Dahshan, N. Debardeleben, B. Ravindran, X. Jian
PLOS/SOSP
Rethinking Communication in Multiple-kernel OSes for New Shared Memory Interconnects
A. Barbalace, P. Olivier, B. Ravindran
MIDDLEWARE
SlimGuard: A Secure and Memory-Efficient Heap Allocator
B. Liu, P. Olivier, B. Ravindran (ACM Artifacts Evaluated - Functional, Available)
MIDDLEWARE
Generalized Consensus for Practical Fault Tolerance
M. Garg, S. Peluso, B. Arun, B. Ravindran
MEMOCODE
Work-in-Progress: Establishing a Refinement Relation between Binaries and Abstract Code
F. Verbeek, J. Bockenek, A. Bharadwaj, I. Roessle, B. Ravindran
SpISA/ITP
Symbolic Execution of x86 Assembly in Isabelle/HOL
F. Verbeek, A. Bharadwaj, J. Bockenek, I. Roessle, B. Ravindran
FMCAD
Scalable Translation Validation of Unverified Legacy OS Code
A. Tahat, S. Joshi, P. Goswami, B. Ravindran
PODC
Brief Announcement: Hyaline: Fast and Transparent Lock-Free Memory Reclamation
R. Nikolaev B. Ravindran
SafeComp
Formal Verification of Memory Preservation of x86-64 Binaries
J. A. Bockenek, F. Verbeek, P. Lammich, B. Ravindran
SYSTOR
Cross-ISA Execution of SIMD Regions for Improved Performance
Y. Pang, R. Lyerly, and B. Ravindran
HPDC
HEXO: Offloading HPC Compute-Intensive Workloads on Low-Cost, Low-Power Embedded Systems
P. Olivier, A. F. Mehrab, S. Lankes, M. Karaoui, R. Lyerly, B. Ravindran
ICDCS
ezBFT: Decentralizing Byzantine Fault-Tolerant State Machine Replication
B. Arun, S. Peluso, B. Ravindran
SFMA/EuroSys
The Multihype: Virtualizing Heterogeneous-ISA Architectures
P. Olivier, B. Ravindran, A. Barbalace
SFMA/EuroSys
A Framework to Secure Applications with ISA Heterogeneity
X. Wang, S. Yeoh, R. Lyerly, S-H. Kim, B. Ravindran
VEE
A Binary-Compatible UnikernelBest paper
P. Olivier, D. Chiba, S. Lankes, C. Min, B. Ravindran
CPP
Formally Verified Big Step Semantics out of x86-64 Binaries
I. Roessle, F. Verbeek, B. Ravindran
ACM TOS
Lerna: Parallelizing Dependent Loops Using Speculation
M. M. Saad, R. Palmieri, B. Ravindran
PMAM/PPoPP
libMPNode: An OpenMP Runtime For Parallel Processing Across Incoherent Domains
R. Lyerly, S-H. Kim, B. Ravindran
PPoPP
Poster: Scheduling HPC Workloads on Heterogenous-ISA Architectures
M. Karaoui, A. Carno, R. Lyerly, S-H. Kim, P. Olivier, C. Min, B. Ravindran
SYSTOR
Lerna: Parallelizing Dependent Loops Using SpeculationBest paper
M. Saad, R. Palmieri, B. Ravindran

Papers prior to 2019 are available on the group site.