Publications (by year)


2014

Verifying Atomicity via Data Independence
Ohad Shacham, Eran Yahav, Guy Gueta, Alex Aiken, Nathan Bronson, Mooly Sagiv and Martin Vechev
ISSTA 2014

Code Completion with Statistical Language Models
Veselin Raychev, Martin Vechev, Eran Yahav
ACM PLDI 2014
PDF

Commutativity Race Detection
Dimitar Dimitrov, Veselin Raychev, Martin Vechev, Eric Koskinen
ACM PLDI 2014
PDF

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
Accepted with minor revisions to ACM TOPLAS (a journal version of the POPL'11 paper)

Practical Concurrent Binary Search Trees via Logical Ordering
Dana Drachsler, Martin Vechev and Eran Yahav
ACM PPoPP 2014
PDF


2013

Effective Race Detection for Event-Driven Programs
Veselin Raychev, Martin Vechev, Manu Sridharan
ACM OOPSLA 2013
PDF , slides: , see the Event Racer website

Refactoring with Synthesis
Veselin Raychev, Max Schaefer, Manu Sridharan, Martin Vechev
ACM OOPSLA 2013
PDF , slides:

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

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


2012

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

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

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


2011

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)
PDF

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

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

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

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

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
PDF

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


2010

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
PDF

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

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

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

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

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


2009

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
PDF

Experience with Model Checking Linearizability
Martin Vechev, Eran Yahav, Greta Yorsh
SPIN 2009
PDF
Further details (SPIN models, instructions) can be found Here

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

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

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


2008

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

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
PDF

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


2007 and earlier:


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

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

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

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

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

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
PDF

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