Abstraction-guided synthesis of synchronization

ion-Guided Synthesis of Synchronization Martin Vechev IBM Research Eran Yahav IBM Research Greta Yorsh IBM Research We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. ework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a cation, and an abstraction, we infer synchronization that ll (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only raction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be d using the given abstraction. We impleme...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Martin T. Vechev, Eran Yahav, Greta Yorsh
• Keywords: IBM Research, POPL 2010, Programming Languages, Synchronization, Synchronization Martin Vechev