Goal

To improve performance, virtually all modern processors (e.g. Power, SPARC, Intel, ARM) support relaxed memory models. Unfortunately, programming these relaxed models is difficult and error-prone, yet highly desirable. In this project, we develop powerful automated synthesis and verification techniques which ensure that modern chips are exploited correctly and efficiently. The techniques are based on model checking, abstract interpretation and dynamic analysis.

Publications

Automatic Verification of RMA Programs via Abstraction Extrapolation
Baumann C., Dan A., Meshman Y., Hoefler T., Vechev M.
VMCAI'18: 19th International Conference on Verification, Model Checking, and Abstract Interpretation
[pdf] [slides]
Modeling and Analysis of Remote Memory Access Programming
Dan A., Lam P., Hoefler T., Vechev M.
OOPSLA'16: Object-Oriented Programming, Systems, Languages and Applications
[pdf][video]
Pattern-based Synthesis of Synchronization for the C++ Memory Model.
Meshman Y., Rinetzky N., and Yahav E.
FMCAD'15: Formal Methods in Computer-Aided Design
[pdf][slides][ virtual machine ][site][online tool]
Effective Abstractions for Verification under Relaxed Memory Models
Dan A., Meshman Y., Vechev M., Yahav E.
VMCAI'15: 16th International Conference on Verification, Model Checking, and Abstract Interpretation
[pdf] [slides]
Synthesis of Memory Fences via Refinement Propagation
Dan A., Meshman Y., Vechev M., Yahav E.
SAS'14: 21th Static Analysis Symposium
[pdf] [slides]
Predicate Abstraction for Relaxed Memory Models
Dan A., Meshman Y., Vechev M., Yahav E.
SAS'13: 20th Static Analysis Symposium
[pdf] [pdf (extended version)] [slides]
Dynamic Synthesis for Relaxed Memory Models
Liu F., Nedev N., Prisadnikov N., Vechev M., Yahav E.
PLDI'12: ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation
[pdf]
Automatic Inference of Memory Fences
Kuperstein M., Vechev M., Yahav E.
SIGACT News: Column 46, Volume 43, Number 2, June 2012
[pdf] [slides]
Partial-Coherence Abstractions for Relaxed Memory Models
Kuperstein M., Vechev M., Yahav E.
PLDI'11: ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation
[pdf] [slides]
Automatic Inference of Memory Fences
Kuperstein M., Vechev M., Yahav E.
FMCAD '10: Formal Methods in Computer Aided Design
[pdf] [slides]

Software

DFENCE (PLDI'12): Find the source on GitHub: Get DFENCE !