Polishing REU project pages

Author: arhammer

_reu/TLA_threading.md

@@ -15,3 +15,5 @@ features:
       icon: fa-history
 ---
 
+This project aims to improve _recomposition_ for efficiently verifying distributed systems.
+The project involves improving techniques for decomposing systems and improving algorithms for threading to accelerate the speed of model checking.

_reu/comp_verif_tla.md

@@ -2,7 +2,7 @@
 title: Compositional Verification of Distributed Protocols in TLA+
 subtitle: 
 layout: product
-image: /assets/img/recomposition.jpg
+image: /assets/img/john_reu_project.png
 year: 2025
 mentor: Ian Dardik
 student: John Ngyuyen
@@ -22,7 +22,6 @@ __Student Involvement__
 Students will learn about the theory of model checking, including TLA+ and compositional verification. The goal of the project is for the student to implement compositional verification techniques in an existing model checker for the TLA+ language. Students will work with one of two model checkers that our team has been developing: Recomp-Verify and Carini (see the references). Both model checkers are implemented in Java, so students will be expected to write Java code.
 
 __References__
-[https://github.com/cmu-soda/recomp-verify/tree/FMCAD24](https://github.com/cmu-soda/recomp-verify/tree/FMCAD24)
-
-[https://github.com/cmu-soda/carini](https://github.com/cmu-soda/carini)
+- [https://github.com/cmu-soda/recomp-verify/tree/FMCAD24](https://github.com/cmu-soda/recomp-verify/tree/FMCAD24)
+- [https://github.com/cmu-soda/carini](https://github.com/cmu-soda/carini)
 

_reu/fault_centered_robustness.md

@@ -0,0 +1,20 @@
+---
+title: Fault Centered Robustness in TLA+
+subtitle: 
+layout: product
+image: /assets/img/will_reu_project.png
+year: 2024
+mentor: Ian Dardik
+student: William Morris
+features:
+    - label: Robustness
+      icon: fa-puzzle-piece
+    - label: TLA+
+      icon: fa-plus-square
+    - label: Distributed Protocols
+      icon: fa-cogs
+---
+
+The guarantees provided by formal verification are only as good as the _assumptions_ that are made about the environment.
+Therefore, in prior work, we have proposed _robustness analysis_ to help system designers how robust their guarantees are to environmental _deviations_.
+In this project, we lift the notion of robustness to symbolic transition systems in _fault-centered robustness_, in which we calculate safe environmental envelopes based on a user-given set of symbolic faults.