Update index.md

index.md

@@ -137,6 +137,14 @@ LICS, 2019.
 
 ### Other publications 
 
+  - **Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu**.
+    *Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier*,
+    OOPSLA, 2023.
+    - A language-agnostic program verifier takes as input both a program with its formal specification and the formal semantics of the programming language in which the program is written, and 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 a virtual machine language, showing that the proposed method is language-agnostic. 
+  - **Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu**.
+    *[Towards a Trustworthy Semantics-Based Language Framework via Proof Generation](https://fsl.cs.illinois.edu/publications/chen-lin-trinh-rosu-2021-cav.html)*,
+    CAV, 2021.
+    - We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based on proof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework both practical and trustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising. 
   - **Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Pena, Grigore Rosu**.
     *[Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic](https://fsl.cs.illinois.edu/publications/chen-pena-rodrigues-rosu-trinh-2020-oopsla.html)*,
     OOPSLA, 2020.