|
|
HCOS Members
Primary Investigators
|
File systems and storage, operating systems, security, networking, and software engineering.
|
|
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.
|
|
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.
|
|
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.
|
|
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)
|
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.
|
|
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.
|
|
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.
|
|
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)
|
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
|
|
Wenkai Tan
Formal methods and Monte Carlo-based model checking.
|
|
