Skip to content

Commit 0f91bf2

Browse files
arhammerarhammer
committed
Creating REU page
1 parent a5cf246 commit 0f91bf2

File tree

8 files changed

+172
-1
lines changed

8 files changed

+172
-1
lines changed

‎_config.yml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,11 @@ collections:
6868
output: true
6969
layout: product
7070
show_sidebar: false
71+
reu:
72+
output: true
73+
layout: product
74+
show_sidebar: false
75+
permalink: /reu/:name/
7176
navbar_fixed: true
7277
footer_fixed: true
7378

‎_data/navigation.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,5 @@
88
link: /news/
99
- name: Tools
1010
link: /tools/
11+
- name: REU
12+
link: /reu/

‎_reu/FOL_separators.md‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
---
2+
title: First-Order Quantified Separator in Alloy Analyzer
3+
subtitle:
4+
layout: product
5+
image: /assets/img/separator.png
6+
year: 2025
7+
student: One An
8+
mentor: Andy Hammer
9+
features:
10+
- label: First-Order Logic
11+
icon: fa-ellipsis-v
12+
- label: Alloy
13+
icon: fa-cloud
14+
- label: Example Driven Synthesis
15+
icon: fa-filter
16+
---
17+
18+
__Description and Significance__
19+
First-order logic is used to express system invarients, but it's formal complexity hinders wide-scale adoption.
20+
During debugging of formal expression, *counter-examples* are often used to identify cases that have unexpected behavior for a given invariant.
21+
These examples can be used to identify what is called a *separator* -- an expression that separates positive and negative examples.
22+
23+
__Student Involvement__
24+
Students will use Alloy -- a modeling tool based on first-order and relational logics and transitive closure -- to create a separator when given examples.
25+
The goal of the project is to identify if using formal methods is a viable method for synthesis of a separator.
26+
27+
__Project Results__
28+
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‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
---
2+
title: TLA+ Threading for Recomp-Verify
3+
subtitle:
4+
layout: product
5+
image: /assets/img/recomposition.jpg
6+
year: 2024
7+
student: Eduardo Naranjo
8+
mentor: Ian Dardik
9+
features:
10+
- label: Compositional Verification
11+
icon: fa-home
12+
- label: TLA+
13+
icon: fa-bug
14+
- label: Distributed Protocols
15+
icon: fa-history
16+
---
17+

‎_reu/comp_verif_tla.md‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
---
2+
title: Compositional Verification of Distributed Protocols in TLA+
3+
subtitle:
4+
layout: product
5+
image: /assets/img/recomposition.jpg
6+
year: 2025
7+
mentor: Ian Dardik
8+
student: John Ngyuyen
9+
features:
10+
- label: Compositional Verification
11+
icon: fa-object-group
12+
- label: TLA+
13+
icon: fa-plus-square
14+
- label: Distributed Protocols
15+
icon: fa-cogs
16+
---
17+
18+
__Description and Significance__
19+
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.
20+
21+
__Student Involvement__
22+
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.
23+
24+
__References__
25+
[https://github.com/cmu-soda/recomp-verify/tree/FMCAD24](https://github.com/cmu-soda/recomp-verify/tree/FMCAD24)
26+
27+
[https://github.com/cmu-soda/carini](https://github.com/cmu-soda/carini)
28+

‎assets/img/separator.png‎

29.2 KB
Loading

‎projects.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,4 @@ Parv's STL/RL project (ICCPS and NFM work)
1616
Saloni's Kafka project (ABZ paper)
1717
Leo's Alloy visualization project
1818
Ian's TLA+ project
19-
Andy's MPC project -->
19+
Andy's MPC project -->

‎reu.md‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
---
2+
layout: page
3+
title: REU Projects
4+
show_sidebar: false
5+
hide_footer: false
6+
permalink: /reu/
7+
---
8+
9+
<div class="team">
10+
11+
<h2>Research Experiences for Undergraduates</h2>
12+
<p>
13+
The REU program at CMU allows for undergraduate students to gain experience in research methods and practices.
14+
Students work on projects throughout the summer with a graduate student advisor.
15+
Any undergraduate who is interested in working with SoDA may apply through the
16+
<a href="https://www.cmu.edu/scs/s3d/reuse/">REUSE application</a>.
17+
</p>
18+
19+
<h2>Projects</h2>
20+
21+
{% assign current_year = 2026 %}
22+
{% assign years = site.reu | map: "year" | uniq | sort | reverse %}
23+
24+
{% for y in years %}
25+
{% if y == current_year %}
26+
<h3>Current Projects</h3>
27+
{% else %}
28+
<h3>Summer {{ y }}</h3>
29+
{% endif %}
30+
31+
<div class="team-members">
32+
{% assign projects = site.reu | where: "year", y %}
33+
{% for project in projects %}
34+
<a href="{{ project.url | relative_url }}" class="team-member-link">
35+
<div class="team-member">
36+
<img src="{{ project.image | relative_url }}" alt="{{ project.title }}" style="width:100%;">
37+
<div class="container">
38+
<h4><b>{{ project.title }}</b></h4>
39+
<p><strong>Mentor:</strong> {{ project.mentor }}</p>
40+
{% if project.student %}
41+
<p><strong>Student:</strong> {{ project.student }}</p>
42+
{% endif %}
43+
<p>{{ project.description | truncatewords: 25 }}</p>
44+
{% if project.project_link %}
45+
<a href="{{ project.project_link }}" target="_blank" class="project-link-button">View Project</a>
46+
{% endif %}
47+
</div>
48+
</div>
49+
</a>
50+
{% endfor %}
51+
</div>
52+
{% endfor %}
53+
54+
</div>
55+
56+
<style>
57+
.team-members {
58+
display: flex;
59+
flex-wrap: wrap;
60+
justify-content: flex-start;
61+
}
62+
.team-member-link {
63+
text-decoration: none;
64+
color: inherit;
65+
}
66+
.team-member {
67+
margin: 10px;
68+
box-shadow: 0 4px 8px 0 rgba(0,0,0,0.2);
69+
transition: 0.3s;
70+
width: 280px;
71+
}
72+
.team-member:hover {
73+
box-shadow: 0 8px 16px 0 rgba(0,0,0,0.2);
74+
}
75+
.container {
76+
padding: 2px 16px;
77+
}
78+
.project-link-button {
79+
display: inline-block;
80+
margin-top: 8px;
81+
padding: 6px 12px;
82+
background-color: #3273dc;
83+
color: white;
84+
border-radius: 4px;
85+
text-decoration: none;
86+
font-size: 0.9em;
87+
}
88+
.project-link-button:hover {
89+
background-color: #275aa8;
90+
}
91+
</style>

0 commit comments

Comments
 (0)