Add OOPSLA'23 publication

publications/lin-chen-trinh-wang-rosu-2023-oopsla.bib

@@ -0,0 +1,25 @@
+@inproceedings{lin-chen-trinh-wang-rosu-2023-oopsla,
+  author    = {Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and Grigore Ro\c{s}u},
+  title     = {Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier},
+  abstract  = {
+A language-agnostic program verifier takes three inputs: a program, its formal specification, and the formal
+semantics of the programming language in which the program is written. It then uses a language-agnostic
+verification algorithm to prove the program correct with respect to its specification, using directly the formal
+language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the
+correctness of each successful verification run by generating a proof certificate for it. The proof certificate
+can be checked by a small proof checker. The preliminary experiments apply the method to generate proof
+certificates for the verification of an imperative language, a functional language, and an assembly language,
+showing that the proposed method is language-agnostic.
+  },
+  author_id         = {Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and Grigore Rosu},
+  category          = {fsl, executable_semantics, logics, matching_logic,
+                       program_verification, programming_languages},
+  project_url       = {https://github.com/kframework/matching-logic-proof-checker},
+  project_name      = {Matching Logic Proof Checker},
+  booktitle_acronym = {OOPSLA'23},
+  booktitle_url     = {https://2023.splashcon.org/track/splash-2023-oopsla},
+  booktitle         = {Proceedings of OOPSLA 2023},
+  year              = {2023},
+  month             = {July},
+  publisher         = {ACM},
+}

publications/lin-chen-trinh-wang-rosu-2023-oopsla.md

@@ -0,0 +1,66 @@
+---
+bib:
+  abstract: 'A language-agnostic program verifier takes three inputs: a program, its
+    formal specification, and the formal semantics of the programming language in
+    which the program is written. It then uses a language-agnostic verification algorithm
+    to prove the program correct with respect to its specification, using directly
+    the formal language semantics. Such a complex verifier can easily have bugs. This
+    paper proposes a method to certify the correctness of each successful verification
+    run by generating a proof certificate for it. The proof certificate can be checked
+    by a small proof checker. The preliminary experiments apply the method to generate
+    proof certificates for the verification of an imperative language, a functional
+    language, and an assembly language, showing that the proposed method is language-agnostic.'
+  author:
+  - first: Zhengyao
+    last: Lin
+  - first: Xiaohong
+    last: Chen
+  - first: Minh-Thai
+    last: Trinh
+  - first: John
+    last: Wang
+  - first: Grigore
+    last: Ro\c{s}u
+  author_id: Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and
+    Grigore Rosu
+  author_ids:
+  - zhengyao-lin
+  - xiaohong-chen
+  - minhthai-trinh
+  - john-wang
+  - grigore-rosu
+  authors:
+  - id: zhengyao-lin
+    text: Zhengyao Lin
+  - id: xiaohong-chen
+    text: Xiaohong Chen
+  - id: minhthai-trinh
+    text: Minh-Thai Trinh
+  - id: john-wang
+    text: John Wang
+  - id: grigore-rosu
+    text: Grigore Rosu
+  booktitle: Proceedings of OOPSLA 2023
+  booktitle_acronym: OOPSLA'23
+  booktitle_url: https://2023.splashcon.org/track/splash-2023-oopsla
+  category:
+  - fsl
+  - executable_semantics
+  - logics
+  - matching_logic
+  - program_verification
+  - programming_languages
+  date: 2023-07-01
+  id: lin-chen-trinh-wang-rosu-2023-oopsla
+  month: July
+  project_name: Matching Logic Proof Checker
+  project_url: https://github.com/kframework/matching-logic-proof-checker
+  publisher: ACM
+  title: Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
+  type: inproceedings
+  year: '2023'
+bib_url: publications/lin-chen-trinh-wang-rosu-2023-oopsla.bib
+layout: paper
+pdf_url: publications/lin-chen-trinh-wang-rosu-2023-oopsla.pdf
+title: Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
+---