https://uwplse.org

UW PLSEUW PLSE News Blog Projects People Colloquia Meetings Internal Get Involved UW Programming Languages and Software Engineering (PLSE) About UW PLSE UW CSE’s Programming Languages and Software Engineering group advances fundamental research and practical applications (some in this GitHub organization) in programming environments, program analysis, language design, synthesis, compilers, testing, verification, and security. We have strong ties to the Sampa and SAMPL groups, Intel, Cray, Microsoft Research, NVIDIA, AT&T, and others. Are you an undergrad at UW who wants to get involved with our research? Check out our page on getting involved! Recent Blog Posts 30 September 2024 Understanding Curry-Howard through Rocq by Audrey Seo keywords: #rocq #coq #inductive-datatypes #curry-howard #theorem-proving #proof-assistant 16 September 2024 How to Knit Objects Weird by Amy Zhu, Marlena Preigh keywords: #knitting 02 September 2024 Theorem Proving with Differential Equations by Ryan Zambrotta keywords: #proof-assistant #differential-equation #computer-algebra See all blog posts News September 2024Congratulations to Zach for his promotion to Professor! Congrats to Ben, Sam, Ryan Featherman, Hannah, Ardi, and René for their paper Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs at ISSTA 2024. Congrats to Audrey, Dan, and their collaborators for their paper Correctly Compiling Proofs About Programs Without Proving Compilers Correct at ITP 2024. Congrats to James, Mike, and René, whose paper “Verifying the Option Type with Rely-Guarantee Reasoning” was accepted to ASE 2024. Congrats to Benedikt Schesch, Ryan Featherman, Kenneth, Ben R. Roberts, and Mike, whose paper “Evaluation of Version Control Merge Tools” was accepted to ASE 2024. August 2024Congrats to Haoran, Mike, and their collaborators, whose paper “GoFree: Reducing Garbage Collection via Compiler-Inserted Freeing” was accepted to CGO 2025. July 2024Congrats to René, Mike, and their collaborators, whose paper “Call graph soundness in Android static analysis” was accepted to ISSTA 2024. Congrats to Yihong, Remy, and Dan for their paper “Semantic foundations of equality saturation”, which is accepted at ICDT 2025. May 2024Congrats to René, Mike, and their collaborators, whose paper Are Mutants a Valid Substitute for Real Faults in Software Testing? will be awarded a Test of Time award at FSE 2024. Congrats to Eunice, Edward, Jeff, and René, whose paper rTisane: Externalizing conceptual models for data analysis prompts reconsideration of domain assumptions and facilitates statistical modeling won a Best Paper award at CHI 2024 Shout out to Anjali, James, and Zach for organizing the PNW PLSE 2024 workshop, which was held on May 7th. Check out the link to see the full program! Two PLSE-affiliated papers are selected for MIT PL Review 2024: Better Together: Unifying Datalog and Equality Saturation by Yihong, Remy, Oliver, Zach, Max, and collaborators. Efficient Bottom-Up Synthesis for Programs with Local Variables by Yihong and collaborators. April 2024Congrats to Amy, Yuxuan, Ben, Zach, and Adriana for their paper Computational Illusion Knitting, which is accepted at SIGGRAPH 2024. Congrats to Thia for winning NSF Graduate Research Fellowships Program (GRFP) and Vishal for winning honorable mention. Congrats to Gilbert and his collaborators, whose paper A Verified Compiler for a Functional Tensor Language is accepted at PLDI 2024. March 2024Congrats to Edward, Zach, and Steven for their paper Magic Markup: Maintaining Document-External Markup with an LLM at Programming with AI workshop collocated with 2024. The PLSE lab organized a game jam. Check out the poster and the games! January 2024The biweekly PLSE blog series is launched! November 2023Two papers from PLSE are accepted at ASPLOS 2024: FPGA Technology Mapping Using Sketch-Guided Program Synthesis by Gus, Ben, Vishal, Andrew, Steven, Oak, René, Gilbert, and Zach Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code Transformations by Michael, Reshabh, Alexandra, Dan, and David. Congrats to everyone! October 2023Congrats to Yihong and his collaborators whose paper Efficient Bottom-Up Synthesis for Programs with Local Variables is accepted at POPL 2024. Congrats to Hannah and her collaborators whose paper Live Pattern Matching with Typed Holes won a distinguished paper award at OOPSLA. September 2023Oliver gave a talk on Making Interval Arithmetic Robust to Overflow at ARITH 2023. Congrats to Andrew for winning the first place in the postgraduate category; Thia for winning the first place and Vishal for winning the third place in the undergraduate category at the Student Research Competition at ICFP 2023! John co-organized the FARM workshop at ICFP, where Amy gave a talk on Exploring Self-Embedded Knitting Programs with Twine. Congrats to Gus, who was awarded the Bonderman Fellowship for independent travel! August 2023PLSE remembers Cornell student and friend of the lab Priya Srikumar. Five papers from PLSE are accepted to OOPSLA 2023: Equality Saturation Theory Exploration à la Carte by Anjali, Brett, Ryan, Thia, Amy, Oliver, Max, Zach, and Chandra. Live Pattern Matching with Typed Holes by Hannah and her collaborators. A Pretty Expressive Printer by Sorawee, Emina, and their collaborators. Rhombus: A New Spin on Macros Without All the Parentheses by Sorawee and his collaborators. Inference of Resource Management Specifications by Mike and his collaborators. Moreover, Mike and collaborators’ paper Pluggable Type Inference for Free is accepted to ASE 2023. Sorawee and collaborators’ paper on Generating Conforming Programs With Xsmith is accepted to GPCE 2023. July 2023Congrats to Thomas and Hannah for winning first and second place in the ISSTA 2023 ACM Student Research Competition Congrats to Edward, Caleb, Brett, Eunice, Zach, and Pavel, whose paper on Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting is accepted at UIST 2023. Congrats to Jacob, Xi, Emina, and their collaborators for having their paper on Synthesis-Aided Crash Consistency for Storage Systems accepted at ECOOP 2023. Zach and Pavel co-organized FPTalks 2023, where Edward gave a talk on Odyssey. René co-organized ECOOP and ISSTA 2023. June 2023The PLSE lab played a big part at PLDI 2023: Yihong presented the egglog paper. Gus gave a talk at PLARCH on Generate Compilers from Hardware Models!. Gilbert co-organized DRAGSTERS 2023. Gilbert gave a talk at ARRAY on “Performance vs. Correctness When Writing Low-Level HPC/Tensor/Array Code”. Max and Zach co-organized the second EGRAPHS workshop; Oliver and Yihong presented. May 2023Remy and Eunice will join UCLA as Assistant Professors. Max will join UC Berkeley as an Assistant Professor. Sorawee and Jacob will join Veridise. Congrats to all! Anjali and Zach co-organized PNW PLSE 2023, which is a success. Hannah, Ardi, Eunice, Audrey, John, Gus, and many friends presented! April 2023Hannah and many friends at PLSE hosted a PLSE outreach activity for the Admitted Student Day. March 2023Alexandra received a fellowship from NSF Graduate Research Fellowship Program (GRFP). Congrats! January 2023 Congrats to Remy, Max, and Dan Suciu, for their paper Free Join: Unifying Worst-Case Optimal and Traditional Joins, which will appear at SIGMOD 2023! October 2022 Congrats to Hannah, Ardi, René, and collaborators for their Onward! paper on Contextualized programming language documentation, which will appear at SPLASH 2022! September 2022 Congrats to Mike and his collaborators for their paper Call Me Maybe: Using NLP to automatically generate unit test cases respecting temporal constraints at ASE 2022! July 2022 Gilbert Bernstein will be joining PLSE as an Assistant Professor in Jan. Welcome Prof. Bernstein! Congrats to Oliver, Max, Zach, and collaborators for their paper Short Proofs from Congruence Closure accepted to FMCAD! FPTalks ‘22 was successfully held on July 6, with a plethora of exciting talks. Congratulations! Congrats to Sorawee, Emina, and their collaborators for their paper Testing Dafny (Experience Paper) accepted to ISSTA 2022. June 2022 Congrats to Yihong for winning the second place at the Grand Finals of the ACM Student Research Competition! EGRAPHS ‘22, the first ever workshop dedicated to e-graphs and related techniques, was successfully held. Shout out to Max and Zach for organizing it! May 2022 Congrats to Martin, Mike, and their collaborators for their paper on Accumulation Analysis at ECOOP 2022! March 2022 Martin will join NJIT as an Assistant Professor, congratulations and please keep in touch! Eunice, Audrey, René, and Jeff received an honorable mention for their paper on Tisane, at CHI 2022! Dan Suciu, Remy, and collaborators’ work Convergence of Datalog over (Pre-) Semirings is named a Best Paper at PODS 2022! Rock, Katharina, and René’s work on Scaffolding Preregistrations to Automatically Generate Analysis Code and Methods Descriptions will appear at CHI 2022, Congrats! January 2022 René and collaborators’ work on Repairing brain-computer interfaces with fault-based data acquisition will appear at ICSE 2022, Congrats! Sam, Ryan, René, and collaborators’ work on Prioritizing mutants to guide mutation testing will appear at ICSE 2022, Congrats! Eunice, Melissa, René, and collaborators’ work on Hypothesis formalization has been published at TOCHI, Congrats! René and collaborators’ work on Comparing mutation tools for research, education, and practice has been accepted to CACM, Congrats! December 2021 Mike He received an honorable mention from the CRA outstanding undergraduate researcher award. Congrats! Eunice, Audrey, René and collaborator’s work on Tisane will appear at CHI 2022, Congrats! October 2021 4 papers from PLSE are accepted at POPL’22: 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 Yihong, Remy, Max, and Zach’s paper Relational E-Matching Sorawee, Luke, Xi and Emina’s paper A formal foundation for symbolic evaluation with merging Congrats to all! Congrats to Chandra, Max, Amy, Remy, Brett, Adam, Adriana, Dan, and Zach 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! September 2021 Congrats to Melissa and Eunice 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 accepted to SIGMOD 2022! Eunice and Chandra will attend Rising Stars 2021. Make sure to catch them in Boston if you’re there! August 2021 Congrats to Remy and his collaborators for their paper on Convergence of Datalog over (Pre-) Semirings accepted at PODS 2022! Congrats to Jasper, Chandra, and their collaborators for their paper: “Taxon: Language for Formal Reasoning with Digital Fabrication Machines” accepted at UIST 2021! Congrats to Chandra, Adam, Adriana, Dan, and Zach and their collaborators for their paper: “A Roadmap Towards Parallel Printing for Desktop 3D Printers” accepted at SFF 2021! July 2021 Congrats to Chandra, Max, Amy, Remy, Brett, Adam, Adriana, Dan, and Zach for their paper on using Equality Saturation for Rewrite Rule Inference at OOPSLA 2021! June 2021 Congrats to Yihong and Caleb, who tied for the first place at the Student Research Competition at PLDI’21! 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!! May 2021 Congrats to Emina and Xi on their Amazon Research Award for advancing automated verification for critical infrastructure software! Gus, Andrew, Steven, Luis, Zach, and collaborators’ paper, “Pure, Low-Level Tensor Program Rewriting via Access Patterns” will appear at MAPS’21! Brett, Chandra, Zach, 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, Mike and collaborators for their new FSE acceptance “Checking Conformance of Applications against GUI Policies”! Talia will join UIUC as an assistant professor. Exciting news for both Talia and UIUC!! Max and Joe both defended their thesis! Congrats Dr. Willsey and Dr. Redmon!! April 2021 Yihong’s work on Relational E-matching is accepted to PLDI SRC, make sure to check out his poster! Steven, Mike He, Gus, 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! March 2021 Congrats to Chenglong, Ras, and Amy Ko for winning the CHI 2021 Best Paper Award with their paper Falx: Synthesis-Powered Visualization Authoring! February 2021 Two papers from PLSE are accepted to PLDI’21: Proof Repair Across Type Equivalences by Talia, RanDair Porter, Dan & collaborators Reticle: A Virtual Machine for Programming Modern FPGAs by Luis, Joseph, Dan, Luis and collaborators. Congrats all! January 2021 3 papers from PLSE will appear at MLSys 2021: “Efficiently Compiling Dynamic Neural Networks for Model Inference” by Jared, Zach, and their collaborators; “Equality Saturation for Tensor Graph Superoptimization” by Max, Remy, and their collaborators; “A Learned Performance Model for the Tensor Processing Unit” by Sam and collaborators. Marisa, Steven, Altan, Mike, Jared, Zach and collaborators’ paper “Dynamic Tensor Rematerialization” is accepted to ICLR 2021! December 2020 Chenglong, Ras, Amy, and their collaborators’ work “Falx: Synthesis-powered Visualization Authoring” was accepted to CHI 2021! Rashmi, Jason, Suzzane and Mike’s paper “Verifying Determinism in Sequential Programs” was accepted to ICSE 2021! René and his collaborators’ paper “Does mutation testing improve testing practices?” was accepted to ICSE 2021! Max, Chandra, Remy, Zach 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. November 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. Julie is presenting her work at OOPSLA 2020. Josh is presenting his bachelor’s thesis work at PLATEAU 2020. Jared defended his thesis! Congrats, Dr. Jared! September 2020 Congrats to Julie, Ras, and collaborators on the OOPSLA 2020 acceptance! Max, Remy, Chandra, Zach and collaborators’ work on egg was accepted to POPL 2021! Congrats, all! James Wilcox also has an accepted POPL 2021 paper with his collaborators. May-August 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. May 4 2020 Huge congrats to Mike for receiving the ACM SIGSOFT Outstanding Research Award for his work on programmer productivity! April 5 2020 Congrats to Jacob, Luke, Xi, Emina, and their collaborators from UT Austin for their CAV 2020 paper on Synthesizing JIT Compilers for In-Kernel DSLs! April 1 2020 Congrats to Talia for receiving a PEO scholar award! MAr 30 2020 Congrats to Josh for receiving the NSF GRFP! Mar 16 2020 Amanda is joining Apple as a Research Engineer! Congratulations!! Mar 9 2020 Carpentry Compiler by Chandra, Zach, and their collaborators from GRAIL was once again featured in a news article, this time in The Daily! Feb 27 2020 Chandra, Max, Adam, James W., Zach, Eva, and Dan’s paper on using Equality Saturation for Synthesizing Structured CAD models is accepted to PLDI 2020! Feb 10 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 SIGOPS Blog. Check it out! Feb 9 2020 Gus’s paper, Enumerating Hardware-Software Splits with Program Rewriting, was accepted to the Young Architect Workshop at ASPLOS2020. Dec 9 2019 Congrats to Martin, Mike, and their collaborators for their paper on Verifying Object Construction at ICSE 2020! Dec 9 2019 Congrats to Amanda, Chenglong and Amy, and co-authors Alannah Oleson and James Fogarty for their acceptance of their paper “Scout: Rapid Exploration of Interface Layout Alternatives through High-Level Design Constraints” to CHI ‘20. Dec 2 2019 Carpentry Compiler by Chandra, Zach, and their collaborators from GRAIL featured on UW News! Nov 27 2019 Congrats to Talia, Alex, Dan, and Sorin on their CPP 2020 paper about analyzing the changes that proof engineers make to programs, specifications, and proofs in Coq! Nov 14 2019 Martin Kellogg won gold at the Student Research Competition at ASE with his work on compile-time detection of machine image sniping! Nov 10 2019 Congrats to Chenglong, Yu, Ras, Alvin, and collaborators on their POPL 2020 paper on visualization by example! Nov 7 2019 Congrats to Sorawee, James Bornholt and Emina for their VMCAI 2020 paper on fixing code that explodes under symbolic evaluation! Nov 3 2019 Max is giving an invited talk about Puddle at ICCAD! Oct 28 2019 Congrats to Luke, James Bornholt, Emina, Xi, and collaborators on their Best Paper Award at SOSP! Oct 23 2019 OctoML secured millions in funding! Congrats Luis, Jared, Zach, and all others involved outside of PLSE! Oct 22 2019 Josh will give a talk about his work on Theia with Jared, Doug, and Zach as part of SPLASH-E! Sep 18 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! Sep 3 2019 Talia, 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. July 29 2019 PLSE has two papers at SIGGRAPH ASIA 2019: Maaz and his collaborators for their work on lifting legacy image processing functions to high level DSLs, and Chandra, Zach and their collaborators for their work on compilers for carpentry. Congratulations! July 27 2019 Talia will be attending Rising Stars this year! July 21 2019 James W. joined Certora as their CTO! July 19 2019 Pavel joined Utah’s School of Computing as an Assistant Professor! July 11 2019 James Bornholt will be joining UT Austin as an Assistant Professor in 2020! July 1 2019 Congrats to Pavel, Zach, Mike, and their collaborator, Shoaib Kamil for their latest Cassius paper at OOPSLA 2019! Jun 1 2019 Congrats to Talia, Nate, John Leo, and Dan on their ITP paper: Ornaments for Proof Reuse in Coq. Talia will be talking about this and other proof-related work at the Coq Users and Developers Workshop! May 9 2019 Watch out world! Three PLSE undergrads are heading off to grad school in the fall: David to UCSD, Nate to Northeastern, and Jasper to CMU. Apr 24 2019 Doug will be heading to Brown in the fall as a lecturer. Congrats Doug! April 16 2019 James W., and Zach together with their collaborators have papers in CAV 2019! Congratulations!! Mar 18 2019 Chenglong got a paper into CVPR 2019! Mar 15 2019 Our very own John Toman defended his PhD! 🎓 Feb 20 2019 Bill’s paper on tracking floating point precision got into CONGA, where Zach will be giving the keynote! Feb 5 2019 Jasper’s paper on Inductive-Inductive Types in Cubical Type Theory got into FoSSaCS 2019. Dec 21 2018 Congrats to Doug, Mike, Zach, and their Systems collaborators Ellis, and Tom for their EuroSys 2019 paper on DSLabs! Dec 5 2018 Ras was named an ACM Fellow for his contributions to program synthesis. Congrats! Nov 21 2018 Chandra won the Adobe Research Fellowship! Nov 7 2018 Zach and Karl won a Facebook Continuous Reasoning Research Award for their work on continuous program verification. Nov 7 2018 Congrats to Max, Mangpo, Sam, and Ras for their ASPLOS 2019 acceptances! Oct 31 2018 Max’s work on Puddle was a runner-up for the Madrona Prize at the Allen School’s Industrial Affiliates event. Oct 28 2018 Sarah traveled all over, giving talks at UMass Amherst, PROBPROG, and UIST, as well as attending Rising Stars. Oct 26 2018 James gave a talk at NESVD about his work on distributed systems verification. Oct 26 2018 Chenglong and his collaborators won InfoVis Best Paper for their work on Draco! Oct 26 2018 Talia gave a talk at UCSD on her automated proof repair work. Oct 24 2018 Chandra gave a talk on her Reincarnate work at MPI-SWS. Oct 18 2018 Jared and his collaborators merged Relay, a new high-level IR, into the TVM machine learning stack. Oct 10 2018 Congrats to John and Dan! Their work on Concerto will appear in POPL 2019. Oct 4 2018 PLSE kicked off the Allen School autumn colloquium series with fantastic talks from John, Pavel, James B., James W., and Doug! Sep 29 2018 Pavel gave talks at both RacketCon and NPFL. Sep 25 2018 Amanda gave a talk at the Berkeley Institute of Design about inferring user interface structure. Sep 24 2018 Chandra gave a talk at ICFP on her work on Reincarnate. Aug 29 2018 Congrats to Ali, Ras and their collaborators for their paper on the TPS project accepted in the Cell Reports journal! Aug 16 2018 Congrats to Chenglong, James, Alvin, Emina, and Ras for their papers at OOPSLA 2018! Aug 6 2018 Congrats to Sarah, Ras and their collaborators for their paper on scraping distributed web data at UIST 2018! July 23 2018 Zach taught distributed system verification at the DeepSpec Summer School in Princeton! July 17 2018 Emina and Mike gave two keynotes for ISSTA in Amsterdam! July 16 2018 Pavel, Zach and their collaborators presented their paper on Tools for Floating-Point Computations at FM in Oxford, UK! July 8 2018 Zach gave the keynote for The Coq Workshop in Oxford, UK! June 20 2018 UW PLSE students had several great talks and papers at PLDI! Pavel on VizAssert, Alex on Herbgrind, and James and Doug on modular verification of distributed Systems! June 16 2018 Congrats to Shumo, Jared, Brendan Murphy, Alvin and their collaborators for their paper on SQL semantics in VLDB 2018! June 15 2018 Congrats to the Herbie team for releasing Herbie 1.2! June 11 2018 Beep! Brrrzzzz. Zach and Dan just received an NSF grant to continue their work on PL foundations for 3D printing. June 8 2018 Congrats to Stuart, Calvin, Eric, and Ali for graduating with PhDs! 🎓 June 1 2018Congrats to Calvin, Mike and Emina for Distinguished Paper at ICSE’18 for Cozy. May 17 2018 Beep! Brrrzzzz. Chandrakana, James, Taylor, Dan and Zach’s paper on Functional Programming for Compiling and Decompiling CAD has been accepted to ICFP 2018! May 11 2018 Congrats to Sam and his collaborators for their SecDev 2018 paper on Checked C! Apr 30 2018 Congrats to Martin and Mike for their ISSTA 2018 papers! Apr 15 2018 Jared’s ASPLOS 2017 paper with UCSB collaborators was selected as an IEEE Micro Top Pick! Apr 11 2018 Congrats to John and Dan for their ECOOP 2018 paper! Apr 10 2018 Congrats to Jared, Steven, Josh, Logan, Tianqi, and Zach for their MAPL 2018 paper! Apr 9 2018 Congrats to Eric, Pavel, Zach and their collaborators for their CAV, ITP and FM 2018 papers! Apr 5 2018 Joe won a Google PhD Fellowship! Apr 3 2018 Congrats to Max for receiving an NSF Honorable mention! Mar 11 2018 Congrats to Amy Ko for being recognized with the ICSE 2018 10-year most influential paper award! Mar 1 2018 Make sure to submit to PNW PLSE 2018! Feb 2018 Check out James Wilcox’s article in CACM on Highlights in Systems Verification! Feb 28 2018 Don’t miss James Wilcox presenting VerifiedFT at PPoPP 2018! Feb 12 2018 Congrats to Michael Ernst for earning the ISSTA 2018 Impact Paper Award! Feb 12 2018 Congrats to Pavel, Adam, Mike, Zach, Doug, James, and their coauthors on PLDI’18 acceptances. Come see the talks in Philly! Feb 4 2018 Joe is giving a TED talk on YOLO! Jan 24 2018 Œuf is now open source. Check it out on GitHub! Jan 19 2018 Zach won an NSF CAREER award! Jan 18 2018 James Bornholt receives a 2018 Facebook Fellowship. Jan 13 2018 James Wilcox will have a paper at PPoPP 18: VerifiedFT: A Verified, High-Performance Dynamic Race Detector Dec 11 2017Congrats to Amanda and Amy for their acceptance of their paper “Rewire: Interface Design Assistance from Examples” to CHI ‘18. Nov 19 2017 UW PLSE will be out in force at POPL 2018! We have three papers at POPL: James and Zach (with Ilya Sergey) on a logic for distributed systems verification Emina (with Northeastern PRL) on Typed Rosette Ras (with Kartik Chandra) on type system verification and synthesis We also have two papers at CPP: Talia, Nate, and Dan (with John Leo) on automated proof repair Eric, Stuart, James, Zach, and Dan on verified extraction of verified code And one at OBT! Max and Jared on Extensible Semantics for Fluidics. See you in Los Angeles! Oct 7 2017 Mangpo will be giving a talk on her work High-Coverage Hint Generation for Racket Programming Assignments with Berkeley colleagues at RacketCon 2017! Oct 3 2017 Rashmi Mudduluru will be giving a talk on her work Lasso Detection Using Partial State Caching with MSR colleagues at FMCAD 2017! Sept 7 2017Amy just received a grant to investigate different programming strategies together with Thomas LaToza. Congrats, Amy and Thomas, and we’re excited to see the results of the work. Aug 11 2017Congrats on 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 2017Congrats to Julie for her Onward! 2017 paper on Internet of Things automation. Jul 22 2017Joe’s YOLO9000 just won Best Paper Honorable Mention at CVPR’2017! Jul 19 2017Cosette, 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 2017At this year’s 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 2017Martin 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 2017Congratulations to 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 2017Congratulations 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 1 2017UW PLSE has two papers in 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 2017Herbie 1.1 has been released. Good work, Pavel, Jason, Alex, and Zach! Apr 27 2017Mike 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 2017You cannot miss 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 2017Congratulations to Chandrakana, Dan, and their coauthors for their paper, “Debugging Probabilistic Programs”, at MAPL 2017. Apr 18 2017Congratulations to Alvin and Emina on receiving CAREER awards from the NSF. Apr 15 2017Remy (Yisu) Wang, Zhen Zhang, and Rashmi Mudduluru will be joining UW PLSE next year. Welcome! Apr 15 2017Congrats to 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 2017Congratulations to Sarah and Mangpo for their paper, “Data-Driven Synthesis of Full Probabilistic Programs”, at CAV 2017. Mar 7 2017Congratulations to 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 2017Joe’s YOLO9000 has been accepted to CVPR’17: better, faster, strong object detection with a single net. Feb 24 2017Congratulations 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 2017James 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 2017Zach gave a talk at the University of Utah on floating point at the University of Washington: Herbie, Herbgrind, and FPBench. Jan 16 2017Congratulations Mike on winning the ICSE 2017 Most Influential Paper award for his work on feedback-directed random test generation. Jan 16 2017Jared helped give a tutorial on his work adding native compilation to the LEAN theorem prover. Check it out! Dec 14 2016Evaluating & 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 2016Melissa Galloway was featured in UW CSE’s Undergrad Spotlight. Dec 9 2016Congratulations to Chris Mackie and Nate Yazdani, honorable mentions for 2017 CRA Outstanding Undergraduate Researchers! Nov 17 2016Calvin 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 2016Congratulations to Helgi Sigurbjarnarson, 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 2016Amy Ko gave a keynote A human view of programming languages at SPLASH 2016 Oct 5 2016Luke will present a poster on his and Jared’s work on bootstrapping a secure eBPF compiler in Coq at OSDI 2016! Sep 18 2016Emina Torlak gave the keynote at RacketCon2016 Aug 30 2016Chandrakana and Mike’s work on program analyses for smart home security has been accepted to PLAS 2016! Aug 19 2016UW had eight (!) papers accepted to the 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 2016Congratulations to everyone accepted to OOPLSA 2016! Cassius, Bagpipe, Ringer, and Calvin’s work with Samsung Research America Jul 27 2016Ivan a UW alum, Yuriy a UW postdoc alum, Patty, and Mike’s paper, Debugging Distributed Systems appeared in CACM August 2016 issue! Jul 25 2016Talia, Franzi, and Dan’s paper, “AUDACIOUS: User-Driven Access Control with Unmodified Operating Systems” to appear in ACM CCS 2016! Jul 20 2016Staccato won both the Distinguished Artifact and Distinguished Poster awards at ECOOP 2016. Congrats, John and Dan! Jul 5 2016PLSE swept the best student paper awards at 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 2016Ras wins an Influential Paper Award from ISCA for his 2001 paper Focusing Processor Policies via Critical-Path Prediction. May 9 2016Konne will be presenting Bagpipe’s BGP formalization in Brazil at NetPL 16. May 7 2016Recent PLSE alum and soon-to-be Cornell professor Adrian Sampson won UW CSE’s William Chan Memorial Dissertation Award! May 4 2016Alvin won the DoE Early Career Award! Apr 25 2016Alvin and his collaborators from MIT, Stanford, and Barefoot Networks’ work on programmable switches was accepted to SIGCOMM 2016. Apr 18 2016Ivan, 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 2016Mike, Alberto, Alessandra, and Mauro’s paper on Automatic generation of oracles for exceptional behaviors was accepted to ISSTA 2016. Apr 16 2016Mike, Damiano, Massimo, and Fausto’s paper on Semantics for locking specifications was accepted to NFM 2016. Apr 15 2016Neutrons was accepted to CAV’16. If you’re there, come to the talk to learn about verifying a neutron therapy machine. Mar 29 2016Congratulations to Talia Ringer and Amanda Swearngin for winning NSF graduate fellowships! Mar 1 2016John 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 2016YOLO has been accepted to CVPR’16. Congrats to Joe! Feb 26 2016Xi’s work on undefined behavior detection appears in this month’s Communications of the ACM. Feb 23 2016Emina Torlak won the AITO Dahl-Nygaard prize and the Sloan Fellowship! Jan 20 2016We have three papers accepted to 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 2016Mike and Javier’s paper on Locking discipline inference and checking was accepted to ICSE 2016. Jan 11 2016Konstantin Weitz was a finalist for the Facebook Fellowship Program! Dec 21 2015Pavel Panchekha won the Adobe Research Fellowship. Congrats! Dec 17 2015Daryl Zuniga won the prestigious UW Mary Gates Scholarship and an Honorable Mention for the CRA Undergraduate Research Award! Dec 4 2015Our paper on verifying Raft in Verdi will appear at CPP 2016! Nov 17 2015PLSE has 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 2015Alvin Cheung won MIT’s George M. Sprowls Award for outstanding PhD theses in computer science! Oct 5 2015James, Emina, Dan, and Luis’s paper on optimizing program synthesis with metasketches has been accepted to POPL 2016. Sep 17 2015Sam just won the Lockheed Martin Award for Best Engineering Project at the Young Software Engineer Awards. Woohoo! Aug 3 2015PLSE sent four papers to OOPSLA this year: on object-oriented constraint solving, constraint programming, synthesis of layout engines, and a framework for synthesis. Jul 20 2015The PLSE group has 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 2015Timelapse has been accepted to UIST’15. Come find out about diffing web interfaces. Jun 16 2015The Herbie and Verdi projects killed it at PLDI’15. Didn’t make the talks? Check out the project pages. May 7 2015The Herbie paper won Distinguished Paper at PLDI. Make sure you go see the talk! May 4 2015UW PLSE at SNAPL’15: a dependency case language for a neutron therapy machine, and hardware-software co-design! Apr 7 2015Ras Bodik is joining UW PLSE. We’re so incredibly excited to work with him! Mar 31 2015Congrats Doug Woos and Pavel Panchekha, two students in UW PLSE, who just became NSF fellows. Jan 18 2015Verso presenting first steps toward low-level optimizations in CompCert, at CoqPL’15. See all News posts Projects More projects » Rosette A solver-aided programming language for Racket. Grisette A monadic library for symbolic evaluation. Herbie Automatically improve the accuracy of floating point expressions. Checker Framework Extend the Java type checker to catch more bugs. Exo Exocompilation for productive programming of hardware accelerators. Tea Automating statistical analysis Tisane Formalizing statistical models from conceptual relationships egg Fast and flexible e-graphs. egglog e-graphs + datalog! ruler Rewrite Rule synthesis. aleph A truly high-level quantum programming language. Tensat Equality saturation for tensor graph superoptimization Potpie The first proof compiler that has been proven correct. Free Join Unifying worst-case optimal and traditional joins Lakeroad More complete synthesis for specialized FPGA primitives via program synthesis. Glenside A pure DSL for mapping tensor programs to accelerators via equality saturation. Faculty Gilbert Bernstein Rastislav Bodik Luis Ceze Michael D. Ernst Dan Grossman René Just Amy J. Ko Andrew Lumsdaine Zachary Tatlock Matt Wang James Wilcox Postdocs Haobin Ni Ph.D. students Alexandra Michael Amy Zhu Andres Paz Anjali Pal Audrey Seo Benjamin Kushigian Dan Cascaval Edward Misback Elli Beres Gus Smith Hannah Potter Haoran "Hurry" Peng James Yoo Jasper Tran O'Leary Moses Lurbur Nat Hurtig Oliver Flatt Reshabh K Sharma Ryan Zambrotta Sam Kaufman Sirui Lu Yihong Zhang M.S. students Alex Fischman Kirsten Graham Matthew Shang Staff Suzanne Millstein Mark Roberts Affiliate Faculty Maaz Ahmad Chandrakana Nandi Emina Torlak Xi Wang Alan Borning Undergraduates Ken Matsui Kenneth Yang Rich Chen Sascha Kehrli Stanley Yang Yash Mathur Ivory Wang Ph.D. Alumni Maaz Ahmad Adobe Jonathan Aldrich CMU Gail Alverson Microsoft Tom Bergan Google Ivan Beschastnikh UBC James Bornholt UT Austin BJ Burg Apple Brad Chamberlain Cray William Chan 1972-1999 Sarah Chasins Berkeley Kingsum Chow Alibaba Shumo Chu UCSB Sung K. Chung Jeff Dean Google Joe Devietti Penn Robert Duisburg UW CGS Laura Effinger-Dean Google Michael Ernst UW Bjorn Freeman-Benson InVisionApp Colin Gordon Drexel University Bill Griswold UCSD David Grove IBM Research Brandon Holt Apple Eunice Jun UCLA Martin Kellogg NJIT Miryung Kim UCLA Ali Sinan Köksal Google Benjamin Lerner Northeastern Sorin Lerner UCSD Vass Litvinov Cray Calvin Loncaric Oracle Gustavo Lopez Steven Lyubomirsky OctoML John Maloney Amir Michail UNSW Todd Millstein UCLA Markus Mock Google Kristi Morton Eric Mullen Google Gail C. Murphy U. British Columbia Kıvanç Muşlu MSR Chandrakana Nandi Certora Julie Newcomb Qualcomm Michael Noth Pavel Panchekha Utah Daniel Perelman MSR Stuart Pernsteiner Galois Matthai Philipose MSR Mangpo Phothilimthana Google Alex Polozov MSR Sorawee Porncharoenwase AWS Will Portnoy Microsoft Joe Redmon Michael Ringenburg Cray Talia Ringer U. Illinois Jared Roesch OctoML Co-founder L. Denise Pinnel Salisbury Adrian Sampson Cornell Michael Sannella Vibha Sazawal U. Maryland Todd Schiller MOKA Marty Sirkin Kevin Sullivan U. Virginia Amanda Swearngin Apple John Toman Certora Jacob Van Geffen Veridise Michael VanHilst Nova SE U. Luis Vega OctoML Chenglong Wang Microsoft Remy Wang UCLA Konstantin Weitz Google Doug Wiebe Apple James Wilcox UW Max Willsey Berkeley Molly Wilson Benjamin P. Wood Wellesley Doug Woos Brown Tao Xie U. Illinois Yoshi Yamane Sai Zhang Google William A. Zorn Intel M.S. Alumni Jenny Abrahamson Airbnb Rajas Agashe Block Paulo Barros Jackson Cannon Redacted Andrew Cheung Forrest Coward Microsoft Mark Davis Stephanie Dietzel Salesforce Kellen Donohue Palantir Seth Fowler Qualcomm Sagar Jain Google Darioush Jalali Vimala Jampala Microsoft Adam Jiang Oracle Marisa Kirisame Utah Edward Lu Google Christopher Mackie AWS Ardi Madadi MPI Rashmi Mudduluru Deric Pang Figma Spencer Pearson Marlena Preigh Mason Remy Microsoft Thia Richey UPenn Tyler Rigsby Google Alex Sanchez-Stern UMass Thomas Schweizer Meta Lexin Shan Zachary Stein Eric Spishak Google Liviu Tancau Google Brian Walker Google Logan Weber MIT Elliott Zackrone AWS Yihong Zhang UW Edit on GitHub — Computer Science & Engineering at the University of Washington

en

en

1730501941

https://uwplse.org

Modifier votre site ?

Que fais-tu?