Update README.md

README.md

@@ -8,7 +8,9 @@ The work for Clojure and C has begun but not continued.
 
 Paper: https://www.researchgate.net/publication/337441241_A_Multi-target_Code_Generator_for_High-Level_B
 
-Citation:
+Citations:
+
+- B2Program Paper:
 
 ```
 @InProceedings{b2program,
@@ -23,6 +25,44 @@ doi = {10.1007/978-3-030-34968-4_25}
 }
 ```
 
+- B2Program Validation Documents Paper:
+
+```
+@InProceedings{b2program_js,
+author="Vu, Fabian
+and Happe, Christopher
+and Leuschel, Michael",
+editor="Groote, Jan Friso
+and Huisman, Marieke",
+title="Generating Domain-Specific Interactive Validation Documents",
+booktitle="Formal Methods for Industrial Critical Systems",
+year="2022",
+publisher="Springer International Publishing",
+address="Cham",
+pages="32--49",
+isbn="978-3-031-15008-1"
+}
+```
+
+- B2Program Model Checking Code Generation Paper:
+
+```
+@InProceedings{b2program_mc,
+author="Vu, Fabian
+and Brandt, Dominik
+and Leuschel, Michael",
+editor="Riesco, Adrian
+and Zhang, Min",
+title="Model Checking B Models via High-Level Code Generation",
+booktitle="Formal Methods  and Software Engineering",
+year="2022",
+publisher="Springer International Publishing",
+address="Cham",
+pages="334--351",
+isbn="978-3-031-17244-1"
+}
+```
+
 The main features of B2Program are:
 - Code generation from a formal model
 - Code generation for model checking including parallelization, and caching (only supported in Java, C++ and Rust)