UW CSE’s Programming Languages and Software Engineering (PLSE) group advances fundamental research and develops solutions to real-world problems while eschewing arbitrary boundaries within the field. Our collaborative approach and emphasis on both theory and practice set us apart from many of our peers. With four new faculty since 2013, we are growing in many directions.

PLSE faculty and students benefit from strong ties to the local software community and interaction with researchers from Cray, Microsoft Research, NVIDIA, Pacific Northwest National Laboratory, and others. Our work encompasses the spectrum of programming languages and software engineering, including programming environments, program analysis, language design, run-time systems, compilers, testing, verification, and security. Several of us also participate in UW CSE’s inter-disciplinary SAMPA group, which pursues research projects focused on making computer systems faster, more reliable and more energy efficient.

We leverage theory, design, and experimentation to build useful software artifacts that benefit both the developer community and end users. Our research has led to advances in type systems, software testing, parallel and concurrent programming, formal verification, program synthesis, approximate computing, web programming, and more. UW CSE has a proud history of producing graduates with strong records of accomplishment in programming languages and software engineering. Our Ph.D. alumni go on to prestigious industry and academic positions, and many undergraduates and Masters students do great work with us before moving on to employment with leading companies or entering top graduate programs.

We generally have so much going on that we struggle to keep an up-to-date list of projects available publicly. Here is just a handful of our many recent projects that can give a sense of our range of interests:

• Rosette: A new solver-aided language that extends the Racket language with facilities for program synthesis, verification, debugging and angelic execution, using SAT and SMT solvers. Rosette makes it easy to develop new solver-aided languages for specific domains, by simply writing an interpreter or a library.
• Verified software infrastructure: Being able to build software along with a machine-checkable proof of correctness for key system properties is becoming a reality. Building on our past successes in building formally verified web browsers and compiler-optimization frameworks, we are now working on domains such as binary-level transformations, distributed systems, and floating-point computations.
• Testing tests: A quality test-suite is fundamentally important for any software-engineering project, but it is far from settled how to efficiently create a quality test suite or even how to define and measure the quality of a test suite. Our recent work has shed new light on both questions with faster, more scalable techniques for generating quality tests as well as new analyses and benchmarks for measuring the effectiveness of a testing technique.
• Pluggable type-checking: A pluggable type-checker refines (strengthens) the built-in type system of a programming language. We continue to develop infrastructure to make it easy to define custom type-checkers for novel program properties, which in turn helps developers find defects – or prove their absence – statically. We have developers checkers for several such properties, including errors related to format strings, graphics threads, regular expressions, and much more.