Research
The UV Research
Group
Group Meeting : M 12:25 - 1:45
Memory Model
Verification
Verification of today's complex cache coherence protocols for multiprocessor
systems against their intended memory models is a difficult, and not very
well understood task.My research aims at finding ways to a) define memory
models in a manner suitable to verification, and b) define abstractions
for complex protocol implementations to derive models better suited to verification.
Partial Order Reduction
Techniques
Traditional partial order reduction algorithms are aimed at process-based
system descriptions, and make heavy use of the interleaving concurrent process
idiom to define heuristics for the calculation of the ample set. Unfortunately,
these heuristics are not applicable to systems that do not use the process
notion in their descriptions. A widely used tool of this nature is the explicit
state enumeration based model checker Murphi. This work
aims at discovering new heuristics for ample set calculations that do not
depend on the process notion.
Course Work
Fall '99
Spring '00
Fall '00
Spring '02
CS 6962 : Theorem Proving
Spring '03
Teaching
Fall '99
CS 6100 : Foundations
of Computer Science - TA
Class Hours : T H 10:45 - 12:05
Office Hours : M F 9:30 - 10:30