Rust
From MaRDI portal
swMATH28437MaRDI QIDQ40151FDOQ40151
Author name not available (Why is that?)
Official website: https://www.rust-lang.org/
Cited In (98)
- Eulertigs
- SPUMONI
- pufferfish2
- PuffAligner
- IPSA
- RHLE Benchmarks
- A Recursive Inclusion Checker for Recursively Defined Subtypes
- Set constraints, pattern match analysis, and SMT
- Aneris: a mechanised logic for modular reasoning about distributed systems
- Title not available (Why is that?)
- RustHorn: CHC-based verification for Rust programs
- Verifying Whiley programs with Boogie
- IronFleet
- SableJBDD
- Formal verification of a Java component using the RESOLVE framework
- Metamath Zero: designing a theorem prover prover
- MONI
- Title not available (Why is that?)
- BDD
- JDD
- Tackling real-life relaxed concurrency with FSL++
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Concise read-only specifications for better synthesis of programs with pointers
- Refinement through restraint: bringing down the cost of verification
- MoSeL
- Scala
- Chalice
- CLSAT
- Lilac
- Cyclone
- Irdis
- Toolchain
- Banshee
- Viper
- Mtac
- ModuRes
- Joogie
- Vellvm
- Mezzo
- SIROCCO
- go
- COCHIS: stable and coherent implicits
- SIDH
- CacBDD
- Theseus
- Idris
- Pilsner
- Lincx
- QWire
- Stardust
- Verasco
- Forsythe
- CertiKOS
- MoCHi
- Autosubst
- Alms
- CertiCoq
- SMACK
- VF2++
- Panoply
- JayHorn
- AstraVer
- OEuf
- Bedrock
- Template-Coq
- VST-Floyd
- Calysto
- CSIDH
- Chiron
- IOzone
- ORCA
- Cascade
- Crust
- GraVy
- Rust2Viper
- On the Frobenius number of certain numerical semigroups
- Computing race variants in message-passing concurrent programming with selective receives
- Temporary read-only permissions for separation logic
- IMP2_Binary_Heap
- AddressSanitizer
- Silq
- FROST
- On_The_FrobeniusNumber
- CauDEr
- MetaCoq
- TimSort
- retworkx
- Nagini
- Extracting functional programs from Coq, in Coq
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Whiley
- JMLAutoTest
- RustBelt
- RustHorn
- Whiteoak
- Abstraction and subsumption in modular verification of C programs
- SoftBound
- Efficient Verified Implementation of Introsort and Pdqsort
This page was built for software: Rust
