5 citations · 6 across the 11 of their papers we have counts for
11 papers
ProofPulse: Interactive Proof Coverage Analysis for Dafny
Álvaro F. Silva, Ruben Martins, Alexandra Mendes
Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak sp…
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…
Security Vulnerability Detection with Multitask Self-Instructed Fine-Tuning of Large Language Models
Aidan Z. H. Yang, Haoye Tian, He Ye +2
Software security vulnerabilities allow attackers to perform malicious activities to disrupt software operations. Recent Transformer-based language models have significantly advanc…
Revisiting Unnaturalness for Automated Program Repair in the Era of Large Language Models
Aidan Z. H. Yang, Sophia Kolak, Vincent J. Hellendoorn +2
Language models have improved by orders of magnitude with the recent emergence of Transformer-based Large Language Models (LLMs). LLMs have demonstrated their ability to generate n…
On Repairing Natural Language to SQL Queries
Aidan Z. H. Yang, Ricardo Brancas, Pedro Esteves +5
Data analysts use SQL queries to access and manipulate data on their databases. However, these queries are often challenging to write, and small mistakes can lead to unexpected dat…
Large Language Models for Test-Free Fault Localization
Aidan Z. H. Yang, Ruben Martins, Claire Le Goues +1
Fault Localization (FL) aims to automatically localize buggy lines of code, a key first step in many manual and automatic debugging tasks. Previous FL techniques assume the provisi…