Merge pull request #15 from cmu-soda/andy_updates

Adding REU page

Author: sheyining

_config.yml

@@ -68,6 +68,11 @@ collections:
     output: true
     layout: product
     show_sidebar: false
+  reu:
+    output: true
+    layout: product
+    show_sidebar: false
+    permalink: /reu/:name/
 navbar_fixed: true
 footer_fixed: true
 

_data/navigation.yml

@@ -8,3 +8,5 @@
   link: /news/
 - name: Tools
   link: /tools/
+- name: REU
+  link: /reu/

_reu/FOL_separators.md

@@ -0,0 +1,28 @@
+---
+title: First-Order Quantified Separator in Alloy Analyzer
+subtitle: 
+layout: product
+image: /assets/img/separator.png
+year: 2025
+student: One An
+mentor: Andy Hammer
+features:
+    - label: First-Order Logic
+      icon: fa-ellipsis-v
+    - label: Alloy
+      icon: fa-cloud
+    - label: Example Driven Synthesis
+      icon: fa-filter
+---
+
+__Description and Significance__
+First-order logic is used to express system invarients, but it's formal complexity hinders wide-scale adoption.
+During debugging of formal expression, *counter-examples* are often used to identify cases that have unexpected behavior for a given invariant.
+These examples can be used to identify what is called a *separator* -- an expression that separates positive and negative examples.
+
+__Student Involvement__
+Students will use Alloy -- a modeling tool based on first-order and relational logics and transitive closure -- to create a separator when given examples.
+The goal of the project is to identify if using formal methods is a viable method for synthesis of a separator.
+
+__Project Results__
+One An successfully submitted a Student Research Competition paper to the Automated Software Engineering Conference of 2025 on Folloy - the tool created to synthesize separators in Alloy.

_reu/TLA_threading.md

@@ -0,0 +1,19 @@
+---
+title: TLA+ Threading for Recomp-Verify
+subtitle: 
+layout: product
+image: /assets/img/recomposition.jpg
+year: 2024
+student: Eduardo Naranjo
+mentor: Ian Dardik
+features:
+    - label: Compositional Verification
+      icon: fa-home
+    - label: TLA+
+      icon: fa-bug
+    - label: Distributed Protocols
+      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

@@ -0,0 +1,27 @@
+---
+title: Compositional Verification of Distributed Protocols in TLA+
+subtitle: 
+layout: product
+image: /assets/img/john_reu_project.png
+year: 2025
+mentor: Ian Dardik
+student: John Ngyuyen
+features:
+    - label: Compositional Verification
+      icon: fa-object-group
+    - label: TLA+
+      icon: fa-plus-square
+    - label: Distributed Protocols
+      icon: fa-cogs
+---
+
+__Description and Significance__
+Distributed protocols, e.g. Paxos and Raft, are at the heart of communication for distributed systems. It is very important for these protocols to be correct, yet verifying (proving) their correctness is extremely challenging. In this project, we aim to improve the scalability and performance of tools that are used to verify the correctness of distributed protocols written in the TLA+ formal specification language. In particular, we will be applying compositional techniques to improve the state of the art for model checking (automatically verifying) distributed protocols.
+
+__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)
+

_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.

assets/img/john_reu_project.png

@@ -16,4 +16,4 @@ Parv's STL/RL project (ICCPS and NFM work)
 Saloni's Kafka project (ABZ paper)
 Leo's Alloy visualization project 
 Ian's TLA+ project
-Andy's MPC project -->
+Andy's MPC project -->