When choosing a programming language to use for a project—or when implementing one—there are many considerations to keep in mind. One of those is whether or not the programming language uses any sort of garbage collection. Today, I’m going to talk about one method of garbage collection that we can implement ourselves fairly easily: two-space copying garbage collection.
In this post, I will relate some of the key findings and lessons learned in our 2024 ISSTA publication Equivalent Mutants In The Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs (that’s a mouthful so I’ll just call it EMIW). In EMIW, my co-authors and I performed an extensive manual analysis of mutants generated for Java programs to gain insight into the types of equivalent mutants generated for real-world code. We found that a number of equivalent mutants follow simple patterns. We used these patterns to write simple, efficient static analyses, which we call suppression rules, to suppress equivalent mutants before the are ever generated. We added the suppression rules to the Major mutation framework and will refer to Major with suppression rules as EMS.
Hi friends! I’m back to discuss more accessibility improvements we’ve made to the PLSE website: how we found more issues, how we fixed them, and how we’ll (hopefully) not make these same mistakes in the future! In particular, this post touches on running automated browser tests across our entire website to flag specific types of accessibility issues. Along the way, we’ll learn about some specific web accessibility standards and how to implement them not-poorly!
Do you wonder what it’s like to do research at PLSE? If you are a student without prior research experience, the PLSE lab may seem intimidating at first. However, PLSE supports a diverse body of undergraduates working on various research topics, from software engineering questions like “How good is a test suite” all the way to compilers for hardware. Our undergrads play an integral part in the PLSE community, growing with the lab and constantly making PLSE a better place.
For the last 8 months, I’ve been working on Odyssey, a tool for analyzing floating point expressions by integrating floating point tools into one dynamic workbench. One of our big milestones is approaching, as we’ll present Odyssey at the Supercomputing Conference (SC 2024) in less than a week.
I recently submitted a data reproduction artifact accompanying our paper “Verifying the Option Type with Rely-Guarantee Reasoning.” There are things that I wish I had done from the get-go next time, so I’m writing them down in this post. Hopefully, you’ll find some of the things I write here useful in creating your own data artifacts!
Before I ever started my PhD, I could have recited to you the Curry-Howard Isomorphism: proofs are programs, and programs are proofs. But it was only when I started working on proof compilation in the interactive theorem prover Rocq (formerly known as Coq) that I feel that I truly understood it – along with why it works, why theorem provers work, and all sorts of cool tricks and connections you can use.
If you saw my last blog post, you know that I work on design tools for knitting unusual things. Today I’m introducing my new project, which is a design tool to support knitting things in unusual ways. I’m also introducing my new amazing collaborator, Marlena!
Once UW kicks off the school year at the end of this month, I’ll officially be a second-year PhD student It’s a scary, yet exciting, thought! There will be loads of new incoming students, interesting research, and many surprises in store! This is also the perfect time to think critically about my goals in the PhD. One of them is building a larger theme for my research. I’m not committing to a thesis topic here. Rather, I’m searching for a concise, ideally pithy, way to describe my research. This blog post is a trial run for one theme: Real Analysis through the lens of Programming Languages.
This summer, I’ve been interning at Sandia National Labs, working on extending CompCert for concurrent programs. We represent program states as a list of threads t :: ts and a memory state m. Much of my work relates to trying to formalize safety properties of the memory state as the program steps. This is my first time using Rocq outside of CSE 505, so I thought it would be interesting to write up some reflections on the experience.