[UVM logo]

Christian Skalka, Research Project Details

Home | Research Interests | Research Projects | Teaching | Publications | Presentations

Trace and Flow Effects

Trace effects are a form of type-and-effect that statically approximate run-time event traces, where events are records of some program action (similar to log entries). A principal novelty of trace effects is that they express temporal ordering of events. We have established a foundational theory of trace effects, which shows how artifacts of type reconstruction can be combined with model checking techniques to provide a powerful program logic based on temporal logic assertions. Our type theory is scalable; we have shown that trace effects apply to object-orientation and other advanced language features as found in e.g. Java.

Flow effects are similar to trace effects, but events in the flow effect model are dataflow constraints; for example, if a function f is applied to 5, then an event recording the flow of an integer type into the domain type of f is recorded. Because flow effects also account for temporal ordering, the analysis is context sensitive.

This is joint work with Scott Smith, Paritosh Shroff, and David Van Horn.

Christian Skalka's work on this project was supported by a DoD DEPSCoR grant through the Air Force Office of Scientific Research.

Valid XHTML Valid CSS