PNW  PLSE  2023

Parallel Programming with Chapel (Slides | Recording)

Brad Chamberlain, Hewlett Packard Enterprise

Generating Test Oracles with Tratto

Elliott Zackrone, University of Washington

Linear Types for Systems Verification (Slides)

Jialin Li, University of Washington

Verified Program Construction (Recording)

Shaz Qadeer, Meta

Proof Compilers (Recording)

Audrey Seo, University of Washington

Interactive Code Generation with User-Intent Formalization (Recording)

Shuvendu Lahiri, Microsoft Research 

Hot Takes on Machine Learning for Program Analysis (Recording)

Unless you have been living under a rock, you have noticed the general popularity of AI/Machine Learning over the last few years.  These techniques have also made their way to program analysis research. Even though I see my research as focussing on classical static analysis techniques, it turns out that I've applied Machine Learning techniques in my own work as early as 2008. This year, my students and I have done work on Rust bug classification; code representations for method name/return type prediction in WebAssembly; and formally verifying Copilot-generated code. I'll survey less-recent and more-recent applications of machine learning in program analysis, present overviews of my work, and tell you all about my opinions about what machine learning is good for in the domain of static analysis.

Bio: Patrick Lam is going on a West Coast (North America) tour this May and visiting friends and colleagues, both in the research community and otherwise. He is an Associate Professor at the University of Waterloo and is interested in software engineering applications of static analysis techniques. He is also planning to get out into the North American mountains before a visit to the Victoria University of Wellington (New Zealand) on his upcoming sabbatical. Ask him about New Zealand!

Analysis and Synthesis of Musical Counterpoint (Slides)

John Leo,  Halfaya Research

Untangling Git Commits

Thomas Schweizer, University of Washington

CodaMOSA (Recording)

Caroline Lemieux, University of British Columbia

Automated Type Inference in Python (Slides | Recording)

Jifeng Wu, University of British Columbia

Lakeroad: Hardware Compilation via Program Synthesis (Slides | Recording)

Gus Smith, University of Washington

Semantic Assertions

Ashish Tiwari, Microsoft Research

Fully In-Place Functional Programming (Recording)

Daan Leijen,  Microsoft Research

Programming Abstractions for Quantum Computing (Slides | Recording)

Jennifer Paykin, Intel

Project Zeta (Recording)

Nikhil Swamy, Microsoft Research

A DSL Framework for F* (Recording)

Guido Martinez, Microsoft Research

Compiler Mitigations for Security Risks (Recording)

Alexandra Michael, University of Washington

Wasm-check

Adam Geller, University of British Columbia

Checked C (Slides | Recording)

David Tarditi, Secure Software Development Project

An Anti-Capitalist, Multicultural, Accessible Programming Language (Recording)

Amy Ko, University of Washington

Code-Aware Agents for Cloud Security

Patrice Godefroid, Lacework

Live, Rich, and Composable Programming

Josh Horowitz, University of Washington

Generating High-Performance Communication Kernels (Slides | Recording)

Madan Musuvathi, Microsoft Research

Generating Formally Verified Parsers with EverParse (Slides | Recording)

Tahina Ramananandro, Microsoft Research

Rich Specifications for Ethereum Smart Contract Verification (Recording)

Alexander Summers, University of British Columbia

Verus: Verifying Rust Programs (Recording)

Chris Hawblitzel, Microsoft Research