I thought it might be nice to have a discussion thread to collect interesting papers on machine learning and automation, and to bring them to the attention of others.

Here is a recent one! https://people.cs.umass.edu/~brun/pubs/pubs/Agrawal23icse-demo.pdf

PRoofster: Automated Formal Verification

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/.

PRoofster [is a] new graphical frontend for search-based proof-synthesis techniques that emphasizes

explainability. Conceptually, PRoofster can be straightforwardly extended to work with any proof-synthesis backend tool, and implements special features to support explainability for search-based backends. Here, we demonstrate PRoofster with Proverbot9001 [45] as its backend. PRoofster’s main contributions support the developer in two ways:

1) The developer can enter a theorem describing a software property they want proven, and PRoofster uses its underlying backend to attempt to generate a proof. If successful, PRoofster displays the Coq proof script, verifying that theproperty is correct. PRoofster uses the Alectryon library to render literate Coq code [39 ], which is interactive and easy to read, even when one does not have immediate access to a proof assistant to step through the synthesized proof. The developer can explore the context throughout the proof to better understand why the property is verifiably correct.

2) If the synthesis is unsuccessful, PRoofster uses the D3.js library [6] to allow the developer to interactively explore the search tree it used in trying to synthesize a proof, and understand the relevant context. The developer can then identify the most promising search-path, augment it, and have PRoofster attempt to synthesize a proof again, using that information. A live PRoofster deployment is available at https://proofster.

cs.umass.edu/.

Last updated: Jul 13 2024 at 04:02 UTC