Viper: A Verification Infrastructure for Permission-Based Reasoning
From MaRDI portal
Publication:2796035
DOI10.1007/978-3-662-49122-5_2zbMath1475.68191OpenAlexW2294722445MaRDI QIDQ2796035
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Publication date: 23 March 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/20.500.11850/85086
Related Items (23)
Formal verification of parallel prefix sum and stream compaction algorithms in CUDA ⋮ 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 ⋮ 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 ⋮ Generalized arrays for Stainless frames ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Deductive verification of floating-point Java programs in KeY ⋮ \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages ⋮ Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys ⋮ On Temporal and Separation Logics ⋮ 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
Uses Software
This page was built for publication: Viper: A Verification Infrastructure for Permission-Based Reasoning