Viper
From MaRDI portal
Software:26932
No author found.
Related Items (22)
Formal verification of parallel prefix sum and stream compaction algorithms in CUDA ⋮ Automated Verification of Parallel Nested DFS ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ 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 ⋮ 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 ⋮ Caper ⋮ Principled Software Development ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Viper: A Verification Infrastructure for Permission-Based Reasoning ⋮ On Temporal and Separation Logics ⋮ Automating deductive verification for weak-memory programs ⋮ 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 ⋮ Verifying Whiley programs with Boogie ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
This page was built for software: Viper
