@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 =
  {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},
  pages = {26--30},
  year = {2023},
  accept = {$\frac{38}{80} \approx 48\%$},

  note = {DOI: 10.1109/ICSE-Companion58688.2023.00018}, 
  doi = {10.1109/ICSE-Companion58688.2023.00018},
  
  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/.},

  fundedBy = {DARPA HR0011-22-9-0063, NSF CCF-2210243},
}