Fall 2024¶

Fall 2024 What is Research Slides

Abstracts for Fall 2024 Talks

Dec 6 Dr. Zhuojun Duan - Linking Pollution to Thunderstorm Formation Using Data Mining

Abstract: This project conducts a multi-variable investigation of thunderstorm environments across two distinct geographic regions to explore the aerosol and thermodynamic conditions associated with thunderstorm initiation. A 12-year dataset of cloud-to-ground (CG) lightning flashes was used to reconstruct thunderstorms within a 225 km radius centered on the Washington, D.C., and Kansas City metropolitan areas. A total of 196,836 and 310,209 thunderstorms were identified for Washington, D.C., and Kansas City, MO, respectively. Hourly meteorological and aerosol data were integrated with the thunderstorm event database.

Our findings reveal that warm-season thunderstorm environments under benign synoptic conditions differ significantly in thermodynamics, aerosol properties, and concentrations between the Washington, D.C., and Kansas City regions. Despite these differences, thunderstorm intensity—measured by flash counts—appears to be governed by similar thermodynamic-aerosol interactions across both regions. Specifically, statistically significant positive relationships were observed between convective available potential energy (CAPE) and flash counts. Furthermore, aerosol concentration emerged as a more critical factor for lightning enhancement than particle size.

Nov 22 Dr. Bradley McCoy - Guarding

Abstract: Given a polyhedral terrain and a set of guard points, a point q on the terrain is guarded if there is at least one point in the guard set that sees q. In this talk, we consider variations of this problem. We will look back at classical guarding results such as Chavatal's art gallery theorem. We will share recent results on guarding terrains with segments. Then, we will look forward to several open problems. The open problems have a low barrier of entry. So, please bring something to write with and be ready to participate.

Oct 25 Will Morris - Bringing Robustness Analysis to TLA+ and Why it Matters

Abstract: Tired of missing subtle edge cases in your programming assignments? Come learn how to easily prove your algorithms are correct! In response to today’s increasingly complex software systems, interest is growing in formal specification languages that allow users to prove properties of high-level models of their systems. In this presentation, I will examine the merits of model checking with a special emphasis on the TLA+ specification language. I will then explore the limitations of model checking and how the notion of software robustness can address those limits. Finally, I will detail my efforts to elevate robustness to a first-class citizen of the TLA+ language. I will also talk about my experience in the (paid) Research Experience for Undergraduates program under which I did this research, with an eye towards students who might consider applying.