Fetching the paper…
Reading the bibliography…
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems.
Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019 · 1903
Earlier work this paper cites.
Guarded Commands, Nondeterminacy and Formal Derivation of Programs
Edsger W. Dijkstra. 1975 · 1975
Earlier work this paper cites.
Linear Types can Change the World!. In Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990 . North-Holland, 561
Philip Wadler. 1990 · 1990
Earlier work this paper cites.
On the Frame Problem in Procedure Specifications
Alexander Borgida, John Mylopoulos, and Raymond Reiter. 1995 · 1995
Earlier work this paper cites.
Typed Memory Management in a Calculus of Capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99)
Karl Crary, David Walker, and Greg Morrisett. 1999 · 1999
Earlier work this paper cites.
Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP ’00)
Frederick Smith, David Walker, and J. Gregory Morrisett. 2000 · 2000
Earlier work this paper cites.
Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings . IEEE Computer Society, 55–74
John C. Reynolds. 2002 · 2002
Earlier work this paper cites.
Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures (LNCS, Vol. 4111) . Springer, 364–387
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005 · 2005
Earlier work this paper cites.
L3: A Linear Language with Locations. In Typed Lambda Calculi and Applications
Greg Morrisett, Amal Ahmed, and Matthew Fluet. 2005 · 2005
Earlier work this paper cites.
Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Conference on Practical Aspects of Declarative Languages (PADL’05)
Dengping Zhu and Hongwei Xi. 2005 · 2005
Earlier work this paper cites.
Resources, concurrency, and local reasoning
Peter W. O’Hearn. 2007 · 2006
Earlier work this paper cites.
Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4603) , Frank Pfenning (Ed.). Springer, 183–198
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2007 · 2007
Earlier work this paper cites.
Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (LNCS, Vol. 4963) . Springer, 337–340
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008 · 2008
Earlier work this paper cites.
The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) , A. Gupta and D. Kroening (Eds.)
Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010 · 2010
Earlier work this paper cites.
Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (LNCS, Vol. 6355) . Springer, 348–370
K. Rustan M. Leino. 2010 · 2010
Earlier work this paper cites.
A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In Conference: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010
Rustan Leino and Philipp Rümmer. 2010 · 2010
Cited alongside, same era.
Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages . Wrocław, Poland, 53–64
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. 2011 · 2011
Cited alongside, same era.
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6617) , Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer, 41–55
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011 · 2011
Cited alongside, same era.
RustHorn: CHC-Based Verification for Rust Programs. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings (LNCS, Vol. 12075) . Springer, 484–514
Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2020 · 2020
Later among the works it cites.
Steel: proof-oriented programming in a dependently typed concurrent separation logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, and Tahina Ramananandro. 2021 · 2021
Later among the works it cites.
Rust in the Android platform
Google Security Blog. 2021 · 2021
Later among the works it cites.
A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust
David J. Pearce. 2021 · 2021
Later among the works it cites.
GhostCell: Separating Permissions from Data in Rust
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. 2021 · 2021
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Nicholas D. Matsakis and Felix S. Klock. 2014 · 2014
Cited alongside, same era.
The Lean Theorem Prover. In Proceedings of the Conference on Automated Deduction (CADE)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015 · 2015
Cited alongside, same era.
Cogent: Verifying High-Assurance File System Implementations. In Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016 · 2016
Cited alongside, same era.
Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings (LNCS, Vol. 9583) . Springer, 41–62
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016 · 2016
Cited alongside, same era.
Dependent Types and Multi-Monadic Effects in F*. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016 · 2016
Cited alongside, same era.
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a · 2018
Cited alongside, same era.
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018b · 2018
Cited alongside, same era.
The Rust Programming Language
Steve Klabnik and Carol Nichols. 2018 · 2018
Cited alongside, same era.
Leveraging Rust Types for Modular Specification and Verification
Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019 · 2019
Cited alongside, same era.
Later among the works it cites.
The Prusti Project: Formal Verification for Rust. In NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings (LNCS, Vol. 13260) . Springer, 88–108
Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers. 2022 · 2022
Later among the works it cites.
The Coq Proof Assistant
Coq Development Team. 2022 · 2022
Later among the works it cites.
Creusot: A Foundry for the Deductive Verication of Rust Programs. In Proceedings of ICFEM 2022 - International Conference on Formal Engineering Methods (Lecture Notes in Computer Science) . Springer Verlag, Madrid, Spain
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022 · 2022
Later among the works it cites.
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. 2022 · 2022
Later among the works it cites.
Aeneas: Rust Verification by Functional Translation
Son Ho and Jonathan Protzenko. 2022 · 2022
Later among the works it cites.
Linear types for large-scale systems verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2022 · 2022
Later among the works it cites.
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs With Unsafe Code. In PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022 . ACM, 841–856
Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. 2022 · 2022
Later among the works it cites.
Linus Torvalds: Rust will go into Linux 6.1
Steven Vaughan-Nichols. 2022 · 2022
Later among the works it cites.
Verus: Verifying Rust Programs using Linear Ghost Types – Supplementary Material
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023 · 2023
Closest in time.