...
This talk will focus on MemSAT, a recent application of Kodkod to debugging and reasoning about memory models. MemSAT takes as input an axiomatic specification of a memory model and a multi-threaded test program containing assertions. The test program and the assertions comprise a litmus test for the memory model
| Wiki Markup |
|---|
{html}—{html} |
...
Emina Torlak received her Ph.D. (2009), M.Eng. (2004) and B.Sc. (2003) in Computer Science from MIT. Her primary research interests are in the development and application of scalable tools for lightweight formal methods, program analysis, debugging and testing. She designed and implemented Kodkod, a relational constraint solver with numerous applications to design analysis, code checking, test-case generation, and declarative configuration. Emina is currently a Senior Computer Scientist at LogicBlox, where she is working on specification-based testing of online analytical processing applications. Prior to joining LogicBlox, she was a Research Staff Member at the IBM T. J. Watson Research Center, where her work focused on the analysis of weak memory models, symbolic debugging, and resource leak detection.
| Attachments | ||
|---|---|---|
|