ConcurrentHOL
From MaRDI portal
- A completeness theorem for Kleene algebras and the algebra of regular events
- A denotational semantics for SPARC TSO
- A generalization of Owicki-Gries's Hoare logic for a concurrent while language
- A lattice-theoretic characterization of safety and liveness
- A logical view of composition
- A New Solution to Lamport's Concurrent Programming Problem Using Small Shared Variables
- A refinement calculus for shared-variable parallel and distributed programming
- Abstract Interpretation Frameworks
- Alternative semantics for temporal logics
- An abstract account of composition
- An axiomatic proof technique for parallel programs
- Assumption/guarantee specifications in linear-time temporal logic
- Brookes is relaxed, almost!
- Colimits for concurrent collectors
- Composition: a way to make proofs harder
- Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
- Computer Science Logic
- Concurrency verification. Introduction to compositional and noncompositional methods
- Concurrent Kleene algebra and its foundations
- Constructing the views framework
- Continuous Lattices and Domains
- Correctness of parallel programs: The Church-Rosser approach
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Data Refinement
- Defining liveness
- Encoding, decoding and data refinement
- Explicit stabilisation for modular rely-guarantee reasoning
- Fine-grained concurrency with separation logic
- Formal derivation of concurrent garbage collectors
- Full abstraction for a shared-variable parallel language
- Fundamental concepts of the methodology of the deductive sciences. I.
- Generalised rely-guarantee concurrency: an algebraic foundation
- Heyting algebras. Duality theory. Translated from the Russian by A. Evseev
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Laws of programming
- Lazy compositional verication
- Local rely-guarantee reasoning
- Logic and structure
- Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
- Modular verification for shared-variable concurrent programs
- Myths about the mutual exclusion problem
- On powerdomains and modality
- On rely-guarantee reasoning
- On the completeness of compositional reasoning methods
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
- Parallel program schemata
- Peterson's mutual exclusion algorithm revisited
- Prespecification in data refinement
- Program derivation by fixed point computation
- Proof theory and algebra in logic
- Proofs of Networks of Processes
- Proving Liveness Properties of Concurrent Programs
- Safety without stuttering
- Safety, liveness and fairness in temporal logic
- Temporal logic and state systems
- Tentative steps toward a development method for interfering programs
- The existence of refinement mappings
- The Rely-Guarantee method for verifying shared variable concurrent programs
- The weakest prespecification
- Theories of Programming Languages
- Time for verification. Essays in memory of Amir Pnueli
- TLA + Proofs
- Topological representations of distributive lattices and Brouwerian logics.
- Transformations of discrete closure systems
- Understanding concurrent systems
- Verification of sequential and concurrent programs
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Views, compositional reasoning for concurrent programs
- ZB 2005: Formal Specification and Development in Z and B
This page was built for software: ConcurrentHOL
