You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: src/previous-events.md
+22-1Lines changed: 22 additions & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,5 +1,26 @@
1
1
## Previous Meetings
2
2
3
+
<!-- ### November Meeting () -->
4
+
5
+
### October Meeting (October 24th, 2022)
6
+
7
+
#### Abstract
8
+
9
+
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on *functional* properties of their code.
10
+
11
+
[Video](https://youtu.be/9j9EE36lJJI)
12
+
13
+
### September Meeting (September 26th, 2022)
14
+
15
+
#### Abstract
16
+
This talk describes CreuSAT, a formally verified SAT solver written in Rust. In addition to implementing the core conflict-driven clause learning (CDCL) algorithm, CreuSAT also implements a series of crucial optimizations.
17
+
The most important of these is the two watched literals scheme with blocking literals and circular search, the variable move-to-front (VMTF) decision heuristic, clause deletion, phase saving, and moving average based restarts.
18
+
19
+
The resulting solver is the first deductively verified solver which is able to consistently solve problems from the SAT competition.
20
+
This is done while maintaining a relatively small code base, amounting to around 4 thousand lines of proof code and program code combined, with a low proof overhead of around three lines of proof code per line of program code.
21
+
22
+
[Video](https://youtu.be/MkhjDpai8fM)
23
+
3
24
### June Meeting (June 27th, 2022)
4
25
5
26
#### Abstract
@@ -8,7 +29,7 @@ Statically analyzing information flow, or how data influences other data within
8
29
#### About the Speaker
9
30
Will Crichton is a 6th year CS Ph.D. student at Stanford University advised by Profs. Pat Hanrahan and Maneesh Agrawala. His research combines programming language theory and cognitive psychology to build better tools for programmers. Will just defended his thesis, "Revisiting Program Slicing with Ownership-based Information Flow", and will soon be starting a postdoc with Shriram Krishnamurthi at Brown to study the learnability of Rust.
Copy file name to clipboardExpand all lines: src/welcome.md
+2-8Lines changed: 2 additions & 8 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -24,11 +24,5 @@ These initiatives may interest the developers of formal methods tools for Rust,
24
24
25
25
# Upcoming Meetings
26
26
27
-
## July
28
-
29
-
Due to a cancellation we no longer have a scheduled speaker for July! If you're interested please let us know.
30
-
31
-
32
-
We hold our meetings on the last monday of every month. Currently, we base ourselve off of European time, with meetings at 7PM. If this causes an issue for you, please leave a message on zulip.
0 commit comments