Proofster: Automated Formal Verification
by Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun
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 Proofster, a web-based tool aimed at assisting developers with the formal verification process via proof synthesis. Proofster 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, Proofster outputs the proof-space search tree its synthesis explored, which can guide the developer to provide a hint to enable Proofster to synthesize the proof. Proofster runs online at https://proofster.cs.umass.edu/ and a video demonstrating Proofster is available at https://youtu.be/xQAi66lRfwI/.

Citation:
Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, and Yuriy Brun, Proofster: Automated Formal Verification, in Proceedings of the Demonstrations Track at the 45th International Conference on Software Engineering (ICSE), 2023.
Bibtex:
@inproceedings{Agrawal23icse-demo,
  author = {Arpan Agrawal and Emily First and Zhanna Kaufman and Tom Reichel and 
  Shizhuo Zhang and Timothy Zhou and Alex Sanchez-Stern and Talia Ringer and 
  Yuriy Brun},
  title =
  {\href{http://people.cs.umass.edu/brun/pubs/pubs/Agrawal23icse-demo.pdf}{Proofster: 
  {Automated} Formal Verification}},
  booktitle = {Proceedings of the Demonstrations Track at the 45th International Conference on Software Engineering (ICSE)},
  venue = {ICSE Demo},
  address = {Melbourne, Australia},
  month = {May},
  date = {14--20},
  year = {2023},
  accept = {$\frac{38}{80} \approx 48\%$},
  
  abstract = {<p>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 Proofster, a
  web-based tool aimed at assisting developers with the formal verification
  process via proof synthesis. Proofster 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, Proofster outputs the proof-space search tree its
  synthesis explored, which can guide the developer to provide a hint to
  enable Proofster to synthesize the proof. Proofster runs online at
  https://proofster.cs.umass.edu/ and a video demonstrating Proofster is
  available at https://youtu.be/xQAi66lRfwI/.</p>},
}