Predicate abstraction for relaxed memory models. A. M. Dan, Y. Meshman, M. T. Vechev, and E. Yahav. In SAS, 2013.
[submission] [extended version ] [virtual machine]
Synthesis of memory fences via refinement propagation. A. M. Dan, Y. Meshman, M. T. Vechev, and E. Yahav. In SAS, 2014.
[submission]
Effective abstractions for verification under relaxed memory models. A. M. Dan, Y. Meshman, M. T. Vechev, and E. Yahav. In VMCAI, 2015.
[submission]
Pattern-based synthesis of synchronization for the c++ memory model. Y. Meshman, N. Rinetzky, and E. Yahav. In FMCAD, 2015.
[submission][slides][virtual machine][site][online tool]