FormalSpecCpp: A Dataset of C++ Formal Specifications Created Using LLMs
This program is tentative and subject to change.
This paper introduces FormalSpecCpp, a dataset to address the critical need for standardized verification of the C++ program specifications. To the best of our knowledge, this is the first comprehensive collection of C++ programs with well-defined formal specifications. Additionally, we present a specification translation approach that employs rule-based prompting strategies to handle critical aspects of the target programming language such as appropriate type selection, safety checks, and assertion mapping. This work provides a standardized dataset for evaluating specification inference tools and explores how Large Language Models (LLMs) can support automated specification generation across various programming languages. We envision this benchmark advancing research on program verification, automated testing, and specification inference for C++ programs and providing guidelines for using LLMs to generate specifications for other programming languages.
This program is tentative and subject to change.
Tue 29 AprDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 10mTalk | Automatic High-Level Test Case Generation using Large Language Models Technical Papers Navid Bin Hasan Bangladesh University of Engineering and Technology, Md. Ashraful Islam Bangladesh University of Engineering and Technology, Junaed Younus Khan Bangladesh University of Engineering and Technology, Sanjida Senjik Bangladesh University of Engineering and Technology, Anindya Iqbal Bangladesh University of Engineering and Technology Dhaka, Bangladesh | ||
14:10 10mTalk | Prompting in the Wild: An Empirical Study of Prompt Evolution in Software Repositories Technical Papers Mahan Tafreshipour University of California at Irvine, Aaron Imani University of California, Irvine, Eric Huang University of California, Irvine, Eduardo Santana de Almeida Federal University of Bahia, Thomas Zimmermann University of California, Irvine, Iftekhar Ahmed University of California at Irvine Pre-print | ||
14:20 10mTalk | Towards Detecting Prompt Knowledge Gaps for Improved LLM-guided Issue Resolution Technical Papers Ramtin Ehsani Drexel University, Sakshi Pathak Drexel University, Preetha Chatterjee Drexel University, USA Pre-print | ||
14:30 10mTalk | Intelligent Semantic Matching (ISM) for Video Tutorial Search using Transformer Models Technical Papers | ||
14:40 10mTalk | Language Models in Software Development Tasks: An Experimental Analysis of Energy and Accuracy Technical Papers Negar Alizadeh Universiteit Utrecht, Boris Belchev University of Twente, Nishant Saurabh Utrecht University, Patricia Kelbert Fraunhofer IESE, Fernando Castor University of Twente | ||
14:50 10mTalk | TriGraph: A Probabilistic Subgraph-Based Model for Visual Code Completion in Pure Data Technical Papers Anisha Islam Department of Computing Science, University of Alberta, Abram Hindle University of Alberta | ||
15:00 5mTalk | Inferring Questions from Programming Screenshots Technical Papers Faiz Ahmed York University, Xuchen Tan York University, Folajinmi Adewole York University, Suprakash Datta York University, Maleknaz Nayebi York University | ||
15:05 5mTalk | Human-In-The-Loop Software Development Agents: Challenges and Future Directions Industry Track Jirat Pasuksmit Atlassian, Wannita Takerngsaksiri Monash University, Patanamon Thongtanunam University of Melbourne, Kla Tantithamthavorn Monash University, Ruixiong Zhang Atlassian, Shiyan Wang Atlassian, Fan Jiang Atlassian, Jing Li Atlassian, Evan Cook Atlassian, Kun Chen Atlassian, Ming Wu Atlassian | ||
15:10 5mTalk | FormalSpecCpp: A Dataset of C++ Formal Specifications Created Using LLMs Data and Tool Showcase Track Madhurima Chakraborty University of California, Riverside, Peter Pirkelbauer Lawrence Livermore National Laboratory, Qing Yi Lawrence Livermore National Laboratory | ||