DroidSpeak: Efficient Context Sharing for Multiple-LLM Inference
Yuhan Liu, Yuyang Huang, Jiayi Yao, Zhuohan Gu, Kuntai Du, Hanchen Li, Yihua Cheng, Junchen Jiang, Shan Lu, Madan Musuvathi, Esha Choukse
NSDI | May 2026
Madan Musuvathi
Partner Research Manager
出版物
-
-
-
MSCCL++: Rethinking GPU Communication Abstractions for AI Inference
Changho Hwang, Peng Cheng, Roshan Dathathri, Abhinav Jangda, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Aashaka Shah, Ziyue Yang, Binyang Li, Caio Rocha, Qinghua Zhou, Mahdieh Ghazimirsaeed, Sreevatsa Anantharamu, Jithin Jose
ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2026
-
-
-
PEAK: A Performance Engineering AI-Assistant for GPU Kernels Powered by Natural Language Transformations
M. Tariq, Abhinav Jangda, Angelica Moreira, Madan Musuvathi, Tyler Sorensen
December 2025
-
-
-
If At First You Don’t Succeed, Try, Try, Again…? Insights and LLM-informed Tooling for Detecting Retry Bugs in Software Systems
Bogdan Alexandru Stoica, Utsav Sethi , Yiming Su , Cyrus Zhou, Shan Lu, Jonathan Mace, Madan Musuvathi, Suman Nath
ACM SOSP 2024 | November 2024
-
LLM-Vectorizer: LLM-Based Verified Loop Vectorizer
Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, Shuvendu Lahiri
OOPSLA 2024 | June 2024
-
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
-
-
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
-
HotGPT: How to Make Software Documentation More Useful with a Large Language Model?
Yiming Su, Chengcheng Wan, Utsav Sethi, Shan Lu, Madan Musuvathi, Suman Nath
Hot Topics in Operating Systems (HotOS) | June 2023
-
WAFFLE: Exposing Memory Ordering Bugs Efficiently with Active Delay Injection
Bogdan Alexandru Stoica, Shan Lu, Madan Musuvathi, Suman Nath
EuroSys'23 | May 2023
-
-
-
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
-
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
-
Cancellation in Systems: An Empirical Study of Task Cancellation Patterns and Failures
Utsav Sethi, Haochen Pan, Shan Lu, Suman Nath, Madan Musuvathi
OSDI | June 2022
-
GC3: An Optimizing Compiler for GPU Collective Communication
Meghan Cowan, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Yifan Xiong
February 2022
-
-
-
Synthesizing Collective Communication Algorithms for Heterogeneous Networks with TACCL
Aashaka Shah, Vijay Chidambaram, Meghan Cowan, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi, Rachee Singh
November 2021
-
Breaking the Computation and Communication Abstraction Barrier in Distributed Machine Learning Workloads
Abhinav Jangda, Jun Huang, Guodong Liu, Amir Hossein Nodehi Sabet, Saeed Maleki, Youshan Miao, Madan Musuvathi, Todd Mytkowicz, Olli Saarikivi
ASPLOS 2022 | May 2021
-
Synthesizing optimal collective communication algorithms
Zixian Cai, Zhengyang Liu, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi
PPoPP 2021 | January 2021
-
-
-
EVA: An Encrypted Vector Arithmetic Language and Compiler for Efficient Homomorphic Computation
Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, Madan Musuvathi
PLDI 2020 | December 2019
-
Efficient and Scalable Thread-Safety Violation Detection —- Finding thousands of concurrency bugs during testing
Guangpu Li, Shan Lu, Madan Musuvathi, Suman Nath, Rohan Padhye
ACM Symposium on Operating Systems Principles (SOSP) | October 2019
Best Paper Award
-
Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
-
CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
PLDI 2019 | June 2019
-
What bugs cause production cloud incidents?
Haopeng Liu, Shan Lu, Madan Musuvathi, Suman Nath
Workshop on Hot Topics in Operating Systems (HotOS) | May 2019
-
-
-
Troubleshooting Transiently-Recurring Errors in Production Systems with Blame-Proportional Logging
Liang Luo, Suman Nath, Lenin Ravindranath Sivalingam, Madan Musuvathi, Luis Ceze
USENIX Annual Technical Conference | July 2018
-
Semantics-Preserving Parallelization of Stochastic Gradient Descent
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2018 International Parallel and Distributed Processing Symposium | May 2018
-
-
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
-
-
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
-
2DFQ: Two-Dimensional Fair Queuing for Multi-Tenant Cloud Services
Jonathan Mace, Peter Bodík, Madan Musuvathi, Rodrigo Fonseca, Krishnan Varadarajan
SIGCOMM 2016 | August 2016
-
Parallelizing WFST Speech Decoders
Charith Mendis, Jasha Droppo, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Geoffrey Zweig
ICASSP 2016 | March 2016
-
Low-Rank Methods for Parallelizing Dynamic Programming Algorithms
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2016 Parallel Computing | March 2016
-
-
-
Parallelizing User-Defined Aggregations using Symbolic Execution
Veselin Raychev, Madan Musuvathi, Todd Mytkowicz
October 2015
-
Systematically Exploring the Behavior of Control Programs
Jason Croft, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
2015 USENIX Annual Technical Conference, USENIX ATC '15, Santa Clara, CA, USA | July 2015
-
Yinyang K-Means: A Drop-In Replacement of the Classic K-Means with Consistent Speedup
Yufei Ding, Yue Zhao, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 | July 2015
-
TOP: A Framework for Enabling Algorithmic Optimizations for Distance-Related Problems
Yufei Ding, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
PVLDB | June 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo, Alec Wolman, Landon P. Cox, Kiron Lebeck, Ali Razeen, Madan Musuvathi, Stefan Saroiu
MobiSys’15 | May 2015
-
Failure Sketches: A Better Way to Debug
Baris Kasikci, Cristiano Pereira, Gilles Pokam, Benjamin Schubert, Madanlal Musuvathi, George Candea, Madan Musuvathi
15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015 | May 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo Laffaye, Alec Wolman, Landon Cox, Kiron Lebeck, Ali Razeen, Stefan Saroiu, Madan Musuvathi
MobiSys | May 2015
-
Retro: Targeted Resource Management in Multi-tenant Distributed Systems
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
NSDI | May 2015
-
The Silently Shifting Semicolon
Daniel Marino, Todd D. Millstein, Madanlal Musuvathi, Satish Narayanasamy, Abhayendra Singh, Madan Musuvathi
1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA | May 2015
-
-
-
Towards General-Purpose Resource Management in Shared Cloud Services
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
2014 Hot Topics in System Dependability | October 2014
-
Towards General-Purpose Resource Management in Shared Cloud
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madanlal Musuvathi, Madan Musuvathi
HotDep'14: Proceedings of the 10th USENIX conference on Hot Topics in System Dependability | October 2014
-
Data-Parallel Finite-State Machines
Todd Mytkowicz, Madan Musuvathi, Wolfram Schulte
Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2014
-
Parallelizing dynamic programming through rank convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2014 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming | February 2014
DOI PDF Publication Publication Publication Publication Publication
-
Parallelizing Dynamic Programming Through Rank Convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
February 2014
-
-
-
Bounded Partial-Order Reduction
Katherine E. Coons, Madan Musuvathi, Kathryn S McKinley
ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) | October 2013
-
Safety-first Approach to Memory Consistency Models
International Symposium on Memory Management, ISMM '13, Seattle, WA, USA | June 2013
-
Failure Recovery: When the Cure Is Worse Than the Disease
Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Peter Bodík, Madan Musuvathi, Zheng Zhang, Lidong Zhou
HotOS | May 2013
HotOS
-
A Safety-First Approach to Memory Models
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
IEEE Micro | May 2013, 巻33(3): pp. 96-104
-
-
-
Dynamic Analyses for Data-Race Detection
John Erickson, Stephen N. Freund, Madanlal Musuvathi, Madan Musuvathi
Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers | September 2012
-
Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection
Santosh Nagarakatte, Sebastian Burckhardt, Milo M. K. Martin, Madan Musuvathi
Programming Languages Design and Implementation | July 2012
Programming Languages Design and Implementation
-
End-To-End Sequential Consistency
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
International Symposium on Computer Architecture | June 2012
-
Back to the future: Forecasting program behavior in automated homes
, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
MSR-TR-2012-131 | May 2012
-
Concurrent Library Correctness on the TSO Memory Model
Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
What’s Decidable About Weak Memory Models?
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
Show No Weakness: Sequentially Consistent Specification of TSO Libraries
Alexey Gotsman, Madan Musuvathi, Hongseok Yang
International Symposium on Distributed Computing (DISC '12) | January 2012
-
-
-
Finding Protocol Manipulation Attacks
Todd Millstein, Ramesh Govindan, Madan Musuvathi, Nupur Kothari, Ratul Mahajan
ACM SIGCOMM | August 2011
-
A Case for an SC-Preserving Compiler
Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Programming Language Design and Implementation (PLDI) 2011 | June 2011
-
Predictable and Progressive Testing of Multithreaded Code
Sebastian Burckhardt, Madan Musuvathi, Shaz Qadeer, Jonathan "Peli" de Halleux, Thomas Ball
IEEE Software | May 2011, 巻28: pp. 75-83
-
Efficient Processor Support for DRFx, a Memory Model with Exceptions
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) | March 2011
-
-
-
Effective Data-Race Detection for the Kernel
John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk
Operating System Design and Implementation (OSDI'10) | October 2010
Operating System Design and Implementation (OSDI'10)
-
Line-Up: A Complete and Automatic Linearizability Checker
Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan
Programming Language Design and Implementation (PLDI) | June 2010
Programming Language Design and Implementation (PLDI)
-
DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages
Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Daniel Marino, Madan Musuvathi
International Conference on Programming Language Design and Implementation (PLDI). | June 2010
International Conference on Programming Language Design and Implementation (PLDI).
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
Conference on Tools and Algorithms for the Construction and Analysis of Systems | April 2010
-
Verifying Local Transformations of Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu Singh, Madan Musuvathi
CC 2010: International Conference on Compiler Construction | March 2010
CC 2010: International Conference on Compiler Construction
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010) | March 2010
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010)
-
On the Verification Problem for Weak Memory Models
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2010
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-
GAMBIT: Effective Unit Testing for Concurrency Libraries
Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
MSR-TR-2010-3 | January 2010
-
Fluxo: A System for Internet Service Programming by Non-expert Developers
Emre Kiciman, Ben Livshits, Madan Musuvathi, Kevin C. Webb
ACM Symposium on Cloud Computing | January 2010
-
-
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
MSR-TR-2009-143 | October 2009
-
LiteRace: Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Conference on Programming Language Design and Implementation (PLDI '09) | June 2009
-
FLUXO: A Simple Service Compiler
Emre Kiciman, Ben Livshits, Madan Musuvathi
12th Workshop on Hot Topics in Operating Systems | May 2009
12th Workshop on Hot Topics in Operating Systems
-
(Short Paper) Improving the Responsiveness of Internet Services with Automatic Cache Placement
Alex Rasmussen, Emre Kiciman, Ben Livshits, Madan Musuvathi
EuroSys 2009 | April 2009
-
-
-
Finding and Reproducing Heisenbugs in Concurrent Programs
Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu
OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008
-
Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madan Musuvathi, Satish Narayanasamy
MSR-TR-2008-175 | November 2008
-
Verifying Compiler Transformations for Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu singh, Madan Musuvathi
MSR-TR-2008-171 | November 2008
-
Can You Fool Me? Towards Automatically Checking Protocol Gullibility
Milan Stanojevic, Ratul Mahajan, Todd Millstein, Madan Musuvathi
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks | October 2008
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks
-
Modular difference logic is hard
Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
MSR-TR-2008-140 | October 2008
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
Computer-Aided Verification (CAV) | July 2008
The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.
-
Memory Model Safety of Programs
Sebastian Burckhardt, Madan Musuvathi
July 2008
Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)
-
Fair stateless model checking
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 08: Programming Language Design and Implementation | June 2008
PLDI 08: Programming Language Design and Implementation
-
Cover Algorithms and their Combination
Sumit Gulwani, Madan Musuvathi
ESOP'08/ETAPS'08 Proceedings of the Theory and Practice of Software, 17th European conference on Programming Languages and Systems | March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
MSR-TR-2008-12 | January 2008
A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.
-
-
-
CHESS: A systematic testing tool for concurrent software
Madan Musuvathi, Shaz Qadeer, Thomas Ball
MSR-TR-2007-149 | November 2007
-
Iterative context bounding for systematic testing of multithreaded programs
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 07: Programming Language Design and Implementation | June 2007
PLDI 07: Programming Language Design and Implementation
-
Iterative Context Bounding for Systematic Testing of Multithreaded Programs
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-14 | January 2007
-
Partial-Order Reduction for Context-Bounded State Exploration
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-12 | January 2007
-
-
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, 巻144: pp. 27-41
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
-
-
-
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
-
An Incremental Heap Canonicalization Algorithm
Madanlal Musuvathi, David L. Dill, Madan Musuvathi
SPIN 05: SPIN Workshop | August 2005
-
Modular Arithmetic Decision Procedure
Domagoj Babic, Madan Musuvathi
MSR-TR-2005-114 | August 2005
-
A Combination Method for Generating Interpolants
Greta Yorsh, Madan Musuvathi
MSR-TR-2004-108 | July 2005
in CADE 2005: Twentieth International Conference on Automated Deduction.
-
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
-
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinmin Ou
in TACAS 2005: Eleventh Conference on Tools and Algorithms for the Construction and Analysis of Software | April 2005
-
-
-
Using model checking to find serious file system errors
Junfeng Yang, Paul Twohey, Dawson R. Engler, Madanlal Musuvathi, Madan Musuvathi
ACM Transactions on Computer Systems, OSDI 04: Sixth Symposium on Operating Systems Design & Implementation | December 2004
OSDI 04: Sixth Symposium on Operating Systems Design & Implementation
-
A Two-Tier Technique for Supporting Quantifiers in A Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinming Ou
MSR-TR-2004-109 | October 2004
-
An Incremental Heap Canonicalization Algorithm
Madan Musuvathi, David L. Dill
MSR-TR-2004-37 | April 2004
-
-
-
Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding
Madan Musuvathi, Dawson R. Engler
Electronic Notes in Theoretical Computer Science | July 2003, 巻89(3)
-
-
-
CMC: A pragmatic approach to model checking real code
Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation
-
-
-
MSCCL++: Rethinking GPU Communication Abstractions for AI Inference
Changho Hwang, Peng Cheng, Roshan Dathathri, Abhinav Jangda, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Aashaka Shah, Ziyue Yang, Binyang Li, Caio Rocha, Qinghua Zhou, Mahdieh Ghazimirsaeed, Sreevatsa Anantharamu, Jithin Jose
ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2026
-
LLM-Vectorizer: LLM-Based Verified Loop Vectorizer
Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, Shuvendu Lahiri
OOPSLA 2024 | June 2024
-
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
-
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
-
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
-
GC3: An Optimizing Compiler for GPU Collective Communication
Meghan Cowan, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Yifan Xiong
February 2022
-
Synthesizing Collective Communication Algorithms for Heterogeneous Networks with TACCL
Aashaka Shah, Vijay Chidambaram, Meghan Cowan, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi, Rachee Singh
November 2021
-
Breaking the Computation and Communication Abstraction Barrier in Distributed Machine Learning Workloads
Abhinav Jangda, Jun Huang, Guodong Liu, Amir Hossein Nodehi Sabet, Saeed Maleki, Youshan Miao, Madan Musuvathi, Todd Mytkowicz, Olli Saarikivi
ASPLOS 2022 | May 2021
-
Synthesizing optimal collective communication algorithms
Zixian Cai, Zhengyang Liu, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi
PPoPP 2021 | January 2021
-
Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
-
Efficient and Scalable Thread-Safety Violation Detection —- Finding thousands of concurrency bugs during testing
Guangpu Li, Shan Lu, Madan Musuvathi, Suman Nath, Rohan Padhye
ACM Symposium on Operating Systems Principles (SOSP) | October 2019
Best Paper Award
-
CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
PLDI 2019 | June 2019
-
Semantics-Preserving Parallelization of Stochastic Gradient Descent
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2018 International Parallel and Distributed Processing Symposium | May 2018
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
-
Low-Rank Methods for Parallelizing Dynamic Programming Algorithms
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2016 Parallel Computing | March 2016
-
Parallelizing User-Defined Aggregations using Symbolic Execution
Veselin Raychev, Madan Musuvathi, Todd Mytkowicz
October 2015
-
Systematically Exploring the Behavior of Control Programs
Jason Croft, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
2015 USENIX Annual Technical Conference, USENIX ATC '15, Santa Clara, CA, USA | July 2015
-
Yinyang K-Means: A Drop-In Replacement of the Classic K-Means with Consistent Speedup
Yufei Ding, Yue Zhao, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 | July 2015
-
TOP: A Framework for Enabling Algorithmic Optimizations for Distance-Related Problems
Yufei Ding, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
PVLDB | June 2015
-
The Silently Shifting Semicolon
Daniel Marino, Todd D. Millstein, Madanlal Musuvathi, Satish Narayanasamy, Abhayendra Singh, Madan Musuvathi
1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA | May 2015
-
Failure Sketches: A Better Way to Debug
Baris Kasikci, Cristiano Pereira, Gilles Pokam, Benjamin Schubert, Madanlal Musuvathi, George Candea, Madan Musuvathi
15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015 | May 2015
-
Data-Parallel Finite-State Machines
Todd Mytkowicz, Madan Musuvathi, Wolfram Schulte
Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2014
-
Parallelizing dynamic programming through rank convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2014 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming | February 2014
DOI PDF Publication Publication Publication Publication Publication
-
Parallelizing Dynamic Programming Through Rank Convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
February 2014
-
Safety-first Approach to Memory Consistency Models
International Symposium on Memory Management, ISMM '13, Seattle, WA, USA | June 2013
-
A Safety-First Approach to Memory Models
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
IEEE Micro | May 2013, 巻33(3): pp. 96-104
-
Dynamic Analyses for Data-Race Detection
John Erickson, Stephen N. Freund, Madanlal Musuvathi, Madan Musuvathi
Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers | September 2012
-
Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection
Santosh Nagarakatte, Sebastian Burckhardt, Milo M. K. Martin, Madan Musuvathi
Programming Languages Design and Implementation | July 2012
Programming Languages Design and Implementation
-
End-To-End Sequential Consistency
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
International Symposium on Computer Architecture | June 2012
-
What’s Decidable About Weak Memory Models?
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
Concurrent Library Correctness on the TSO Memory Model
Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
Show No Weakness: Sequentially Consistent Specification of TSO Libraries
Alexey Gotsman, Madan Musuvathi, Hongseok Yang
International Symposium on Distributed Computing (DISC '12) | January 2012
-
Finding Protocol Manipulation Attacks
Todd Millstein, Ramesh Govindan, Madan Musuvathi, Nupur Kothari, Ratul Mahajan
ACM SIGCOMM | August 2011
-
A Case for an SC-Preserving Compiler
Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Programming Language Design and Implementation (PLDI) 2011 | June 2011
-
Predictable and Progressive Testing of Multithreaded Code
Sebastian Burckhardt, Madan Musuvathi, Shaz Qadeer, Jonathan "Peli" de Halleux, Thomas Ball
IEEE Software | May 2011, 巻28: pp. 75-83
-
Efficient Processor Support for DRFx, a Memory Model with Exceptions
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) | March 2011
-
Effective Data-Race Detection for the Kernel
John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk
Operating System Design and Implementation (OSDI'10) | October 2010
Operating System Design and Implementation (OSDI'10)
-
Line-Up: A Complete and Automatic Linearizability Checker
Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan
Programming Language Design and Implementation (PLDI) | June 2010
Programming Language Design and Implementation (PLDI)
-
DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages
Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Daniel Marino, Madan Musuvathi
International Conference on Programming Language Design and Implementation (PLDI). | June 2010
International Conference on Programming Language Design and Implementation (PLDI).
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
Conference on Tools and Algorithms for the Construction and Analysis of Systems | April 2010
-
Verifying Local Transformations of Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu Singh, Madan Musuvathi
CC 2010: International Conference on Compiler Construction | March 2010
CC 2010: International Conference on Compiler Construction
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010) | March 2010
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010)
-
On the Verification Problem for Weak Memory Models
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2010
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-
GAMBIT: Effective Unit Testing for Concurrency Libraries
Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
MSR-TR-2010-3 | January 2010
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
MSR-TR-2009-143 | October 2009
-
LiteRace: Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Conference on Programming Language Design and Implementation (PLDI '09) | June 2009
-
FLUXO: A Simple Service Compiler
Emre Kiciman, Ben Livshits, Madan Musuvathi
12th Workshop on Hot Topics in Operating Systems | May 2009
12th Workshop on Hot Topics in Operating Systems
-
(Short Paper) Improving the Responsiveness of Internet Services with Automatic Cache Placement
Alex Rasmussen, Emre Kiciman, Ben Livshits, Madan Musuvathi
EuroSys 2009 | April 2009
-
Finding and Reproducing Heisenbugs in Concurrent Programs
Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu
OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008
-
Verifying Compiler Transformations for Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu singh, Madan Musuvathi
MSR-TR-2008-171 | November 2008
-
Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madan Musuvathi, Satish Narayanasamy
MSR-TR-2008-175 | November 2008
-
Can You Fool Me? Towards Automatically Checking Protocol Gullibility
Milan Stanojevic, Ratul Mahajan, Todd Millstein, Madan Musuvathi
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks | October 2008
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
Computer-Aided Verification (CAV) | July 2008
The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.
-
Memory Model Safety of Programs
Sebastian Burckhardt, Madan Musuvathi
July 2008
Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
MSR-TR-2008-12 | January 2008
A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.
-
Iterative context bounding for systematic testing of multithreaded programs
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 07: Programming Language Design and Implementation | June 2007
PLDI 07: Programming Language Design and Implementation
-
Iterative Context Bounding for Systematic Testing of Multithreaded Programs
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-14 | January 2007
-
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
-
Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding
Madan Musuvathi, Dawson R. Engler
Electronic Notes in Theoretical Computer Science | July 2003, 巻89(3)
-
CMC: A pragmatic approach to model checking real code
Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation
-
-
-
DroidSpeak: Efficient Context Sharing for Multiple-LLM Inference
Yuhan Liu, Yuyang Huang, Jiayi Yao, Zhuohan Gu, Kuntai Du, Hanchen Li, Yihua Cheng, Junchen Jiang, Shan Lu, Madan Musuvathi, Esha Choukse
NSDI | May 2026
-
MSCCL++: Rethinking GPU Communication Abstractions for AI Inference
Changho Hwang, Peng Cheng, Roshan Dathathri, Abhinav Jangda, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Aashaka Shah, Ziyue Yang, Binyang Li, Caio Rocha, Qinghua Zhou, Mahdieh Ghazimirsaeed, Sreevatsa Anantharamu, Jithin Jose
ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2026
-
If At First You Don’t Succeed, Try, Try, Again…? Insights and LLM-informed Tooling for Detecting Retry Bugs in Software Systems
Bogdan Alexandru Stoica, Utsav Sethi , Yiming Su , Cyrus Zhou, Shan Lu, Jonathan Mace, Madan Musuvathi, Suman Nath
ACM SOSP 2024 | November 2024
-
HotGPT: How to Make Software Documentation More Useful with a Large Language Model?
Yiming Su, Chengcheng Wan, Utsav Sethi, Shan Lu, Madan Musuvathi, Suman Nath
Hot Topics in Operating Systems (HotOS) | June 2023
-
WAFFLE: Exposing Memory Ordering Bugs Efficiently with Active Delay Injection
Bogdan Alexandru Stoica, Shan Lu, Madan Musuvathi, Suman Nath
EuroSys'23 | May 2023
-
Cancellation in Systems: An Empirical Study of Task Cancellation Patterns and Failures
Utsav Sethi, Haochen Pan, Shan Lu, Suman Nath, Madan Musuvathi
OSDI | June 2022
-
GC3: An Optimizing Compiler for GPU Collective Communication
Meghan Cowan, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Yifan Xiong
February 2022
-
Synthesizing Collective Communication Algorithms for Heterogeneous Networks with TACCL
Aashaka Shah, Vijay Chidambaram, Meghan Cowan, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi, Rachee Singh
November 2021
-
Breaking the Computation and Communication Abstraction Barrier in Distributed Machine Learning Workloads
Abhinav Jangda, Jun Huang, Guodong Liu, Amir Hossein Nodehi Sabet, Saeed Maleki, Youshan Miao, Madan Musuvathi, Todd Mytkowicz, Olli Saarikivi
ASPLOS 2022 | May 2021
-
Synthesizing optimal collective communication algorithms
Zixian Cai, Zhengyang Liu, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi
PPoPP 2021 | January 2021
-
Efficient and Scalable Thread-Safety Violation Detection —- Finding thousands of concurrency bugs during testing
Guangpu Li, Shan Lu, Madan Musuvathi, Suman Nath, Rohan Padhye
ACM Symposium on Operating Systems Principles (SOSP) | October 2019
Best Paper Award
-
What bugs cause production cloud incidents?
Haopeng Liu, Shan Lu, Madan Musuvathi, Suman Nath
Workshop on Hot Topics in Operating Systems (HotOS) | May 2019
-
Troubleshooting Transiently-Recurring Errors in Production Systems with Blame-Proportional Logging
Liang Luo, Suman Nath, Lenin Ravindranath Sivalingam, Madan Musuvathi, Luis Ceze
USENIX Annual Technical Conference | July 2018
-
2DFQ: Two-Dimensional Fair Queuing for Multi-Tenant Cloud Services
Jonathan Mace, Peter Bodík, Madan Musuvathi, Rodrigo Fonseca, Krishnan Varadarajan
SIGCOMM 2016 | August 2016
-
Parallelizing User-Defined Aggregations using Symbolic Execution
Veselin Raychev, Madan Musuvathi, Todd Mytkowicz
October 2015
-
Systematically Exploring the Behavior of Control Programs
Jason Croft, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
2015 USENIX Annual Technical Conference, USENIX ATC '15, Santa Clara, CA, USA | July 2015
-
Yinyang K-Means: A Drop-In Replacement of the Classic K-Means with Consistent Speedup
Yufei Ding, Yue Zhao, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 | July 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo, Alec Wolman, Landon P. Cox, Kiron Lebeck, Ali Razeen, Madan Musuvathi, Stefan Saroiu
MobiSys’15 | May 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo Laffaye, Alec Wolman, Landon Cox, Kiron Lebeck, Ali Razeen, Stefan Saroiu, Madan Musuvathi
MobiSys | May 2015
-
Retro: Targeted Resource Management in Multi-tenant Distributed Systems
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
NSDI | May 2015
-
Failure Sketches: A Better Way to Debug
Baris Kasikci, Cristiano Pereira, Gilles Pokam, Benjamin Schubert, Madanlal Musuvathi, George Candea, Madan Musuvathi
15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015 | May 2015
-
Towards General-Purpose Resource Management in Shared Cloud Services
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
2014 Hot Topics in System Dependability | October 2014
-
Towards General-Purpose Resource Management in Shared Cloud
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madanlal Musuvathi, Madan Musuvathi
HotDep'14: Proceedings of the 10th USENIX conference on Hot Topics in System Dependability | October 2014
-
Data-Parallel Finite-State Machines
Todd Mytkowicz, Madan Musuvathi, Wolfram Schulte
Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2014
-
Parallelizing Dynamic Programming Through Rank Convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
February 2014
-
Failure Recovery: When the Cure Is Worse Than the Disease
Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Peter Bodík, Madan Musuvathi, Zheng Zhang, Lidong Zhou
HotOS | May 2013
HotOS
-
A Safety-First Approach to Memory Models
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
IEEE Micro | May 2013, 巻33(3): pp. 96-104
-
Back to the future: Forecasting program behavior in automated homes
, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
MSR-TR-2012-131 | May 2012
-
Finding Protocol Manipulation Attacks
Todd Millstein, Ramesh Govindan, Madan Musuvathi, Nupur Kothari, Ratul Mahajan
ACM SIGCOMM | August 2011
-
Efficient Processor Support for DRFx, a Memory Model with Exceptions
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) | March 2011
-
Fluxo: A System for Internet Service Programming by Non-expert Developers
Emre Kiciman, Ben Livshits, Madan Musuvathi, Kevin C. Webb
ACM Symposium on Cloud Computing | January 2010
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
MSR-TR-2010-3 | January 2010
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
MSR-TR-2009-143 | October 2009
-
(Short Paper) Improving the Responsiveness of Internet Services with Automatic Cache Placement
Alex Rasmussen, Emre Kiciman, Ben Livshits, Madan Musuvathi
EuroSys 2009 | April 2009
-
Finding and Reproducing Heisenbugs in Concurrent Programs
Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu
OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008
-
Can You Fool Me? Towards Automatically Checking Protocol Gullibility
Milan Stanojevic, Ratul Mahajan, Todd Millstein, Madan Musuvathi
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks | October 2008
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks
-
Fair stateless model checking
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 08: Programming Language Design and Implementation | June 2008
PLDI 08: Programming Language Design and Implementation
-
CHESS: A systematic testing tool for concurrent software
Madan Musuvathi, Shaz Qadeer, Thomas Ball
MSR-TR-2007-149 | November 2007
-
Partial-Order Reduction for Context-Bounded State Exploration
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-12 | January 2007
-
CMC: A pragmatic approach to model checking real code
Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation
-
-
-
DroidSpeak: Efficient Context Sharing for Multiple-LLM Inference
Yuhan Liu, Yuyang Huang, Jiayi Yao, Zhuohan Gu, Kuntai Du, Hanchen Li, Yihua Cheng, Junchen Jiang, Shan Lu, Madan Musuvathi, Esha Choukse
NSDI | May 2026
-
PEAK: A Performance Engineering AI-Assistant for GPU Kernels Powered by Natural Language Transformations
M. Tariq, Abhinav Jangda, Angelica Moreira, Madan Musuvathi, Tyler Sorensen
December 2025
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
-
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
-
Yinyang K-Means: A Drop-In Replacement of the Classic K-Means with Consistent Speedup
Yufei Ding, Yue Zhao, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 | July 2015
-
TOP: A Framework for Enabling Algorithmic Optimizations for Distance-Related Problems
Yufei Ding, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
PVLDB | June 2015
-
-
-
EVA: An Encrypted Vector Arithmetic Language and Compiler for Efficient Homomorphic Computation
Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, Madan Musuvathi
PLDI 2020 | December 2019
-
CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
PLDI 2019 | June 2019
-
-
-
TOP: A Framework for Enabling Algorithmic Optimizations for Distance-Related Problems
Yufei Ding, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
PVLDB | June 2015
-
Bounded Partial-Order Reduction
Katherine E. Coons, Madan Musuvathi, Kathryn S McKinley
ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) | October 2013
-
On the Verification Problem for Weak Memory Models
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2010
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-
Cover Algorithms and their Combination
Sumit Gulwani, Madan Musuvathi
ESOP'08/ETAPS'08 Proceedings of the Theory and Practice of Software, 17th European conference on Programming Languages and Systems | March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
-
Iterative context bounding for systematic testing of multithreaded programs
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 07: Programming Language Design and Implementation | June 2007
PLDI 07: Programming Language Design and Implementation
-
Iterative Context Bounding for Systematic Testing of Multithreaded Programs
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-14 | January 2007
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, 巻144: pp. 27-41
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
-
An Incremental Heap Canonicalization Algorithm
Madanlal Musuvathi, David L. Dill, Madan Musuvathi
SPIN 05: SPIN Workshop | August 2005
-
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
-
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinmin Ou
in TACAS 2005: Eleventh Conference on Tools and Algorithms for the Construction and Analysis of Software | April 2005
-
A Two-Tier Technique for Supporting Quantifiers in A Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinming Ou
MSR-TR-2004-109 | October 2004
-
An Incremental Heap Canonicalization Algorithm
Madan Musuvathi, David L. Dill
MSR-TR-2004-37 | April 2004
-
CMC: A pragmatic approach to model checking real code
Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation
-
-
-
Parallelizing WFST Speech Decoders
Charith Mendis, Jasha Droppo, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Geoffrey Zweig
ICASSP 2016 | March 2016
-
A Combination Method for Generating Interpolants
Greta Yorsh, Madan Musuvathi
MSR-TR-2004-108 | July 2005
in CADE 2005: Twentieth International Conference on Automated Deduction.
-
-
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo, Alec Wolman, Landon P. Cox, Kiron Lebeck, Ali Razeen, Madan Musuvathi, Stefan Saroiu
MobiSys’15 | May 2015
-
-
-
Data-Parallel Finite-State Machines
Todd Mytkowicz, Madan Musuvathi, Wolfram Schulte
Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2014
-
Parallelizing Dynamic Programming Through Rank Convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
February 2014
-
Efficient Processor Support for DRFx, a Memory Model with Exceptions
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) | March 2011
-
-
-
Modular difference logic is hard
Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
MSR-TR-2008-140 | October 2008
-
Modular Arithmetic Decision Procedure
Domagoj Babic, Madan Musuvathi
MSR-TR-2005-114 | August 2005
-
-
-
Using model checking to find serious file system errors
Junfeng Yang, Paul Twohey, Dawson R. Engler, Madanlal Musuvathi, Madan Musuvathi
ACM Transactions on Computer Systems, OSDI 04: Sixth Symposium on Operating Systems Design & Implementation | December 2004
OSDI 04: Sixth Symposium on Operating Systems Design & Implementation
-
-
-
DroidSpeak: Efficient Context Sharing for Multiple-LLM Inference
Yuhan Liu, Yuyang Huang, Jiayi Yao, Zhuohan Gu, Kuntai Du, Hanchen Li, Yihua Cheng, Junchen Jiang, Shan Lu, Madan Musuvathi, Esha Choukse
NSDI | May 2026
-
MSCCL++: Rethinking GPU Communication Abstractions for AI Inference
Changho Hwang, Peng Cheng, Roshan Dathathri, Abhinav Jangda, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Aashaka Shah, Ziyue Yang, Binyang Li, Caio Rocha, Qinghua Zhou, Mahdieh Ghazimirsaeed, Sreevatsa Anantharamu, Jithin Jose
ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2026
-
If At First You Don’t Succeed, Try, Try, Again…? Insights and LLM-informed Tooling for Detecting Retry Bugs in Software Systems
Bogdan Alexandru Stoica, Utsav Sethi , Yiming Su , Cyrus Zhou, Shan Lu, Jonathan Mace, Madan Musuvathi, Suman Nath
ACM SOSP 2024 | November 2024
-
LLM-Vectorizer: LLM-Based Verified Loop Vectorizer
Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, Shuvendu Lahiri
OOPSLA 2024 | June 2024
-
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
-
HotGPT: How to Make Software Documentation More Useful with a Large Language Model?
Yiming Su, Chengcheng Wan, Utsav Sethi, Shan Lu, Madan Musuvathi, Suman Nath
Hot Topics in Operating Systems (HotOS) | June 2023
-
WAFFLE: Exposing Memory Ordering Bugs Efficiently with Active Delay Injection
Bogdan Alexandru Stoica, Shan Lu, Madan Musuvathi, Suman Nath
EuroSys'23 | May 2023
-
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
-
Cancellation in Systems: An Empirical Study of Task Cancellation Patterns and Failures
Utsav Sethi, Haochen Pan, Shan Lu, Suman Nath, Madan Musuvathi
OSDI | June 2022
-
Breaking the Computation and Communication Abstraction Barrier in Distributed Machine Learning Workloads
Abhinav Jangda, Jun Huang, Guodong Liu, Amir Hossein Nodehi Sabet, Saeed Maleki, Youshan Miao, Madan Musuvathi, Todd Mytkowicz, Olli Saarikivi
ASPLOS 2022 | May 2021
-
Synthesizing optimal collective communication algorithms
Zixian Cai, Zhengyang Liu, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi
PPoPP 2021 | January 2021
-
EVA: An Encrypted Vector Arithmetic Language and Compiler for Efficient Homomorphic Computation
Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, Madan Musuvathi
PLDI 2020 | December 2019
-
Niijima: sound and automated computation consolidation for efficient multilingual data-parallel pipelines
Guoqing Harry Xu, Margus Veanes (margus), Michael Barnett, Madan Musuvathi (madanm), Todd Mytkowicz (toddm), Ben Zorn (zorn), Huan He, Haibo Lin
Proceedings of the 27th ACM Symposium on Operating Systems Principles | October 2019
-
Efficient and Scalable Thread-Safety Violation Detection —- Finding thousands of concurrency bugs during testing
Guangpu Li, Shan Lu, Madan Musuvathi, Suman Nath, Rohan Padhye
ACM Symposium on Operating Systems Principles (SOSP) | October 2019
Best Paper Award
-
CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
PLDI 2019 | June 2019
-
What bugs cause production cloud incidents?
Haopeng Liu, Shan Lu, Madan Musuvathi, Suman Nath
Workshop on Hot Topics in Operating Systems (HotOS) | May 2019
-
Troubleshooting Transiently-Recurring Errors in Production Systems with Blame-Proportional Logging
Liang Luo, Suman Nath, Lenin Ravindranath Sivalingam, Madan Musuvathi, Luis Ceze
USENIX Annual Technical Conference | July 2018
-
Semantics-Preserving Parallelization of Stochastic Gradient Descent
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2018 International Parallel and Distributed Processing Symposium | May 2018
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) | June 2017
-
2DFQ: Two-Dimensional Fair Queuing for Multi-Tenant Cloud Services
Jonathan Mace, Peter Bodík, Madan Musuvathi, Rodrigo Fonseca, Krishnan Varadarajan
SIGCOMM 2016 | August 2016
-
Parallelizing WFST Speech Decoders
Charith Mendis, Jasha Droppo, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Geoffrey Zweig
ICASSP 2016 | March 2016
-
Low-Rank Methods for Parallelizing Dynamic Programming Algorithms
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2016 Parallel Computing | March 2016
-
Parallelizing User-Defined Aggregations using Symbolic Execution
Veselin Raychev, Madan Musuvathi, Todd Mytkowicz
October 2015
-
Systematically Exploring the Behavior of Control Programs
Jason Croft, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
2015 USENIX Annual Technical Conference, USENIX ATC '15, Santa Clara, CA, USA | July 2015
-
Yinyang K-Means: A Drop-In Replacement of the Classic K-Means with Consistent Speedup
Yufei Ding, Yue Zhao, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015 | July 2015
-
TOP: A Framework for Enabling Algorithmic Optimizations for Distance-Related Problems
Yufei Ding, Xipeng Shen, Madanlal Musuvathi, Todd Mytkowicz, Madan Musuvathi
PVLDB | June 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo, Alec Wolman, Landon P. Cox, Kiron Lebeck, Ali Razeen, Madan Musuvathi, Stefan Saroiu
MobiSys’15 | May 2015
-
Kahawai: High-Quality Mobile Gaming Using GPU Offload
Eduardo Cuervo Laffaye, Alec Wolman, Landon Cox, Kiron Lebeck, Ali Razeen, Stefan Saroiu, Madan Musuvathi
MobiSys | May 2015
-
The Silently Shifting Semicolon
Daniel Marino, Todd D. Millstein, Madanlal Musuvathi, Satish Narayanasamy, Abhayendra Singh, Madan Musuvathi
1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA | May 2015
-
Retro: Targeted Resource Management in Multi-tenant Distributed Systems
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
NSDI | May 2015
-
Failure Sketches: A Better Way to Debug
Baris Kasikci, Cristiano Pereira, Gilles Pokam, Benjamin Schubert, Madanlal Musuvathi, George Candea, Madan Musuvathi
15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015 | May 2015
-
Towards General-Purpose Resource Management in Shared Cloud Services
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madan Musuvathi
2014 Hot Topics in System Dependability | October 2014
-
Towards General-Purpose Resource Management in Shared Cloud
Jonathan Mace, Peter Bodík, Rodrigo Fonseca, Madanlal Musuvathi, Madan Musuvathi
HotDep'14: Proceedings of the 10th USENIX conference on Hot Topics in System Dependability | October 2014
-
Data-Parallel Finite-State Machines
Todd Mytkowicz, Madan Musuvathi, Wolfram Schulte
Architectural Support for Programming Languages and Operating Systems (ASPLOS) | March 2014
-
Parallelizing dynamic programming through rank convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
2014 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming | February 2014
DOI PDF Publication Publication Publication Publication Publication
-
Parallelizing Dynamic Programming Through Rank Convergence
Saeed Maleki, Madan Musuvathi, Todd Mytkowicz
February 2014
-
Bounded Partial-Order Reduction
Katherine E. Coons, Madan Musuvathi, Kathryn S McKinley
ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) | October 2013
-
Safety-first Approach to Memory Consistency Models
International Symposium on Memory Management, ISMM '13, Seattle, WA, USA | June 2013
-
Failure Recovery: When the Cure Is Worse Than the Disease
Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Peter Bodík, Madan Musuvathi, Zheng Zhang, Lidong Zhou
HotOS | May 2013
HotOS
-
Dynamic Analyses for Data-Race Detection
John Erickson, Stephen N. Freund, Madanlal Musuvathi, Madan Musuvathi
Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers | September 2012
-
Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection
Santosh Nagarakatte, Sebastian Burckhardt, Milo M. K. Martin, Madan Musuvathi
Programming Languages Design and Implementation | July 2012
Programming Languages Design and Implementation
-
End-To-End Sequential Consistency
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
International Symposium on Computer Architecture | June 2012
-
What’s Decidable About Weak Memory Models?
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
Concurrent Library Correctness on the TSO Memory Model
Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang, Madan Musuvathi
21st European Symposium on Programming (ESOP 2012) | March 2012
21st European Symposium on Programming (ESOP 2012)
-
Show No Weakness: Sequentially Consistent Specification of TSO Libraries
Alexey Gotsman, Madan Musuvathi, Hongseok Yang
International Symposium on Distributed Computing (DISC '12) | January 2012
-
Finding Protocol Manipulation Attacks
Todd Millstein, Ramesh Govindan, Madan Musuvathi, Nupur Kothari, Ratul Mahajan
ACM SIGCOMM | August 2011
-
A Case for an SC-Preserving Compiler
Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Programming Language Design and Implementation (PLDI) 2011 | June 2011
-
Efficient Processor Support for DRFx, a Memory Model with Exceptions
Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011) | March 2011
-
Effective Data-Race Detection for the Kernel
John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk
Operating System Design and Implementation (OSDI'10) | October 2010
Operating System Design and Implementation (OSDI'10)
-
Line-Up: A Complete and Automatic Linearizability Checker
Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan
Programming Language Design and Implementation (PLDI) | June 2010
Programming Language Design and Implementation (PLDI)
-
DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages
Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Daniel Marino, Madan Musuvathi
International Conference on Programming Language Design and Implementation (PLDI). | June 2010
International Conference on Programming Language Design and Implementation (PLDI).
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
Conference on Tools and Algorithms for the Construction and Analysis of Systems | April 2010
-
Verifying Local Transformations of Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu Singh, Madan Musuvathi
CC 2010: International Conference on Compiler Construction | March 2010
CC 2010: International Conference on Compiler Construction
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010) | March 2010
Proceedings of the Fifteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2010)
-
On the Verification Problem for Weak Memory Models
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, Madan Musuvathi
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2010
Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-
GAMBIT: Effective Unit Testing for Concurrency Libraries
Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010
Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming
-
Fluxo: A System for Internet Service Programming by Non-expert Developers
Emre Kiciman, Ben Livshits, Madan Musuvathi, Kevin C. Webb
ACM Symposium on Cloud Computing | January 2010
-
LiteRace: Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi
Conference on Programming Language Design and Implementation (PLDI '09) | June 2009
-
FLUXO: A Simple Service Compiler
Emre Kiciman, Ben Livshits, Madan Musuvathi
12th Workshop on Hot Topics in Operating Systems | May 2009
12th Workshop on Hot Topics in Operating Systems
-
(Short Paper) Improving the Responsiveness of Internet Services with Automatic Cache Placement
Alex Rasmussen, Emre Kiciman, Ben Livshits, Madan Musuvathi
EuroSys 2009 | April 2009
-
Finding and Reproducing Heisenbugs in Concurrent Programs
Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu
OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008
-
Can You Fool Me? Towards Automatically Checking Protocol Gullibility
Milan Stanojevic, Ratul Mahajan, Todd Millstein, Madan Musuvathi
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks | October 2008
in HotNets '08, Seventh ACM Workship on Hot Topics in Networks
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
Computer-Aided Verification (CAV) | July 2008
The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.
-
Fair stateless model checking
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 08: Programming Language Design and Implementation | June 2008
PLDI 08: Programming Language Design and Implementation
-
Cover Algorithms and their Combination
Sumit Gulwani, Madan Musuvathi
ESOP'08/ETAPS'08 Proceedings of the Theory and Practice of Software, 17th European conference on Programming Languages and Systems | March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
-
Iterative context bounding for systematic testing of multithreaded programs
Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi
PLDI 07: Programming Language Design and Implementation | June 2007
PLDI 07: Programming Language Design and Implementation
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
-
An Incremental Heap Canonicalization Algorithm
Madanlal Musuvathi, David L. Dill, Madan Musuvathi
SPIN 05: SPIN Workshop | August 2005
-
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinmin Ou
in TACAS 2005: Eleventh Conference on Tools and Algorithms for the Construction and Analysis of Software | April 2005
-
Using model checking to find serious file system errors
Junfeng Yang, Paul Twohey, Dawson R. Engler, Madanlal Musuvathi, Madan Musuvathi
ACM Transactions on Computer Systems, OSDI 04: Sixth Symposium on Operating Systems Design & Implementation | December 2004
OSDI 04: Sixth Symposium on Operating Systems Design & Implementation
-
CMC: A pragmatic approach to model checking real code
Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002
OSDI 02: Fifth Symposium on Operating Systems Design and Implementation
-
-
-
PEAK: A Performance Engineering AI-Assistant for GPU Kernels Powered by Natural Language Transformations
M. Tariq, Abhinav Jangda, Angelica Moreira, Madan Musuvathi, Tyler Sorensen
December 2025
-
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
-
GC3: An Optimizing Compiler for GPU Collective Communication
Meghan Cowan, Saeed Maleki, Madan Musuvathi, Olli Saarikivi, Yifan Xiong
February 2022
-
Synthesizing Collective Communication Algorithms for Heterogeneous Networks with TACCL
Aashaka Shah, Vijay Chidambaram, Meghan Cowan, Saeed Maleki, Madan Musuvathi, Todd Mytkowicz, Jacob Nelson, Olli Saarikivi, Rachee Singh
November 2021
-
Memory Model Safety of Programs
Sebastian Burckhardt, Madan Musuvathi
July 2008
Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)
-
-
-
Fusing Effectful Comprehensions
Olli Saarikivi, Margus Veanes, Todd Mytkowicz, Madan Musuvathi
MSR-TR-2016-55 | October 2016
-
Back to the future: Forecasting program behavior in automated homes
, Ratul Mahajan, Matthew Caesar, Madan Musuvathi
MSR-TR-2012-131 | May 2012
-
A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Madan Musuvathi, Sebastian Burckhardt, Pravesh Kothari,
MSR-TR-2010-3 | January 2010
-
Preemption Sealing for Efficient Concurrency Testing
Thomas Ball, Sebastian Burckhardt, Katherine Coons, Madan Musuvathi, Shaz Qadeer
MSR-TR-2009-143 | October 2009
-
Verifying Compiler Transformations for Concurrent Programs
Sebastian Burckhardt, Madanlal Musuvathi, Vasu singh, Madan Musuvathi
MSR-TR-2008-171 | November 2008
-
Effective Sampling for Lightweight Data-Race Detection
Daniel Marino, Madan Musuvathi, Satish Narayanasamy
MSR-TR-2008-175 | November 2008
-
Modular difference logic is hard
Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
MSR-TR-2008-140 | October 2008
-
Effective Program Verification for Relaxed Memory Models
Sebastian Burckhardt, Madan Musuvathi
MSR-TR-2008-12 | January 2008
A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.
-
CHESS: A systematic testing tool for concurrent software
Madan Musuvathi, Shaz Qadeer, Thomas Ball
MSR-TR-2007-149 | November 2007
-
Iterative Context Bounding for Systematic Testing of Multithreaded Programs
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-14 | January 2007
-
Partial-Order Reduction for Context-Bounded State Exploration
Madan Musuvathi, Shaz Qadeer
MSR-TR-2007-12 | January 2007
-
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
-
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
-
Modular Arithmetic Decision Procedure
Domagoj Babic, Madan Musuvathi
MSR-TR-2005-114 | August 2005
-
A Combination Method for Generating Interpolants
Greta Yorsh, Madan Musuvathi
MSR-TR-2004-108 | July 2005
in CADE 2005: Twentieth International Conference on Automated Deduction.
-
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
-
A Two-Tier Technique for Supporting Quantifiers in A Lazily Proof-Explicating Theorem Prover
Rustan Leino, Madan Musuvathi, Xinming Ou
MSR-TR-2004-109 | October 2004
-
An Incremental Heap Canonicalization Algorithm
Madan Musuvathi, David L. Dill
MSR-TR-2004-37 | April 2004
-
-
-
A Safety-First Approach to Memory Models
Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi, Madan Musuvathi
IEEE Micro | May 2013, 巻33(3): pp. 96-104
-
Predictable and Progressive Testing of Multithreaded Code
Sebastian Burckhardt, Madan Musuvathi, Shaz Qadeer, Jonathan "Peli" de Halleux, Thomas Ball
IEEE Software | May 2011, 巻28: pp. 75-83
-
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, 巻144: pp. 27-41
-
Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding
Madan Musuvathi, Dawson R. Engler
Electronic Notes in Theoretical Computer Science | July 2003, 巻89(3)
-