Pages that link to "Item:Q837527"

The following pages link to Verification of sequential and concurrent programs (Q837527):

Displaying 50 items.

• Experiments in program verification using Event-B (Q432154) (← links)
• Verification of object-oriented programs: a transformational approach (Q439944) (← links)
• Starvation-free mutual exclusion with semaphores (Q469360) (← links)
• A proof system for adaptable class hierarchies (Q478383) (← links)
• Incremental reasoning with lazy behavioral subtyping for multiple inheritance (Q549694) (← links)
• Toward automatic verification of quantum programs (Q667515) (← links)
• Algebras for iteration and infinite computations (Q715050) (← links)
• Building program construction and verification tools from algebraic principles (Q736461) (← links)
• Correctness and concurrent complexity of the black-white bakery algorithm (Q736464) (← links)
• Verifying traits: an incremental proof system for fine-grained reuse (Q736803) (← links)
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
• Proof systems for planning under 0-approximation semantics (Q893736) (← links)
• A UTP approach for rTiMo (Q1624596) (← links)
• Tournaments for mutual exclusion: verification and concurrent complexity (Q1682286) (← links)
• Reasoning about actions with loops via Hoare logic (Q1712544) (← links)
• Efficient verification of sequential and concurrent C programs (Q1888200) (← links)
• Symbolic execution formally explained (Q1982639) (← links)
• A proof system for disjoint parallel quantum programs (Q2055965) (← links)
• Monadic second-order incorrectness logic for GP 2 (Q2096431) (← links)
• Incorrectness logic for graph programs (Q2117260) (← links)
• Certified verification of relational properties (Q2165505) (← links)
• Verification of concurrent programs using Petri net unfoldings (Q2234071) (← links)
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs (Q2251128) (← links)
• Fifty years of Hoare's logic (Q2280214) (← links)
• Proof pearl: The KeY to correct and stable sorting (Q2351413) (← links)
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos (Q2377304) (← links)
• Verification of programs with half-duplex communication (Q2573635) (← links)
• Highly dependable concurrent programming using design for verification (Q2643127) (← links)
• Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
• Concurrency verification. Introduction to compositional and noncompositional methods (Q2768503) (← links)
• Verification of fine-grain concurrent programs (Q2870197) (← links)
• A Hoare Logic for SIMT Programs (Q2937782) (← links)
• UTP Semantics for rTiMo (Q2971181) (← links)
• Proving Quicksort Correct in Event-B (Q2994490) (← links)
• Introduction to Model Checking (Q3176359) (← links)
• Being and Change: Reasoning About Invariance (Q3449632) (← links)
• The foundations of program verification. In collab. with Ryan D. Stansifer. 2nd ed. (Q3995530) (← links)
• Proving correctness of imperative programs by linearizing constrained Horn clauses (Q4593003) (← links)
• (Q4782047) (← links)
• Automated Verification of Concurrent Search Structures (Q5000450) (← links)
• (Q5015383) (← links)
• (Q5020652) (← links)
• (Q5021219) (← links)
• Unifying Operational Weak Memory Verification: An Axiomatic Approach (Q5056374) (← links)
• Using Hoare Logic in a Process Algebra Setting (Q5164860) (← links)
• A simple, verified validator for software pipelining (Q5255064) (← links)
• A Hoare Logic for GPU Kernels (Q5278201) (← links)
• Indexed and fibered structures for partial and total correctness assertions (Q5889306) (← links)
• Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)
• A dynamic logic with branching modalities (Q6151608) (← links)