Viper
From MaRDI portal
Cited in
(71)- Dafny
- Oclgrind
- Frama-C
- VCC
- Ultimate Automizer
- Chalice
- VeriFast
- Verifying Whiley programs with Boogie
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- Toolchain
- Cyclone
- WhyML
- HIP
- Smallfoot
- Deductive verification of floating-point Java programs in KeY
- VerCors
- GPUVerify
- Automating deductive verification for weak-memory programs
- A verification-driven framework for iterative design of controllers
- GKLEE
- Grasshopper
- Joogie
- BVD
- Mezzo
- Viper: a verification infrastructure for permission-based reasoning
- Contract-based verification of MATLAB-style matrix programs
- Caper
- coreStar
- OpenJML
- Caper
- Infer
- VACID-0
- GRASShopper
- SMACK
- REFINER
- JOANA
- SCCharts
- SCEst
- DarwinSPL
- DeltaEcore
- Rust
- Slide
- GRace
- JSAI
- RVT
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- GraVy
- Rust2Viper
- Crust
- CIVL
- Automated verification of parallel nested DFS
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- RustHorn: CHC-based verification for Rust programs
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- On temporal and separation logics
- WebAssembly
- Loopy
- Nagini
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- SeLoger
- MoSeL
- RustBelt
- RHLE Benchmarks
- RustHorn
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Practical abstractions for automated verification of shared-memory concurrency
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
This page was built for software: Viper
