HCOS Members

Primary Investigators

Picture of Erez Zadok

Erez Zadok (Lead PI)

File systems and storage, operating systems, security, networking, and software engineering.
Picture of Radu Grosu

Radu Grosu

Model-based design and verification of embedded software systems; Model checking, abstract interpretation, logic and automata theory, type theory; Computational models in systems biology; Applied formal methods, software and systems engineering.
Picture of Yanhong Annie Liu

Yanhong A. Liu

Programming languages, compilers, and software systems; Program analysis and transformation techniques for incremental computation and for parallel and concurrent computation; Optimizing compilers, language-based interactive systems, real-time and reactive systems, algorithm design, program development, and software maintenance; Supporting tools and user interfaces that allow convenient and efficient implementation of program analyses and transformations and facilitate their applications.
Picture of Scott Smolka

Scott A. Smolka

Computer-aided verification and validation of computer systems, including concurrent and distributed systems; security, network and wireless protocols; software systems; biological systems; safety-critical and embedded systems. Computational complexity and algorithmica of verification.
Picture of Scott Stoller

Scott Stoller

Methods and tools for design, analysis, testing, and verification of software, especially software for concurrent systems and distributed systems, including specialized techniques for ensuring fault-tolerance and security; program optimization and incremental computation.

Graduate Students (Present)

Picture of Daniel J. Dean

Daniel J. Dean

Tools for visualization of compiler intermediate representations. Designed, developed and maintains a visualizer for GCC's GIMPLE intermediate representation. Using Callanan's GCC plug-in architecture, designed and implemented a compiler-assisted execution tracer.
Picture of Abhinav Duggal

Abhinav Duggal

Studying concurrency issues and automated race detection in Linux kernel code using Seyster's specialized GCC plug-in instrumentation. Implemented a performance-optimized in-kernel logging framework suited to logging fine-grained concurrent memory operations.

Michael Gorbovitski

Refine a prototype implementation of the invariant-driven transformation language and framework for Python so that it is easy to support instrumentation for invariants checking and monitoring of C programs. Evaluate the prototype by experimenting with transformations for role-based access control and other applications.
Picture of Xiaowan Huang

Xiaowan Huang

Using the plug-in architecture developed by Callanan, designed, implemented, and evaluated an interpreter for the GIMPLE internal representation of control-flow graphs in the GCC compiler collection. Such an interpreter is a key component of software model checker for GCC.
Picture of Justin Seyster

Justin Seyster

Visualization tools for structural and behavioral analysis of software. Currently maintains a memory profiling framework for multi-process, multi-threaded applications and a client tool that visualizes memory allocation and use.

Graduate Students (Past)

Picture of Sean Callanan

Sean Callanan

Compiler-assisted instrumentation tools to help programmers understand, debug, and verify the correctness of complex systems. Developed a system for pluggable code transformations for GCC and a variety of applications, and designed and prototyped a memory usage profiling tool for unmodified binaries.

Dr. Callanan is currently working at Apple as a debugging tools engineer.

Sumit Jain

Abhishek Rai

Picture of Wenkai Tan

Wenkai Tan

Formal methods and Monte Carlo-based model checking.
  • Sumit Jain
  • Abhishek Rai