From 7d19deb27d4c3fa2cb64e23db5b32c4af175086c Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Wed, 12 Oct 2022 15:27:30 +0200
Subject: [PATCH] Update README.md

---
 README.md | 44 ++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 1377925e0..36de663f1 100644
--- a/README.md
+++ b/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)
@@ -895,4 +935,4 @@ make install
 * Move the built JAR-file `B2Program-all-0.1.0-SNAPSHOT` to the same folder as `Cruise_finite1_deterministic.mch` and `Cruise_finite1_deterministic.mch`
 * Generate code for `Cruise_finite1_deterministic.mch` `java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l rs -f Cruise_finite1_deterministic.mch -mc true`
 * Rename `Cruise_finite1_deterministic_exec.rs` to `main.rs` and move it and `Cruise_finite1_deterministic.rs` to [btypes_primitives/src/main/rust/bmachine/src](btypes_primitives/src/main/rust/bmachine/src)
-* from the bmachine-directory, run `cargo run --release -- mixed 6 true`
\ No newline at end of file
+* from the bmachine-directory, run `cargo run --release -- mixed 6 true`
-- 
GitLab