Publications (by year)

2014

Phrase-Based Statistical Translation of Programming Languages
Svetoslav Karaivanov, Veselin Raychev, Martin Vechev
Onward 2014
PDF
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
Synthesis of Memory Fences via Refinement Propagation
Yuri Meshman, Andrei Dan, Martin Vechev, Eran Yahav
SAS 2014
PDF
Verifying Atomicity via Data Independence
Ohad Shacham, Eran Yahav, Guy Gueta, Alex Aiken, Nathan Bronson, Mooly Sagiv and Martin Vechev
ISSTA 2014
PDF
Practical Concurrent Binary Search Trees via Logical Ordering
Dana Drachsler, Martin Vechev and Eran Yahav
ACM PPoPP 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)

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