The following pages link to Viper (Q26932):
Displaying 22 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Leveraging compiler intermediate representation for multi- and cross-language verification (Q784116) (← links)
- Practical abstractions for automated verification of shared-memory concurrency (Q784156) (← links)
- 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)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Automating deductive verification for weak-memory programs (Q2324213) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Caper (Q2988651) (← links)
- Principled Software Development (Q4558903) (← links)
- Automated Verification of Parallel Nested DFS (Q5039512) (← links)
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers (Q5041091) (← links)
- Local Reasoning for Global Graph Properties (Q5041096) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (Q5041118) (← links)
- On Temporal and Separation Logics (Q5079764) (← links)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (Q5875940) (← links)
