Viper: A Verification Infrastructure for Permission-Based Reasoning

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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

• Coq
• Dafny
• KRAKATOA
• Why3
• JML
• Spec#
• Frama-C
• Chalice
• VeriFast
• Boogie
• Smallfoot
• VerCors
• Grasshopper
• Viper
• coreStar

This page was built for publication: Viper: A Verification Infrastructure for Permission-Based Reasoning