Explore the words cloud of the RustBelt project. It provides you a very rough idea of what is the project "RustBelt" about.
The following table provides information about the project.
Coordinator |
MAX-PLANCK-GESELLSCHAFT ZUR FORDERUNG DER WISSENSCHAFTEN EV
Organization address contact info |
Coordinator Country | Germany [DE] |
Project website | http://plv.mpi-sws.org/rustbelt/ |
Total cost | 1˙946˙250 € |
EC max contribution | 1˙946˙250 € (100%) |
Programme |
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC)) |
Code Call | ERC-2015-CoG |
Funding Scheme | ERC-COG |
Starting year | 2016 |
Duration (year-month-day) | from 2016-04-01 to 2021-03-31 |
Take a look of project's partnership.
# | ||||
---|---|---|---|---|
1 | MAX-PLANCK-GESELLSCHAFT ZUR FORDERUNG DER WISSENSCHAFTEN EV | DE (MUENCHEN) | coordinator | 1˙946˙250.00 |
'A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.
Rust is a new language developed at Mozilla Research that marries together the low-level flexibility of modern C\ with a strong 'ownership-based' type system guaranteeing type safety, memory safety, and data race freedom. As such, Rust has the potential to revolutionize systems programming, making it possible to build software systems that are safe by construction, without having to give up low-level control over performance.
Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of unsafe blocks, which enable them to opt out of the type system when necessary. The hope is that such unsafe code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art.
In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of unsafe code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems. '
year | authors and title | journal | last update |
---|---|---|---|
2019 |
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models published pages: 1-31, ISSN: 2475-1421, DOI: 10.1145/3290381 |
Proceedings of the ACM on Programming Languages 3/POPL | 2019-06-06 |
2017 |
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer RustBelt: securing the foundations of the rust programming language published pages: 1-34, ISSN: 2475-1421, DOI: 10.1145/3158154 |
Proceedings of the ACM on Programming Languages 2/POPL | 2019-04-18 |
2018 |
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis A separation logic for a promising semantics published pages: , ISSN: , DOI: |
European Symposium on Programming (ESOP) | 2019-04-18 |
2018 |
Azalea Raad, Ori Lahav, Viktor Vafeiadis On Parallel Snapshot Isolation and Release/Acquire Consistency published pages: , ISSN: , DOI: |
European Symposium on Programming (ESOP) | 2019-04-18 |
2018 |
RALF JUNG, ROBBERT KREBBERS, JACQUES-HENRI JOURDAN, ALEÅ BIZJAK, LARS BIRKEDAL, DEREK DREYER Iris from the ground up: A modular foundation for higher-order concurrent separation logic published pages: , ISSN: 0956-7968, DOI: 10.1017/S0956796818000151 |
Journal of Functional Programming 28 | 2019-04-18 |
2017 |
David Swasey, Deepak Garg, Derek Dreyer Robust and compositional verification of object capability patterns published pages: 1-26, ISSN: 2475-1421, DOI: 10.1145/3133913 |
Proceedings of the ACM on Programming Languages 1/OOPSLA | 2019-04-18 |
2017 |
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis Effective stateless model checking for C/C++ concurrency published pages: 1-32, ISSN: 2475-1421, DOI: 10.1145/3158105 |
Proceedings of the ACM on Programming Languages 2/POPL | 2019-04-18 |
2018 |
Azalea Raad, Viktor Vafeiadis Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model published pages: 1-27, ISSN: 2475-1421, DOI: 10.1145/3276507 |
Proceedings of the ACM on Programming Languages 2/OOPSLA | 2019-04-18 |
2018 |
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer MoSeL: a general, extensible modal framework for interactive proofs in separation logic published pages: 1-30, ISSN: 2475-1421, DOI: 10.1145/3236772 |
Proceedings of the ACM on Programming Languages 2/ICFP | 2019-04-18 |
2018 |
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer Mtac2: typed tactics for backward reasoning in Coq published pages: 1-31, ISSN: 2475-1421, DOI: 10.1145/3236773 |
Proceedings of the ACM on Programming Languages 2/ICFP | 2019-04-18 |
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "RUSTBELT" project.
For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.
Send me an email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.
Thanks. And then put a link of this page into your project's website.
The information about "RUSTBELT" are provided by the European Opendata Portal: CORDIS opendata.
High-throughput single-cell phenotypic analysis of functional antibody repertoires
Read MoreWhy is the world green: testing top-down control of plant-herbivore food webs by experiments with birds, bats and ants
Read MoreProviding RObust high TECHnology Tags based on linear carbon nanostructures
Read More