diff --git a/README.md b/README.md index 1377925e0906a03ae7ec6eaf8fc3dd155f65be41..36de663f1e4fa3b8abab2ff7ede46e8b05c18fbf 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`