Skip to content

Commit 517940c

Browse files
Xavier DenisXavier Denis
Xavier Denis
authored and
Xavier Denis
committed
Add all missing meetings
1 parent b49f5c5 commit 517940c

23 files changed

+254
-6
lines changed

‎content/meetings/_index.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
+++
22
title = "RFMIG meetings"
3+
sort_by = "date"
4+
render = false
35
+++
46
meetings section

‎content/meetings/aeneas.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
+++
2+
title = "Aeneas"
3+
date = 2022-10-24
4+
+++
5+
6+
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.
7+
8+
[Video]( https://youtu.be/9j9EE36lJJI )

‎content/meetings/axiom-profiler.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
+++
2+
date = "2024-05-27"
3+
title = "Debugging SMT issues: Axiom Profiler 2.0"
4+
+++
5+
6+
The majority of automated verification tools rely on SMT solvers for logical reasoning. Often tools spend most of the verification time querying them. However, these solvers are rather opaque: what can I as a verification tool developer or even user do when I run into poor performance or timeouts? In this talk I will describe our work on a new SMT analysis tool called “Axiom Profiler 2.0” which can help with debugging such performance problems. Currently the tool can help with the analysis of quantifier instantiations (the most common root cause of performance issues) during a run of z3, though in the future we hope to enable the analysis of other aspects.
7+
A prior tool simply called “Axiom Profiler” (1.0) was created with the same goal, but was cumbersome to use (only running on an older version of Windows), suffered from performance issues and frequent crashes, and supported only a single z3 version. Our new 2.0 tool has been rebuilt from scratch in Rust: it can be compiled to WASM to run anywhere, it is ~10x faster and much more stable, and it supports all modern z3 versions (we are open to supporting other SMT solvers in the future).
8+
The talk will cover the basics of how SMT solvers handle quantifiers, demonstrate how the Axiom Profiler 2.0 helps one to debug and fix related issues, and discuss potential future features. We aim to make this a beneficial tool for all users of SMT solvers and thus I encourage people to raise [suggestions/feature requests/smt-performance-related issues they’ve encountered] during the talk or in the subsequent discussion.

‎content/meetings/contracts.md‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,6 @@
22
title = "Contracts in Rust"
33
date = 2024-09-24
44
+++
5-
**Title**:
6-
7-
**Abstract**:
85

96
As the growing number of verification tools (Aeneas, Creusot, Kani, Prusti, Verus, ...) has shown, there is a growing community for formal verification of Rust code.
107
Each of these tools needs to re-invent a specification language, leading to a rapidly fragmenting ecosystem of incompatible languages and tools.

‎content/meetings/creusat.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
+++
2+
title = "CreuSAT"
3+
date = 2022-09-26
4+
+++
5+
6+
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.
7+
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.
8+
9+
The resulting solver is the first deductively verified solver which is able to consistently solve problems from the SAT competition.
10+
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.
11+
12+
[Video]( https://youtu.be/MkhjDpai8fM )

‎content/meetings/creusot-type-invariants.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
+++
2+
title = "Type Invariants in Creusot"
3+
date = 2023-09-25
4+
+++
5+
6+
Type invariants are a common mechanism in program verification, that allows attaching logical predicates to data types. They typically capture properties of a data type that are preserved by operations on its values. Creusot is a tool for automated deductive verification of (safe) Rust programs. Leveraging the non-aliasing guarantees of Rust's type system, it translates annotated Rust to a functional language. The challenge of supporting type invariants in Creusot is preserving its strong composability without introducing unsoundness in the interaction with Creusot's encoding of mutable borrows. We present a novel translation of invariants for mutable borrows, that overcomes these challenges. Type invariants in Creusot proved useful for the verification of Rust's iterator combinators, reducing the required amount of manual specifications.

‎content/meetings/creusot.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
+++
2+
title = "Creusot"
3+
date = 2022-02-28
4+
+++
5+
6+
Xavier Denis will discuss [Creusot](https://github.com/xldenis/creusot), his deductive verifier for Rust. Creusot aims to provide efficient verification of complex *safe* Rust code, and is backed by the Why3 verification platform. In this talk we'll briefly cover the high-level architecture of Creusot and some of the unique features in the tool.
7+
8+
https://www.eventbrite.com/e/creusot-tickets-260072873967

‎content/meetings/crux-mir.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
+++
2+
title = "CRUX MIR"
3+
date = 2022-05-30
4+
+++
5+
6+
7+
crux-mir is a symbolic testing tool for Rust. The user writes test cases using symbolic variables as inputs; crux-mir uses symbolic execution to check that the tests pass for all possible values of the symbolic variables. crux-mir checks for absence of panics, overflows, and some forms of undefined behavior, and it supports user-defined assertions. Recently, crux-mir gained support for calling Cryptol specifications directly from Rust code and for compositional reasoning, which allows efficiently verifying more complex functions, such as Rust implementations of cryptographic primitives.
8+
In this talk, I'll describe the design of crux-mir and show some examples of its use, with particular focus on the newer Cryptol and compositional reasoning features.
9+
10+
[Video](https://www.youtube.com/watch?v=f3b5V3B4Q8c)

‎content/meetings/ferrocene.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
+++
2+
title = "Ferrocene"
3+
date = 2022-04-25
4+
+++
5+
6+
7+
Ferrocene is an effort to bring Rust into the realm of safety-critical software while also bringing tangible benefits to so called mission-critical efforts. The project has been ongoing for about a year now. This talk will give an overview of current findings and particularly an observation of the current state of the safety-critical ecosystem.
8+
9+
Particularly, it will share observations on the application of formal methods in the realm right now.
10+
11+
---
12+
13+
Florian Gilcher is a co-founder of Ferrous Systems and a Rust teacher since 2015. Previously a member of the Rust Community and Core team and a co-founder of the Rust Foundation, Florian is currently focusing to bringing Rust to safety critical systems, such as cars.
14+
15+
[Video](https://www.youtube.com/watch?v=eaObPhTnoGo)

‎content/meetings/flowistry‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
### June Meeting (June 27th, 2022)
2+
3+
#### Abstract
4+
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in languages with mutation and pointers. Prior work addressed these challenges with bespoke type systems to encode information flow, such as in JFlow (for Java) and FlowCaml (for OCaml). We demonstrate that Rust's existing system of ownership types can repurposed for modular information flow analysis. We describe our analysis using Oxide, a formal model of safe Rust, and prove its soundness as noninterference. We implement the analysis as Flowistry, a tool that analyzes information flow within Rust's MIR CFG. And we show that Flowistry is reasonably precise versus a whole-program analysis via an evaluation on a dataset of large Rust codebases.
5+
6+
#### About the Speaker
7+
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.
8+
9+
[Video](https://youtu.be/adDGcSSZKI4)

0 commit comments

Comments
 (0)