Matthew Sotoudeh

email me

PhD candidate at Stanford University

really, email me

Bachelor's degree from the University of California, Davis with majors in Mathematics and Computer Science

email me

I am fortunate to have been advised at various levels of formality by too many people to name, however the list of recent formal advisors is short enough to fit on a webpage:
Prof. Dawson Engler (PhD advisor),
Prof. Aditya Thakur (BS advisor),
Prof. Clark Barrett (PhD rotation advisor),
Dr. Jason Knight (Intel AIPG),
Dr. Sara Baghsorkhi (Intel Labs).

Beyond my classroom teaching, I have had the opportunity to mentor Sophie Andrews (then Stanford undergraduate, now full-time Apple) whose research on speeding up bounded model checking was recently accepted for publication at DATE 2025.

questions? email me

Conference & Journal Papers

questions? thoughts? complaints? ideas? email me

• Automated Verification of Monotonic Data Structure Traversals in C
  Matthew Sotoudeh
  37th International Conference on Computer Aided Verification (CAV 2025, to appear)
  [Conference]
• Pathological Cases for a Class of Reachability-Based Garbage Collectors
  Matthew Sotoudeh
  2025 Object-Oriented Programming, Systems, Languages, & Applications Conference (OOPSLA 2025, to appear)
  [Full PDF] [Conference PDF] [arXiv] [Artifact] [Conference]
• Efficient SAT-based Bounded Model Checking of Evolving Systems
  Andrews, S.; Sotoudeh, M.; Barrett, C.
  2025 Design, Automation and Test in Europe Conference (DATE 2025)
  [Conference] [Code]
• Sidekick: In-Network Assistance for Secure End-to-End Transport Protocols
  Yuan, G.; Sotoudeh, M.; Zhang, D. K.; Welzl, M.; Mazières, D.; Winstein, K.
  21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 2024)
  Won NSDI 2024 Outstanding Paper Award
  Won NSDI 2024 Community Award
  [Proceedings]
• SyReNN: A Tool for Analyzing Deep Neural Networks
  Sotoudeh, M. (equal contribution); Tao, Z. (equal contribution); Thakur, A. V.
  International Journal on Software Tools for Technology Transfer (STTT 2023)
  [Paper]
• Provable Repair of Deep Neural Networks
  Sotoudeh, M. and Thakur, A. V.
  42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021)
  [Proceedings] [Conference] [Code] [arXiv]
• SyReNN: A Tool for Analyzing Deep Neural Networks
  Sotoudeh, M. and Thakur, A. V.
  27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021)
  [Proceedings] [Code] [arXiv]
• Analogy-Making as a Core Primitive in the Software Engineering Toolbox
  Sotoudeh, M. and Thakur, A. V.
  Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (SPLASH "Onward!" 2020)
  [Proceedings] [Talk] [Poster] [Code] [BibTeX] [arXiv]
• Abstract Neural Networks
  Sotoudeh, M. and Thakur, A. V.
  Proceedings of the 27th Static Analysis Symposium (SAS 2020)
  [Proceedings] [Talk] [Code] [Conference] [arXiv]
• Computing Linear Restrictions of Neural Networks
  Sotoudeh, M. and Thakur, A. V.
  Advances in Neural Information Processing Systems (NeurIPS 2019)
  [Proceedings] [Poster] [Slides] [Code] [BibTeX] [arXiv (old)]
• ISA Mapper: A Compute and Hardware Agnostic Deep Learning Compiler
  Sotoudeh, M.; Venkat, A.; Anderson, M.; Georganas, E.; Heinecke, A.; Knight, J.
  Proceedings of the 16th ACM International Conference on Computing Frontiers (CF 2019)
  [Proceedings] [Slides] [BibTeX] [arXiv (old)]
• C3-Flow: Compute Compression Co-Design Flow for Deep Neural Networks
  Sotoudeh, M. and Baghsorkhi, S. S.
  Proceedings of the 56th Annual Design Automation Conference (DAC 2019)
  [Proceedings] [Slides] [BibTeX] [arXiv (old)]

Other Writings and Posters

• Magic Buddy Allocation
  Matthew Sotoudeh
  Paged Out! #6
  [Article PDF] [Whole Issue PDF] [Magazine Homepage]
• Underconstrained Execution of Device Drivers from Partial Source Code
  Sotoudeh, M.; Srivatsan, A.
  Symposium on Operating Systems Principles (SOSP) 2024 Poster Session
• Stateless SFI: Faster and Safer Machine Code Validation
  Yedidia, Z.; Sotoudeh, M.; and Mazieres, D.
  Operating System Design and Implementation (OSDI) 2024 Poster Session
• Incremental Bounded Model Checking as Program Source Changes
  Andrews, S. and Sotoudeh, M.
  Formal Methods in Computer-Aided Design (FMCAD) 2023 Student Forum
• System-Specific Interpreters Make Megasystems Friendlier
  Matthew Sotoudeh
  Eighth Workshop on Live Programming (LIVE 2022)
  [arXiv] [Code] [Talk] [Workshop]
• A Short Survey of Weak Reasoning Assistants
  Matthew Sotoudeh
  Third Workshop on Human Aspects of Types and Reasoning Assistants (HATRA 2022, extended abstracts)
  [Extended Abstract] [Talk] [Workshop]
• Sidecar: In-Network Performance Enhancements in the Age of Paranoid Transport Protocols
  Yuan, G.; Zhang, D. K.; Sotoudeh, M.; Welzl, M.; Winstein, K.
  Twenty-first ACM Workshop on Hot Topics in Networks (HotNets 2022)
  [Proceedings] [Workshop]
