UW CSE’s Programming
Languages and Software Engineering group advances fundamental
research and practical applications
( GitHub) in programming
environments, program analysis, language design, synthesis,
compilers, testing, verification, and security. We have strong
ties to the Sampa
group, Cray, Microsoft Research, NVIDIA, AT&T, and others.
4 papers from PLSE are accepted at POPL'22: 2021
James and collaborators' paper Induction Duality: Primal-Dual Search for Invariants
James and collaborators' paper Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Zach's paper Relational E-Matching
paper A formal foundation for symbolic evaluation with merging
Congrats to all!
Congrats to Chandra,
for their Distinguished Paper award at SPLASH'21 for their work on Rewrite Rule Inference Using Equality Saturation!
Congrats to Jacob
and collaborators for their Best Paper Award at SOSP'21 for their work on
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3!
2021 Melissa and
for their paper
Adapting Reorderable Matrices for Qualitative Analysis
accepted to the IEEE Visualization 2021 workshop on Human-Data Interaction!
Congrats to Remy and his
collaborators for their paper
Optimizing Recursive Queries with Program Synthesis
Eunice and Chandra will attend Rising Stars 2021.
Make sure to catch them in Boston if you're there!
Congrats to 2021 Remy and his
collaborators for their paper on
Convergence of Datalog over (Pre-) Semirings accepted at
and their collaborators
for their paper:
"Taxon: Language for Formal Reasoning with Digital Fabrication Machines"
accepted at UIST 2021!
and their collaborators
for their paper:
"A Roadmap Towards Parallel Printing for Desktop 3D Printers"
accepted at SFF 2021!
for their paper on using Equality Saturation for Rewrite Rule Inference
at OOPSLA 2021!
Congrats to 2021 Yihong
who tied for the first place at the
Student Research Competition
Congrats to Emina
for receiving the
Robin Milner Young Researcher Award!
Talia defended her thesis! Congrats Dr. Ringer!!
Chandra defended her thesis too and will join Certora as a Senior Researcher. Congrats Dr. Nandi!!
on their Amazon Research Award for advancing automated
verification for critical infrastructure software!
and collaborators' paper,
"Pure, Low-Level Tensor Program Rewriting via Access Patterns"
will appear at MAPS'21!
and collaborators from University of Utah got their
paper on Combining Precision Tuning and Rewriting
accepted at ARITH'21!
Congrats to Martin,
and collaborators for their new FSE acceptance “Lightweight and Modular Resource Leak Verification"!
Congrats to Zhen,
and collaborators for their new FSE acceptance
“Checking Conformance of Applications against GUI Policies”!
will join UIUC as an assistant professor.
Exciting news for both Talia and UIUC!!
both defended their thesis!
Congrats Dr. Willsey and Dr. Redmon!!
2021 Yihong's work on
is accepted to PLDI SRC, make sure to check out his poster!
Zach, and collaborators' paper
From DSLs to Accelerator-Rich Platform Implementations: Addressing the Mapping Gap
will appear at LATTE'21.
Make sure to checkout Steven's talk!
and Amy Ko
for winning the CHI 2021 Best Paper Award with their paper
Falx: Synthesis-Powered Visualization Authoring!
Two papers from PLSE are accepted to PLDI'21: 2021
Proof Repair Across Type Equivalences
Dan & collaborators
Reticle: A Virtual Machine for Programming Modern FPGAs
and collaborators. Congrats all!
3 papers from PLSE will appear at 2021 MLSys 2021:
"Efficiently Compiling Dynamic Neural Networks for Model Inference" by
Zach, and their collaborators;
"Equality Saturation for Tensor Graph Superoptimization" by
Remy, and their collaborators;
"A Learned Performance Model for the Tensor Processing Unit" by
Sam and collaborators.
and collaborators' paper "Dynamic Tensor Rematerialization"
is accepted to ICLR 2021!
Amy, and their collaborators' work
"Falx: Synthesis-powered Visualization Authoring" was accepted to
Rashmi, Jason, Suzzane and
"Verifying Determinism in Sequential Programs" was accepted to
René and his collaborators' paper
"Does mutation testing improve testing practices?" was accepted to
and collaborators' work on
egg was named a Distinguished Paper at POPL 2021!
Zach, Luis, Luis, and
Jared were all involved in hosting or presenting at TVMConf! Check out the videos here.
2020 Maaz received a distinguished reviewer award as part of the OOPSLA 2020 AEC! Congrats, Maaz!
Talia will be giving a talk to
CMU's Principles of Programming group.
work at OOPSLA 2020.
Josh is presenting his bachelor's thesis work at
Jared defended his thesis! Congrats, Dr. Jared!
Congrats to 2020 Julie, Ras, and collaborators on the OOPSLA 2020 acceptance!
and collaborators' work on
egg was accepted to POPL 2021! Congrats, all!
James Wilcox also has an accepted POPL 2021 paper with his collaborators.
2020 Talia ran a long-term mentoring program that matched 173 mentees with 95 mentors from around the world!
At ICFP 2020, Talia also co-chaired the largest PLMW ever.
Congrats to Martin, Mike, and collaborators for the acceptance of their paper "Continuous Compliance" at ASE! Check out the camera ready here!
Remy and his collaborators' work on SPORES appeared at VLDB!
Jacob gave a talk at CAV! Check it out here
The DTR team ( Marisa, Steven, Altan, Mike He, Tianqi, and Zach) won the ADA demo award! Congrats, all!
Congrats to PLSE alumnus James Wilcox for his PLDI best paper!
Talia gave a talk on Proof Transformation as part of the logic supergroup.
Members of PLSE participated in Shut down academia to discuss meaningful changes to address anti-black racism in our communities.
Huge congrats to 2020 Mike
the ACM SIGSOFT Outstanding Research Award
for his work on programmer productivity!
and their collaborators from UT Austin
CAV 2020 paper
on Synthesizing JIT Compilers for In-Kernel DSLs!
Congrats to 2020 Talia for
PEO scholar award!
Congrats to 2020 Josh for
2020 Amanda is joining Apple as a Research Engineer! Congratulations!!
2020 Carpentry Compiler by
Zach, and their
collaborators from GRAIL was once again featured in
a news article, this time in
paper on using Equality Saturation for Synthesizing Structured CAD models
is accepted to PLDI 2020!
2020 Talia organized a
panel at POPL.
Her summary of the panel with links to the recording can be found in both the
SIGPLAN Blog and the
Check it out!
2020 Gus's paper,
Enumerating Hardware-Software Splits with Program Rewriting,
was accepted to the
Young Architect Workshop at ASPLOS2020.
Congrats to 2019 Martin,
Mike, and their collaborators
for their paper on Verifying Object Construction at
Congrats to 2019 Amanda,
co-authors Alannah Oleson and
for their acceptance of their paper
"Scout: Rapid Exploration of Interface Layout Alternatives through High-Level Design Constraints" to
2019 Carpentry Compiler by
Zach, and their
collaborators from GRAIL featured on
Sorin on their
CPP 2020 paper about
analyzing the changes that proof engineers make to programs, specifications, and proofs in Coq!
2019 Martin Kellogg won gold at the
Student Research Competition
at ASE with his work on
compile-time detection of machine image sniping!
and collaborators on their
POPL 2020 paper on
visualization by example!
James Bornholt and
Emina for their
paper on fixing code that explodes under symbolic evaluation!
2019 Max is giving an
invited talk about
and collaborators on their
Best Paper Award
2019 OctoML secured
millions in funding!
and all others involved outside of PLSE!
2019 Josh will give
about his work on Theia with
as part of SPLASH-E!
2019 Talia will give
a talk about her work on proof engineering
at UMass Amherst on November 6th as part of the
Rising Stars in CS Lecture Series!
Zach, and collaborators just dropped some big knowledge about writing big proofs! Check out
QED at Large: A Survey of Engineering of Formally Verified Software.
PLSE has two papers at 2019 SIGGRAPH ASIA 2019:
Maaz and his collaborators for their work on lifting legacy image processing
functions to high level DSLs, and
Zach and their collaborators for their work on compilers for carpentry. Congratulations!
2019 Talia will be attending
Rising Stars this year!
2019 James W. joined Certora as their CTO!
2019 Pavel joined Utah's School of Computing as an Assistant Professor!
2019 James Bornholt will be joining UT Austin as an Assistant Professor in 2020!
Congrats to 2019 Pavel,
Mike, and their collaborator,
for their latest Cassius paper at
John Leo, and
Ornaments for Proof Reuse in Coq.
Talia will be talking about this and other proof-related work at
the Coq Users and Developers Workshop!
Watch out world!
Three PLSE undergrads are heading off to grad school in the fall:
2019 Doug will be
heading to Brown
in the fall as a lecturer. Congrats Doug!
2019 James W., and
together with their collaborators have papers in
CAV 2019! Congratulations!!
got a paper into
Our very own
2019 John Toman
defended his PhD! 🎓
paper on tracking floating point precision got into
will be giving the keynote!
Inductive-Inductive Types in Cubical Type Theory
Congrats to 2018 Doug,
and their Systems collaborators
for their EuroSys 2019 paper on
was named an
for his contributions to program synthesis. Congrats!
Adobe Research Fellowship!
2018 Zach and
Facebook Continuous Reasoning Research Award
for their work on continuous program verification.
2018 Max's work on
was a runner-up for the
at the Allen School's Industrial Affiliates event.
2018 Sarah traveled all over, giving talks at
as well as attending
gave a talk at
about his work on
distributed systems verification.
2018 Chenglong and his collaborators won
InfoVis Best Paper
for their work on
gave a talk at UCSD on her
automated proof repair
2018 Chandra gave a talk on her
Reincarnate work at
2018 Jared and his collaborators
Relay, a new high-level IR, into the
TVM machine learning stack.
Congrats to 2018 John and
Their work on
will appear in POPL 2019.
PLSE kicked off the Allen School autumn colloquium series with fantastic talks from
James W., and
gave talks at both
at the Berkeley Institute of Design about inferring user interface structure.
2018 Chandra gave a
talk at ICFP on her work on
Congrats to 2018 Ali,
Ras and their
collaborators for their paper on the TPS
project accepted in the Cell Reports journal!
for their papers at
Congrats to 2018 Sarah,
Ras and their
collaborators for their paper on scraping distributed web data at
2018 Zach taught
distributed system verification at the
DeepSpec Summer School
2018 Emina and
Mike gave two
ISSTA in Amsterdam!
Zach and their
collaborators presented their paper on Tools for Floating-Point
Computations at FM in Oxford, UK!
2018 Zach gave the
The Coq Workshop in Oxford, UK!
UW PLSE students had several great talks and papers at PLDI!
2018 Pavel on VizAssert,
Alex on Herbgrind, and
on modular verification of distributed Systems!
Congrats to 2018 Shumo,
and their collaborators for their paper on SQL semantics in
Congrats to the 2018 Herbie team
for releasing Herbie 1.2!
2018 Zach and
Dan just received an
NSF grant to continue their
work on PL foundations for 3D printing.
for graduating with PhDs! 🎓
June 1 Congrats
to 2018 Calvin,
for Distinguished Paper at ICSE’18
Zach's paper on
Functional Programming for Compiling and Decompiling CAD has been accepted to ICFP 2018!
Congrats to 2018 Sam and
his collaborators for their
SecDev 2018 paper on Checked C!
Congrats to 2018 Martin and
Mike for their
ISSTA 2018 papers!
2018 Jared's ASPLOS 2017
UCSB collaborators was selected as an
IEEE Micro Top Pick!
Congrats to 2018 John and
Dan for their
ECOOP 2018 paper!
Congrats to 2018 Jared,
Steven, Josh, Logan,
for their MAPL 2018 paper!
Congrats to 2018 Eric,
and their collaborators for their CAV, ITP and FM 2018 papers!
2018 Joe won a
Congrats to 2018 Max for receiving an
NSF Honorable mention!
Congrats to 2018 Andy Ko for being recognized with the ICSE 2018 10-year most influential paper award!
Make sure to submit to 2018 PNW PLSE 2018!
2018 James Wilcox's
article in CACM on
Highlights in Systems Verification!
2018 James Wilcox
presenting VerifiedFT at
Congrats to 2018 Michael Ernst
for earning the
ISSTA 2018 Impact Paper Award!
Congrats to 2018 Pavel,
and their coauthors on PLDI’18 acceptances.
Come see the talks in Philly!
2018 Joe is giving a
TED talk on
2018 Œuf is now open source. Check it out on GitHub!
2018 Zach won an NSF CAREER award!
2018 James Bornholt receives a 2018 Facebook Fellowship.
2018 James Wilcox
will have a paper at
VerifiedFT: A Verified, High-Performance Dynamic Race Detector
Dec 11 Congrats to 2017 Amanda and Andy for their acceptance of their paper "Rewire: Interface Design Assistance from Examples" to CHI '18.
UW PLSE will be out in force at 2017 POPL 2018!
We have three papers at POPL:
We also have two papers at CPP:
And one at OBT!
See you in Los Angeles!
2017 Mangpo will
be giving a talk on her work High-Coverage Hint Generation for Racket Programming Assignments
with Berkeley colleagues at
2017 Rashmi Mudduluru will
be giving a talk on her work Lasso Detection Using Partial State Caching
with MSR colleagues at
Sept 7 2017 Andy just received a grant to investigate different programming strategies together with Thomas LaToza. Congrats, Andy and Thomas, and we're excited to see the results of the work.
Aug 11 Congrats on 2017 OOPSLA'17 acceptances for Talia (for Iorek), Sarah and Ras (for Ringer), and Dan and UW PLSE alumnus Ben Wood (on dynamic race detection). Jul 31 Congrats to 2017 Julie for her Onward! 2017 paper on Internet of Things automation.
Jul 22 2017 Joe's YOLO9000 just won Best Paper Honorable Mention at CVPR’2017!
Jul 19 2017 Cosette, by UW PLSE members Shumo, Konstantin, Chenglong, and Alvin, has just been released! Check out this automatic way to check whether SQL queries are equivalent.
Jul 11 At this year's 2017 ICSE, Mike won the Most Influential Paper Award, along with coauthors Carlos Pacheco, Shuvendu K. Lahiri, and Thomas Ball, for Feedback-Directed Random Test Generation, published ten years ago. Congratulations, Mike!
Jun 26 2017 Martin and Calvin were grand finalists in the ACM's 2017 Student Research Competition—Martin took 3rd in the undergrad category and Calvin 3rd in the graduate category. Congrats to both of them, and to Mike, who advises both of them.
Jun 9 Congratulations to 2017 Max and Vincent for winning a 2017 Qualcomm Innovation Fellowship for their project on domain-specific reconfigurable accelerators! This is Vincent's second QIF win.
Jun 2 Congratulations 2017 Alex, who just defended his Ph.D! Alex will graduate at the end of the quarter and begin working on combining program synthesis with deep learning to improve programming productivity and AI capabilities.
May 1UW PLSE has two papers in 2017 ICFP 2017! Congratulations to Jared and his collaborators for their paper on Lean, and to Konstantin, Steven, Emina, Mike, Zach, and their collaborator Stefan for their paper on SpaceSearch!
May 1 2017 Herbie 1.1 has been released. Good work, Pavel, Jason, Alex, and Zach!
Apr 27 2017 Mike is giving an invited talk at ETAPS 2017, discussing his work on using natural langauge processessing to understand non-semantic portions of code. Do not miss it!
Apr 25 You cannot miss 2017 Joe’s talk, at TED 2017. Tech.co called Joe one of the five most notable TED speakers this year, next to Elon Musk and Serena Williams.
Apr 24 Congratulations to 2017 Chandrakana, Dan, and their coauthors for their paper, “Debugging Probabilistic Programs”, at MAPL 2017.
Apr 18 Congratulations to 2017 Alvin and Emina on receiving CAREER awards from the NSF.
Apr 15 Remy (Yisu) Wang, Zhen Zhang, and Rashmi Mudduluru will be joining UW PLSE next year. Welcome! 2017
Apr 15 Congrats to 2017 Ryan and Luke, who have chosen graduate schools where they will pursue their PhDs. Ryan's going to Cornell, while Luke is staying here at UW!
Apr 12 Congratulations to 2017 Sarah and Mangpo for their paper, “Data-Driven Synthesis of Full Probabilistic Programs”, at CAV 2017.
Mar 7 Congratulations to 2017 Konstantin on passing his Ph.D. Defense! Konstantin will graduate at the end of the quarter and move on to applying his research on verifying network configuration at the Google networking team.
Mar 3 2017 Joe’s YOLO9000 has been accepted to CVPR’17: better, faster, strong object detection with a single net.
Feb 24 Congratulations 2017 John, Dan, James, Zach, Ras, Mangpo, Nate, Chandrakana, and Mike, their coauthors, and the several UW PLSE alumni on their accepted papers to SNAPL’17!
Feb 13 2017 James and Emina's paper on memory model synthesis;
Shumo, Konstantin, and Alvin's paper on HoTTSQL; Chenglong, Alvin, and Ras's paper on SQL query synthesis; and Grigory, Maaz, and Ras's work on static parallelization have all been accepted to PLDI 17! Congratulations!
Feb 3 2017 Zach gave a talk at the University of Utah on floating point at the University of Washington: Herbie, Herbgrind, and FPBench.
Jan 16 Congratulations 2017 Mike on winning the ICSE 2017 Most Influential Paper award for his work on feedback-directed random test generation.
Jan 16 2017 Jared helped give a tutorial on his work adding native compilation to the LEAN theorem prover. Check it out!
Dec 14 2016 Evaluating & improving fault localization techniques was accepted to ICSE 2017. It's by Spencer Pearson, ex-postdoc René Just (now at UMass), Michael Ernst, Deric Pang, Benjamin Keller, and their colleagues at Sheffield and Porto.
Dec 9 2016 Melissa Galloway was featured in UW CSE's Undergrad Spotlight.
Dec 9 Congratulations to 2016 Chris Mackie and Nate Yazdani, honorable mentions for 2017 CRA Outstanding Undergraduate Researchers!
Nov 17 2016 Calvin Loncaric and Spencer Pearson were 1st- and 3rd-place graduate students, and Martin Kellogg and Chris Mackie were 1st- and 3rd-place undergraduate students, in the FSE student research competition
Nov 4 Congratulations to Helgi Sigurbjarnarson, 2016 James Bornholt, Emina Torlak, and Xi Wang for winning best paper "Push-Button Verification of File Systems via Crash Refinement" at OSDI 2016!
Nov 1 2016 Andy Ko gave a keynote A human view of programming languages at SPLASH 2016
Oct 5 2016 Luke will present a poster on his and Jared's work on bootstrapping a secure eBPF compiler in Coq at OSDI 2016!
Sep 18 2016 Emina Torlak gave the keynote at RacketCon2016
Aug 30 2016 Chandrakana and Mike's work on program analyses for smart home security has been accepted to PLAS 2016!
Aug 19 UW had eight (!) papers accepted to the 2016 FSE 2016 Student Research Competition. Congratulations to Waylon Huang, Wing Lam, Calvin Loncaric, Martin Kellogg, Chris Mackie, Chandrakana Nandi, Spencer Pearson, Joe Santino. Their advisor is Michael Ernst.
Aug 3 Congratulations to everyone accepted to 2016 OOPLSA 2016! Cassius, Bagpipe, Ringer, and Calvin’s work with Samsung Research America
Jul 27 2016 Ivan a UW alum, Yuriy a UW postdoc alum, Patty, and Mike's paper, Debugging Distributed Systems appeared in CACM August 2016 issue!
Jul 25 2016 Talia, Franzi, and Dan's paper, "AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems" to appear in ACM CCS 2016!
Jul 20 2016 Staccato won both the Distinguished Artifact and Distinguished Poster awards at ECOOP 2016. Congrats, John and Dan!
Jul 5 PLSE swept the best student paper awards at 2016 SYNT 2016! Maaz and Alvin won for their work on verified lifting for data processing; Julie came in second for her work on synthesis for robot motion planning.
Jun 21 2016 Ras wins an Influential Paper Award from ISCA for his 2001 paper Focusing Processor Policies via Critical-Path Prediction.
May 9 2016 Konne will be presenting Bagpipe's BGP formalization in Brazil at NetPL 16.
May 7 Recent PLSE alum and soon-to-be Cornell professor 2016 Adrian Sampson won UW CSE's William Chan Memorial Dissertation Award!
May 4 2016 Alvin won the DoE Early Career Award!
Apr 25 2016 Alvin and his collaborators from MIT, Stanford, and Barefoot Networks' work on programmable switches was accepted to SIGCOMM 2016.
Apr 18 2016 Ivan, Patty, Yuriy, and Mike's paper on Debugging distributed systems is the cover story in the March/April 2016 issue of ACM Queue.
Apr 17 2016 Mike, Alberto, Alessandra, and Mauro's paper on Automatic generation of oracles for exceptional behaviors was accepted to ISSTA 2016.
Apr 16 2016 Mike, Damiano, Massimo, and Fausto's paper on Semantics for locking specifications was accepted to NFM 2016.
Apr 15 2016 Neutrons was accepted to CAV'16. If you're there, come to the talk to learn about verifying a neutron therapy machine.
Mar 29 Congratulations to 2016 Talia Ringer and Amanda Swearngin for winning NSF graduate fellowships!
Mar 1 2016 John and Dan's paper on Staccato, a bug finder for dynamic configuration updates, and Chenglong's paper on API adaptation will appear at ECOOP 2016!
Feb 29 2016 YOLO has been accepted to CVPR'16. Congrats to Joe!
Feb 26 2016 Xi's work on undefined behavior detection appears in this month's Communications of the ACM.
Feb 23 2016 Emina Torlak won the AITO Dahl-Nygaard prize and the Sloan Fellowship!
Jan 20 We have three papers accepted to 2016 PLDI 2016: Calvin, Emina, and Mike’s data structure synthesis with Cozy; Eric, Daryl, Zach, and Dan’s verified peephole optimizations with Peek; and Alvin's verified lifting of stencils with STNG.
Jan 19 2016 Mike and Javier's paper on Locking discipline inference and checking was accepted to ICSE 2016.
Jan 11 2016 Konstantin Weitz was a finalist for the Facebook Fellowship Program!
Dec 21 2015 Pavel Panchekha won the Adobe Research Fellowship. Congrats!
Dec 17 2015 Daryl Zuniga won the prestigious UW Mary Gates Scholarship and an Honorable Mention for the CRA Undergraduate Research Award!
Dec 4 Our paper on 2015 verifying Raft in Verdi will appear at CPP 2016!
Nov 17 PLSE has 2015 four papers accepted to ASPLOS’16: approximate image and video storage, scalable superoptimization, DNA-based storage, and formal specifications for file system crash-consistency. See you in Atlanta!
Nov 17 2015 Alvin Cheung won MIT's George M. Sprowls Award for outstanding PhD theses in computer science!
Oct 5 2015 James, Emina, Dan, and Luis’s paper on optimizing program synthesis with metasketches has been accepted to POPL 2016.
Sep 17 2015 Sam just won the Lockheed Martin Award for Best Engineering Project at the Young Software Engineer Awards. Woohoo! Aug 3 PLSE sent four papers to 2015 OOPSLA this year: on object-oriented constraint solving, constraint programming, synthesis of layout engines, and a framework for synthesis.
Jul 20 The PLSE group has 2015 five papers accepted to ASE’15: evaluating test generation, handling reflection in static analysis, Crust, history granularity transformations, and dynamic race detection. Don’t miss it!
Jun 27 2015 Timelapse has been accepted to UIST’15. Come find out about diffing web interfaces.
Jun 16 The 2015 Herbie and Verdi projects killed it at PLDI’15. Didn't make the talks? Check out the project pages.
May 7 The 2015 Herbie paper won Distinguished Paper at PLDI. Make sure you go see the talk!
May 4 UW PLSE at 2015 SNAPL’15: a dependency case language for a neutron therapy machine, and hardware-software co-design!
Apr 7 2015 Ras Bodik is joining UW PLSE. We're so incredibly excited to work with him!
Mar 31 Congrats 2015 Doug Woos and Pavel Panchekha, two students in UW PLSE, who just became NSF fellows.
Jan 18 2015 Verso presenting first steps toward low-level optimizations in CompCert, at CoqPL’15.