Pages that link to "Item:Q2796035"

The following pages link to Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035):

Displaying 14 items.

• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
• Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
• Verifying Whiley programs with Boogie (Q2102933) (← links)
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (Q2120963) (← links)
• Generalized arrays for Stainless frames (Q2152661) (← links)
• Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
• \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages (Q2237340) (← links)
• A verification-driven framework for iterative design of controllers (Q2335947) (← links)
• Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys (Q2798781) (← links)
• Caper (Q2988651) (← links)
• On Temporal and Separation Logics (Q5079764) (← links)
• Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)