6 papers
Using LLMs to Adjudicate Static-Analysis Alerts with Error Reduction Techniques
William Klieber, David Svoboda, Lori Flynn +1
Static analysis is widely used for finding security weaknesses in source code before deployment, but it often produces far more alerts than analysts can review. We study how well l…
Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
Shirley Yu, Ruben Martins
Program verification is crucial for software correctness, but producing fully verified programs remains difficult in practice. This paper studies whether implementation structure a…
SPELL: Synthesis of Programmatic Edits using LLMs
Daniel Ramos, Catarina Gamboa, Inês Lynce +3
Library migration is a common but error-prone task in software development. Developers may need to replace one library with another due to reasons like changing requirements or lic…
Inferring multiple helper Dafny assertions with LLMs
Ãlvaro Silva, Alexandra Mendes, Ruben Martins
The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use o…
Can Large Language Models Autoformalize Kinematics?
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj +3
Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, befor…
Hypergraph-Guided Regex Filter Synthesis for Event-Based Anomaly Detection
Margarida Ferreira, Victor Nicolet, Luan Pham +4
We propose HyGLAD, a novel algorithm that automatically builds a set of interpretable patterns that model event data. These patterns can then be used to detect event-based anomalie…