Pages that link to "Item:Q1219675"
From MaRDI portal
The following pages link to An axiomatic proof technique for parallel programs (Q1219675):
Displaying 50 items.
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts (Q1654563) (← links)
- Tournaments for mutual exclusion: verification and concurrent complexity (Q1682286) (← links)
- Conditions of contracts for separating responsibilities in heterogeneous systems (Q1742989) (← links)
- Hybrid process algebra (Q1763160) (← links)
- An assertion-based proof system for multithreaded Java (Q1770359) (← links)
- Invariants, composition, and substitution (Q1894676) (← links)
- Bounded delay for a free address (Q1901690) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- A unified approach of program verification (Q2013885) (← links)
- A proof system for disjoint parallel quantum programs (Q2055965) (← links)
- Compositional verification of smart contracts through communication abstraction (Q2145351) (← links)
- A mechanized refinement proof of the Chase-Lev deque using a proof system (Q2218426) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- Verifying a concurrent garbage collector with a rely-guarantee methodology (Q2319995) (← links)
- Proof-based verification approaches for dynamic properties: application to the information system domain (Q2355384) (← links)
- Automatic workflow verification and generation (Q2368986) (← links)
- Bounded model checking of infinite state systems (Q2369883) (← links)
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos (Q2377304) (← links)
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency (Q2414249) (← links)
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example (Q2418046) (← links)
- Compositional verification of a communication protocol for a remotely operated aircraft (Q2442952) (← links)
- A proof outline logic for object-oriented programming (Q2571207) (← links)
- Towards a Thread-Local Proof Technique for Starvation Freedom (Q2814127) (← links)
- Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency (Q2829245) (← links)
- Regression Verification for Multi-threaded Programs (Q2891406) (← links)
- A Program Construction and Verification Tool for Separation Logic (Q2941173) (← links)
- Proving Linearizability Using Partial Orders (Q2988662) (← links)
- Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs (Q3000591) (← links)
- Compositionality Entails Sequentializability (Q3000634) (← links)
- Axiomatic semantics of projection temporal logic programs (Q3060195) (← links)
- The use of hoare logic in the verification of horizontal microprograms (Q3216113) (← links)
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs (Q3303910) (← links)
- Owicki-Gries Reasoning for Weak Memory Models (Q3449485) (← links)
- Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS (Q3510806) (← links)
- Incremental Reasoning for Multiple Inheritance (Q3605467) (← links)
- Local optimization of colorings of graphs (Q3780451) (← links)
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗ (Q4485121) (← links)
- Reasoning about programs by exploiting the environment (Q4632437) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Q5043584) (← links)
- Unifying Operational Weak Memory Verification: An Axiomatic Approach (Q5056374) (← links)
- Logical foundations for compositional verification and development of concurrent programs in UNITY (Q5096396) (← links)
- A proof system for asynchronously communicating deterministic processes (Q5096883) (← links)
- Wait-free linearization with an assertional proof (Q5136979) (← links)
- Wait-free linearization with a mechanical proof (Q5137000) (← links)
- Fast timing-based algorithms (Q5137323) (← links)
- Automatic verification for a class of distributed systems (Q5137900) (← links)
- Wait-free concurrent memory management by Create and Read until Deletion (CaRuD) (Q5138347) (← links)
- Using Hoare Logic in a Process Algebra Setting (Q5164860) (← links)
- Verification of Concurrent Systems with VerCors (Q5175776) (← links)
