Viper
From MaRDI portal
swMATH15038MaRDI QIDQ26932FDOQ26932
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-662-49122-5_2
Cited In (70)
- RustHorn: CHC-based verification for Rust programs
- RHLE Benchmarks
- Verifying Whiley programs with Boogie
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Contract-based verification of MATLAB-style matrix programs
- 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
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- Deductive verification of floating-point Java programs in KeY
- Viper: a verification infrastructure for permission-based reasoning
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- Automated verification of parallel nested DFS
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- On temporal and separation logics
- Automating deductive verification for weak-memory programs
- MoSeL
- SeLoger
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Frama-C
- VCC
- Ultimate Automizer
- Chalice
- VeriFast
- Cyclone
- HIP
- Smallfoot
- Toolchain
- WhyML
- GPUVerify
- VerCors
- GKLEE
- Grasshopper
- Joogie
- BVD
- Mezzo
- coreStar
- OpenJML
- Caper
- Infer
- VACID-0
- GRASShopper
- SMACK
- REFINER
- DarwinSPL
- DeltaEcore
- JOANA
- SCCharts
- SCEst
- Rust
- Slide
- GRace
- JSAI
- RVT
- CIVL
- Crust
- GraVy
- Rust2Viper
- Loopy
- Nagini
- WebAssembly
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Practical abstractions for automated verification of shared-memory concurrency
- Oclgrind
- RustBelt
- RustHorn
- A verification-driven framework for iterative design of controllers
- Caper
This page was built for software: Viper
