NaNofuzz to TestLoop: A Journey from Empirical to Theoretical Research (and back again)
Speaker: Matthew C. Davis
Matthew C. Davis is a Software Engineering PhD student at Carnegie Mellon University’s School of Computer Science and is advised by Dr. Brad A. Myers and Dr. Joshua Sunshine. Matthew's research focuses on interventions that aim to improve the human ability to build and test useful software and is motivated by his experience in industry as a software engineer and global engineering director.
Abstract
Software testing labor in the United States cost an estimated $47-86 billion in 2021. Since the 1970s, Automatic Test sUite Generators (ATUGs) have aimed to make it easier for developers to generate effective test suites. The vast majority of ATUGs have aimed to improve measures such as code coverage or mutants killed. But improving such measures does not necessarily imply that these tools actually help users efficiently create bug-finding test suites. In this talk, we discuss two of our experimental ATUGs, NaNofuzz and TerzoN, that are based on a human-centered design process. We also discuss TestLoop, a theoretical process model of the developer's test suite generation process that is based on empirical observations of developers generating test suites. We describe various ways in which our empirical research informs and refines our theoretical research---and vice-versa. We also share tips for researchers who want to build and use software engineering theory in their own work.
A functional approach to formalizing Bit Vector representations
Speaker: Katherine Philip
Katherine Philip is a PhD student and Portland State University working in the intersection of systems programming and PL.
Abstract
We study the compilation process for a parametric Bit n type, where n can be instantiated with any natural number to describe bit vectors of width n. These bit vector types support use cases such as bit fields, which are commonly used in low-level systems software to conform to third-party hardware and operating system specifications.
I will share our work-in-progress in formalizing bit vector representations in terms of high-level functional constructs, which allows us to take advantage of well-understood properties, as well as piece together a correct compilation strategy using simple equational reasoning.
Freer Arrows
Speaker: Grant VanDomelen
Grant is a PhD student at Portland State University researching programming languages and program verification, especially with functional programming.
Abstract
Freer arrows are an analogue to freer monads for writing DSLs and programs which benefit from better static analysis at the expense of some expressiveness. I will present our construction of a few variations of freer arrows in Haskell and Rocq, along with some of their interesting properties.
The Memorist Tale: Once Annotated Lazy Program Cost is Fun
Speaker: Yao Li
Yao Li (He/Him) is an assistant professor of computer science at Portland State University. His main research area is in functional programming, interactive theorem proving, and program verification. His current research focuses on using interactive theorem provers to verify existing programs written without verification in mind. He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich.
Abstract
Just because one or two alternative cost semantics to lazy evaluation is not enough, I am going to talk about a third one: the memorist semantics. It is a novel semantics to analyse the cost of lazy programs by tracking the cost of computing each component of a term once and for all. This approach annotates each component of a term with fine-grained cost information and usage sets, enabling compositional reasoning about cost without duplicating computation or requiring demand knowledge upfront. This allows us to compute costs once and reuse them across different demand scenarios. We formalize the memorist semantics in the Rocq Prover and verify its soundness with respect to the existing clairvoyance semantics. This is joint work with Xing Li, Peter Schachte, and Christine Rizkallah (The University of Melbourne).