<div class="csl-bib-body">
<div class="csl-entry">Hance, T. (2026). Verifying Rust code with Verus. In B. Dutertre & B. Könighofer (Eds.), <i>Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026</i> (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_1</div>
</div>
I will introduce Verus, an open-source, Rust-based verification tool aimed at concurrent software and systems software, which I develop together with a number of collaborators in academia and industry. Verus has spawned a number of publications on a range of verified systems, is already seeing industrial use at Microsoft and Amazon, and has been the subject of a number of experiments on generating proofs with AI. In this tutorial, I will give an overview of Verus and what it can do, and why we invented it compared to the previous state-of-the-art approaches to program verification. I will give a tutorial on how to get started with Verus, and I will illustrate how we approach the various challenges of verification through a number of examples.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.title
Verifying Rust code with Verus
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2026/isbn.978-3-85448-093-8_1
-
dc.contributor.affiliation
Max Planck Institute for Software Systems, Germany
-
dc.contributor.editoraffiliation
Amazon Web Services
-
dc.contributor.editoraffiliation
Graz University of Technology (Graz, AT)
-
dc.relation.isbn
978-3-85448-093-8
-
dc.description.volume
7
-
dc.description.startpage
1
-
dc.description.endpage
1
-
dc.rights.holder
the author
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026
-
tuw.peerreviewed
true
-
tuw.relation.ispartof
10.34727/2026/isbn.978-3-85448-093-8
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.book.chapter
1
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E000 - Technische Universität Wien
-
dc.identifier.libraryid
AC17999067
-
dc.description.numberOfPages
1
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.contributor.serieseditor
Hunt, Warren A., Jr.
-
dc.contributor.serieseditor
Weissenbacher, Georg
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-6284-380X
-
tuw.editor.orcid
0000-0001-5183-5452
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.grantfulltext
open
-
crisitem.author.dept
Max Planck Institute for Software Systems, Germany
