PRoofster: Automated Formal Verification

Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Formal verification is an effective but extremely work-intensive method of improving software quality. Verifying the correctness of software systems often requires significantly more effort than implementing them in the first place, despite the existence of proof assistants, such as Coq, aiding the process. Recent work has aimed to fully automate the synthesis of formal verification proofs, but little tool support exists for practitioners. This paper presents oofster, a web-based tool aimed at assisting developers with the formal verification process via proof synthesis. oofster inputs a Coq theorem specifying a property of a software system and attempts to automatically synthesize a formal proof of the correctness of that property. When it is unable to produce a proof, oofster outputs the proof-space search tree its synthesis explored, which can guide the developer to provide a hint to enable oofster to synthesize the proof. oofster runs online at https://proofster.cs.umass.edu/ and a video demonstrating oofster is available at https://youtu.be/xQAi66IRfwI/.

Original languageEnglish (US)
Title of host publicationProceedings - 2023 IEEE/ACM 45th International Conference on Software Engineering
Subtitle of host publicationCompanion, ICSE-Companion 2023
PublisherIEEE Computer Society
Pages26-30
Number of pages5
ISBN (Electronic)9798350322637
DOIs
StatePublished - 2023
Event45th IEEE/ACM International Conference on Software Engineering: Companion, ICSE-Companion 2023 - Melbourne, Australia
Duration: May 14 2023May 20 2023

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Conference

Conference45th IEEE/ACM International Conference on Software Engineering: Companion, ICSE-Companion 2023
Country/TerritoryAustralia
CityMelbourne
Period5/14/235/20/23

Keywords

  • Automated proof synthesis
  • Coq
  • Formal verification
  • Proofster
  • Tool

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'PRoofster: Automated Formal Verification'. Together they form a unique fingerprint.

Cite this