Monday, September 11, 2023, 3:30 – 5pm

3:30 pm
► Madeline Endres, Ph.D. Student, Computer Science and Engineering, University of Michigan
— Cognitive training and psychoactive substances: two different lenses into
developer productivity and wellbeing

"Can technical reading training make students better at programming? Do professional developers think cannabis use leads to more creative programs?" This talk considers two lenses for approaching programmer productivity and wellbeing. First, we measure and leverage the cognition of programming to help novices become experts faster. Second, we explore the role of external factors on programming productivity, with a particular focus on the impact of psychoactive substance use by professional developers. Finally, we conclude with a brief discussion of how interdisciplinary approaches, specifically those from psychology and medicine, can provide insight into human-factored software engineering problems.

Madeline Endres is a final year computer science PhD student at the University of Michigan where she is advised by Westley Weimer. Her research interests lie at the intersection of Software Engineering and human factors, where she explores programmer productivity and wellbeing. Current projects include using medical imaging techniques to learn more about the cognitive basis of programming, building tools and methods to support developers to write more correct code faster, and studying the impact of psychoactive substances on software developers. When she is not doing research, she enjoys cooking, biking, and playing with her cat, Cleo.

4:00 pm
► Ian Dardik, Ph.D. Student in Software Engineering, Software and Societal Systems Department
— Model Checking TLA+ via Recursive Decomposition

TLA+ is a formal specification language used in both academia and the industry for designing reliable software systems. TLA+ owes much of its success to the TLC model checker, a program that automatically verifies TLA+ specifications so users do not need to write proofs. However, TLC—as well as model checkers in general—suffer from the state explosion problem in which model checking times grow exponentially with the size of a specification. In our work, we propose a novel model checking algorithm that aims to reduce state explosion by recursively decomposing large specifications into smaller, more manageable specifications. We have implemented our technique in a TLA+ model checker we call Decomp-Verify. Preliminary results show that the runtime for Decomp-Verify is competitive with TLC for a benchmark suite of distributed protocols; Decomp-Verify even outperforms TLC in several cases.

4:30 pm
► Catarina Gamboa, Ph.D. Student, Software Engineering, Software and Societal
Systems Department
— Exploring the Barriers in Liquid Types

Software reliability is a growing concern in software development, leading developers to adopt techniques like strong-type systems to detect bugs early in development. Liquid types, an extension of type systems with expressive predicates, can catch diverse bugs. However, they are yet to be widely used. This work in progress investigates the current usability issues and barriers by employing qualitative research with three groups: experts, former users, and newcomers, and focusing on LiquidHaskell, the most mature implementation of Liquid Types. By exploring these perspectives, we aim to identify and find ways to address usability barriers in liquid types.

In Person and livestream. See announcement.

Event Type: Talks
Room Number: In Person and Virtual - ET
Building: TCS Hall 358 and Livestream
Speaker's Name: MADELINE ENDRES, IAN DARDIK, CATARINA GAMBOA
Speaker's Professional Title: Ph.D. Student, University of Michigan
Talk Title: There Talks
For More Information: jtliang@andrew.cmu.edu
Affiliations: Software and Societal Systems Department (S3D)
Event Website Title: Series Website
Event Website URL: s3d.cmu.edu…