Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.
Wed 17 JulDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Formal VerificationDemonstrations / Journal First / Research Papers / Industry Papers at Pitanga Chair(s): Yunja Choi Kyungpook National University | ||
11:00 18mTalk | A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification Research Papers DOI Media Attached | ||
11:18 9mTalk | CoqPyt: Proof Navigation in Python in the Era of LLMs Demonstrations Pedro Carrott Imperial College London, Nuno Saavedra INESC-ID and IST, University of Lisbon, Kyle Thompson University of California, San Diego, Sorin Lerner University of California at San Diego, João F. Ferreira INESC-ID and IST, University of Lisbon, Emily First University of California, San Diego DOI Pre-print | ||
11:27 9mTalk | How We Built Cedar: A Verification-Guided Approach Industry Papers Craig Disselkoen Amazon Web Services, Aaron Eline Amazon, Shaobo He Amazon Web Services, Kyle Headley Unaffiliated, MIchael Hicks Amazon, Kesha Hietala Amazon Web Services, John Kastner Amazon Web Services, Anwar Mamat University of Maryland, Matt McCutchen , Neha Rungta Amazon Web Services, Bhakti Shah University of St. Andrews, Emina Torlak Amazon Web Services, USA, Andrew Wells Amazon Web Services | ||
11:36 18mTalk | Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties Journal First Claudio Menghi University of Bergamo; McMaster University, Christos Tsigkanos University of Bern, Switzerland, Mehrnoosh Askarpour McMaster University, Patrizio Pelliccione Gran Sasso Science Institute, L'Aquila, Italy, Gricel Vázquez University of York, UK, Radu Calinescu University of York, UK, Sergio García Volvo Cars Corporation, Sweden | ||
11:54 18mTalk | Rigorous Assessment of Model Inference Accuracy using Language Cardinality Journal First Donato Clun Imperial College London, Donghwan Shin University of Sheffield, Antonio Filieri AWS and Imperial College London, Domenico Bianculli University of Luxembourg | ||
12:12 18mTalk | Simulation-based Testing of Simulink Models with Test Sequence and Test Assessment Blocks Journal First Federico Formica McMaster University, Tony Fan McMaster University, Akshay Rajhans Mathworks, Vera Pantelic McMaster University, Mark Lawford McMaster University, Claudio Menghi University of Bergamo; McMaster University | ||