Viper
From MaRDI portal
Software:26932
swMATH15038MaRDI QIDQ26932FDOQ26932
Author name not available (Why is that?)
Cited In (22)
- 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
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
- Contract-based verification of MATLAB-style matrix programs
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
- Deductive verification of floating-point Java programs in KeY
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Automating deductive verification for weak-memory programs
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- RustHorn: CHC-Based Verification for Rust Programs
- Principled Software Development
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Practical abstractions for automated verification of shared-memory concurrency
- A verification-driven framework for iterative design of controllers
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
- Local Reasoning for Global Graph Properties
- Automated Verification of Parallel Nested DFS
- Caper
- On Temporal and Separation Logics
This page was built for software: Viper
