Publications

Laws of Order: Synchronization in Concurrent Algorithms
Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael and Martin Vechev
Accepted with minor revisions to ACM TOPLAS (a journal version of the POPL'11 paper)

Automatic Synthesis of Deterministic Concurrency
Veselin Raychev, Martin Vechev, Eran Yahav
Static Analysis Symposium (SAS) 2013

Predicate Abstraction for Relaxed Memory Models
Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav
Static Analysis Symposium (SAS) 2013
, extended version:

Scalable and Precise Dynamic Datarace Detection for Structured Parallelism
Raghavan Raman, Jisheng Zhao, Vivek Sarkar, Martin Vechev, Eran Yahav
ACM PLDI 2012

Dynamic Synthesis for Relaxed Memory Models
Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, Eran Yahav
ACM PLDI 2012

Race Detection for Web Applications
Boris Petrov, Martin Vechev, Manu Sridharan, Julian Dolby
ACM PLDI 2012

QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Mathew Arnold, Martin Vechev, Eran Yahav.
ACM TOSEM 2011 (ACM Transactions on Software Engineering and Methodology)

Testing Atomicity of Composed Concurrent Operations
Ohad Shacham, Nathan Bronson, Alex Aiken, Mooly Sagiv, Martin Vechev and Eran Yahav
ACM OOPSLA 2011

Asynchronous Assertions
Eddie Aftandilian, Samuel Guyer, Martin Vechev and Eran Yahav
ACM OOPSLA 2011

Sprint: Speculative Prefetching of Remote Data
Arun Raman, Greta Yorsh, Martin Vechev and Eran Yahav
ACM OOPSLA 2011

Partial-Coherence Abstractions for Relaxed Memory Models
Michael Kuperstein, Martin Vechev and Eran Yahav.
ACM PLDI 2011

Laws of Order: Expensive Synchronization in Concurrent Algorithms Cannot be Eliminated
Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael and Martin Vechev
ACM POPL 2011

Linux Weekly News features our POPL'2011 result: Laws of Order

Efficient Data Race Detection for Async-Finish Parallelism
Raghavan Raman, Jisheng Zhao, Vivek Sarkar, Martin Vechev and Eran Yahav
Runtime Verification (RV) 2010
Best Paper Award

Automatic Inference of Memory Fences
Michael Kuperstein, Martin Vechev and Eran Yahav
Formal Methods in Computer Aided Design (FMCAD) 2010

Automatic Verification of Determinism for Structured Parallel Programs
Martin Vechev, Eran Yahav, Raghavan Raman and Vivek Sarkar.
Static Analysis Symposium (SAS) 2010

Verifying Linearizability with Hindsight
Peter O' Hearn, Noam Rinetzky, Martin Vechev, Eran Yahav and Greta Yorsh.
ACM PODC 2010

Parallel Checking of Expressive Heap Assertions
Martin Vechev, Eran Yahav and Greta Yorsh.
ACM ISMM 2010

QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Mathew Arnold, Martin Vechev, Eran Yahav.
ACM TOSEM 2010

Abstraction-Guided Synthesis Of Synchronization
Martin Vechev, Eran Yahav and Greta Yorsh.
ACM POPL 2010

Position Paper: Verifying Optimistic Algorithms Should be Easy
Noam Rinetzky, Martin Vechev, Eran Yahav and Greta Yorsh.
EC2: Exploiting Concurrency Efficiently and Correctly -- CAV 2009 Workshop

Experience with Model Checking Linearizability
Martin Vechev, Eran Yahav, Greta Yorsh
SPIN 2009

Further details (SPIN models, instructions) can be found Here

Chameleon: Adaptive Selection of Collections
Ohad Shacham, Martin Vechev, Eran Yahav.
ACM PLDI 2009

Inferring Synchronization under Limited Observability
Martin Vechev, Eran Yahav, Greta Yorsh.
TACAS 2009

Idempotent Work Stealing
Maged Michael, Martin Vechev, Vijay Saraswat.
ACM PPoPP 2009

QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Mathew Arnold, Martin Vechev, Eran Yahav.
ACM OOPSLA 2008

Position Paper: Computer-Assisted Construction of Efficient Concurrent Algorithms
Martin Vechev, Eran Yahav, Maged Michael, Hagit Attiya, Greta Yorsh.
EC2: Exploiting Concurrency Efficiently and Correctly -- CAV 2008 Workshop

Deriving Linearizable Fine-Grained Concurrent Objects
Martin Vechev and Eran Yahav.
ACM PLDI 2008

CGCExplorer: A Semi-Automated Search Procedure for Provably Correct Concurrent Collectors
Martin Vechev, Eran Yahav, David F. Bacon and Noam Rinetzky.
ACM PLDI 2007

Correctness-Preserving Derivation of Concurrent Garbage Collection Algorithms
Martin Vechev, Eran Yahav, David F. Bacon.
ACM PLDI 2006

Derivation And Evaluation Of Concurrent Collectors
Martin Vechev, David F. Bacon, Perry Cheng, David Grove.
ECOOP 2005

Write Barrier Elision for Concurrent Garbage Collectors
Martin Vechev and David F. Bacon.
ACM ISMM 2004

Syncopation: Generational Real-time Garbage Collection in the Metronome
David F. Bacon, Perry Cheng, David Grove, Martin Vechev.
ACM LCTES 2005

High-level Real-time Programming in Java
David F. Bacon, Perry Cheng, David Grove, Michael Hind, V.T. Rajan, Eran Yahav, M. Hauswirth, C. Kirsch, Daniel Spoonhower, and Martin T. Vechev.
ACM EMSOFT 2005

Tuning Java on a DSP
Martin Vechev and Peter Petrov.
GSPX 2004

Java on DSP : Challenges and Choices
Martin Vechev and Peter Petrov.
GSPX 2003