34 citations · 54 across the 8 of their papers we have counts for
8 papers · 1 filter
Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability
Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes +2
Formal specifications play a central role in ensuring software reliability, yet automatically synthesizing high-quality specifications remains difficult and often requires domain e…
What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner +3
Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified re…
Toward Automated Validation of Language Model Synthesized Test Cases using Semantic Entropy
Hamed Taherkhani, Jiho Shin, Muhammad Ammar Tahir +3
Modern Large Language Model (LLM)-based programming agents often rely on test execution feedback to refine their generated code. These tests are synthetically generated by LLMs. Ho…
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu +11
Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction an…
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu +10
Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generatio…
DafnyBench: A Benchmark for Formal Software Verification
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach +7
We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such a…
Towards AI-Assisted Synthesis of Verified Dafny Methods
Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma +1
Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises,…
Test Smell: A Parasitic Energy Consumer in Software Testing
Md Rakib Hossain Misu, Jiawei Li, Adithya Bhattiprolu +3
Traditionally, energy efficiency research has focused on reducing energy consumption at the hardware level and, more recently, in the design and coding phases of the software devel…