ACM SIGPLAN
Our OOPSLA 2020 paper “TacTok: Semantics-Aware Proof Synthesis” shows that formal proofs of software properties can be synthesized automatically by learning from previously written proofs by humans. Read more at https://people.cs.umass.edu/~brun/pubs/pubs/First20oopsla.pdf
TacTok: Semantics-Aware Proof Synthesis
Paper DOI: https://doi.org/10.1145/3428299 preprint url: https://people.cs.umass.edu/~brun/pubs/pubs/First20oopsla.pdf more info: https://github.com/LASER-UMASS/TacTok/
Presented at OOPSLA, part of SPLASH 2020
By Emily First, Yuriy Brun, Arjun Guha