Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Zhengyao Lin, Xiaohong Chen 0002, Minh-Thai Trinh, John Wang, Grigore Rosu. Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):56-84, April 2023. [doi]

@article{LinCTWR23,
  title = {Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier},
  author = {Zhengyao Lin and Xiaohong Chen 0002 and Minh-Thai Trinh and John Wang and Grigore Rosu},
  year = {2023},
  month = {April},
  doi = {10.1145/3586029},
  url = {https://doi.org/10.1145/3586029},
  researchr = {https://researchr.org/publication/LinCTWR23},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA1},
  pages = {56-84},
}