Viper

swMATH15038MaRDI QIDQ26932FDOQ26932

Author name not available (Why is that?)

Cited In (22)

• RustHorn: CHC-based verification for Rust programs
• 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
• Contract-based verification of MATLAB-style matrix programs
• Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Deductive verification of floating-point Java programs in KeY
• Viper: a verification infrastructure for permission-based reasoning
• Concise read-only specifications for better synthesis of programs with pointers
• Local reasoning for global graph properties
• Automated verification of parallel nested DFS
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• On temporal and separation logics
• Automating deductive verification for weak-memory programs
• ConSORT: context- and flow-sensitive ownership refinement types for imperative 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
• Caper

This page was built for software: Viper