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 CUDAAutomated Verification of Parallel Nested DFSConcise Read-Only Specifications for Better Synthesis of Programs with PointersLocal Reasoning for Global Graph PropertiesRustHorn: CHC-Based Verification for Rust ProgramsConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative ProgramsDeductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)Product programs in the wild: retrofitting program verifiers to check information flow securityFunctional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithmsIntegrating Owicki-Gries for C11-style memory models into Isabelle/HOLCaperGeneralized arrays for Stainless framesConcise outlines for a complex logic: a proof outline checker for TaDAEfficient modular SMT-based model checking of pointer programsFoundations for entailment checking in quantitative separation logicIris from the ground up: A modular foundation for higher-order concurrent separation logicDeductive verification of floating-point Java programs in KeY\( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languagesEfficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable KeysOn Temporal and Separation LogicsA verification-driven framework for iterative design of controllersVerifying Whiley programs with BoogieA 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