• Bounded Model Checking of Deep Neural Network Controllers
  Sotoudeh, M. (Advised by Thakur, A. V.)
  Won second place at the International Symposium on Principles Of Programming Languages (POPL) 2020 Student Research Competition
  [Competition] [Code]
• Correcting Deep Neural Networks with Small, Generalizing Patches
  Sotoudeh, M. and Thakur, A. V.
  NeurIPS 2019 Workshop on Safety and Robustness in Decision Making
  [PDF] [Code] [BibTeX]

Presentations

• Abstract Neural Networks, COVID Papers from SAS at SPLASH 2022, Auckland, New Zealand
• System-Specific Interpreters Make Megasystems Friendlier, LIVE 2022 short talks, Auckland, New Zealand
• A Survey of Weak Reasoning Assistants, HATRA 2022, Auckland, New Zealand
• Provable Repair of Deep Neural Networks, PLDI 2021, Virtual
• SyReNN: A Tool for Analyzing Deep Neural Networks, TACAS 2021, Virtual
• Understanding and Repairing Deep Neural Networks, Waterloo ML + Logic Colloquium 2020, Virtual (with Aditya Thakur)
• Abstract Neural Networks, SAS 2020, Virtual
• Analogy-Making as a Core Primitive in the Software Engineering Toolbox, Onward! 2020, Virtual
• Bounded Model Checking of Deep Neural Network Controllers, POPL SRC 2020, New Orleans, LA
• Computing Linear Restrictions of Neural Networks, NeurIPS 2019, Vancouver, BC, Canada
• ISA Mapper: A Compute and Hardware Agnostic Deep Learning Compiler, CF 2019, Alghero, Italy
• C3-Flow: Compute Compression Co-Design Flow for Deep Neural Networks, DAC 2019, Las Vegas, NV
• Correcting Deep Neural Networks with Small, Generalizing Patches, SRDM 2019, Vancouver, BC, Canada

Honors & Awards

• Highest Honors, awarded with my B.S. in Computer Science
• Citation for Outstanding Performance, UC Davis Mathematics Department
• Honorable Mention, UC Davis Chancellor's Award for Excellence in Undergraduate Research/Dean Keith Simonton Prize
• National Science Foundation Graduate Research Fellowship
• Honorable Mention, CRA Outstanding Undergraduate Researcher Award
• 2nd Place, POPL 2020 Student Research Competition
• Regents Scholarship, UC Davis
• Rep. Ro Khanna Congressional Award
• Travel Awards: NeurIPS Foundation (2019), UC Davis CS Department (2020), UC Davis URC (2019)

Teaching & Service

For some of the courses I have written day-long lab activites that introduce students to program analysis and automated reasoning in a hands-on activity. You can find most of these in this git repo.

• (Planned) Teaching Fellow (primary instructor) for CS 161 (Design and Analysis of Algorithms), Stanford University, Summer 2025
• (Planned) Teaching Fellow for CS 343S (Domain-Specific Language Design Studio), Stanford University, Spring 2025
• Course Assistant for CS 140e (Embedded Operating Systems), Stanford University, Winter 2025
• Teaching Fellow (primary instructor) for CS 161 (Design and Analysis of Algorithms), Stanford University, Summer 2024
  [Lecture Notes and Homeworks]
• Teaching Fellow for CS 343S (Domain-Specific Language Design Studio), Stanford University, Spring 2024
• Course Assistant for CS 103 (Mathematical Foundations of Computing), Stanford University, Winter 2024
• Course Assistant for CS 240LX (Advanced Operating Systems Lab), Stanford University, Spring 2023
• Course Assistant for CS 197 ("team-based introduction to Computer Science research" for undergraduates), Stanford University, Fall 2022
• Course Assistant for CS 240 (Advanced Topics in Operating Systems), Stanford University, Spring 2022
• TACAS 2022 Artifact Evaluation Committee member
• Co-chair of the UC Davis CS Tutoring Committee

If you are in the Palo Alto area with an interest in teaching and enough free time, I would also recommend DreamCatchers as a great opportunity to volunteer with a local middle school after-school program.

Contact

My permanent email address is matthew@masot.net. If you are considering sending me an email, please do so!

However, I use pretty crude filtering to remove the vast majority of spam I receive. If you are a real human, and you are sending me personally an email, and I have not replied to your email, please know that I really do want to receive and read it, but you might need to rewrite it to be less spammy and resend it before it arrives in my inbox. If you commonly send spam to mailing lists I subscribe to, your email address itself might be blocked. Please try sending from a different address.

To help real humans who want to send me real messages, I publish my filtering script here. Please don't evade the spirit of this gesture or I'll have to stop publishing these.

None of those accounts are entirely managed by me, so it would be prudent to assume any communications sent to those addresses may be viewed surreptitiously by others. You are encouraged to use my PGP Key if this concerns you.

really really, email me !

Other

You can find a variety of projects on my git lair and GitHub profile, ranging from add-ons for Google Docs to transpilers. Please note that I try to respond to crawlers that ignore robots.txt pretty aggressively, so if you live in a region that causes you to share IP blocks with such bad actors (especially ByteSpider), there is a chance your IP address is explicitly banned. In such unfortunate cases, I am happy to unblock your IP if you send me an email.

I used to collect a list of interesting proofs.

In 2017 I taught a one-week course on programming for middle schoolers in the Bay Area. Most of the curriculum for that course, including presentations, lesson outlines, projects, and retrospective comments are available here.

This page was last updated on 4/17/2025.