27 citations · 34 across the 9 of their papers we have counts for
10 papers
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Eric Spencer, Arslan Bisharat, Brian Ortiz +6
TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fa…
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
Arslan Bisharat, Eric Spencer, Brian Ortiz +8
Large language models increasingly write TLA formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblanc…
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Arslan Bisharat, Brian Ortiz, Eric Spencer +5
TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertis…
SysLLMatic: Large Language Models are Software System Optimizers
Huiyun Peng, Arjun Gupte, Ryan Hasler +7
Automatic software system optimization can improve software speed, reduce operating costs, and save energy. Traditional approaches to optimization rely on manual tuning and compile…
Can Large-Language Models Help us Better Understand and Teach the Development of Energy-Efficient Software?
Ryan Hasler, Konstantin Läufer, George K. Thiruvathukal +5
Computing systems are consuming an increasing and unsustainable fraction of society's energy footprint, notably in data centers. Meanwhile, energy-efficient software engineering te…
WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
Konstantin Läufer, Gunda Mertin, George K. Thiruvathukal
Background: In this paper, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), in…
Snapshot Metrics Are Not Enough: Analyzing Software Repositories with Longitudinal Metrics
Nicholas Synovic, Matt Hyatt, Rohan Sethi +11
Software metrics capture information about software development processes and products. These metrics support decision-making, e.g., in team management or dependency selection. How…
On the Interaction of Object-Oriented Design Patterns and Programming Languages
Gerald Baumgartner, Konstantin Läufer, Vincent F. Russo
Design patterns are distilled from many real systems to catalog common programming practice. However, some object-oriented design patterns are distorted or overly complicated becau…
Tests as Maintainable Assets Via Auto-generated Spies: A case study involving the Scala collections library's Iterator trait
Konstantin Läufer, John O'Sullivan, George K. Thiruvathukal
In testing stateful abstractions, it is often necessary to record interactions, such as method invocations, and express assertions over these interactions. Following the Test Spy d…
Metrics Dashboard: A Hosted Platform for Software Quality Metrics
George K. Thiruvathukal, Shilpika, Nicholas J. Hayward +1
There is an emerging consensus in the scientific software community that progress in scientific research is dependent on the "quality and accessibility of software at all levels" (…