Verification of sequential and concurrent programs
From MaRDI portal
(Redirected from Publication:837527)
Recommendations
- scientific article; zbMATH DE number 50008
- scientific article; zbMATH DE number 1032897
- Verifying concurrent programs against sequential specifications
- Programmverifikation
- Efficient verification of sequential and concurrent C programs
- Verification of fine-grain concurrent programs
- Verification of concurrent programs: The automata-theoretic framework
- Specification and verification of concurrent programs through refinements
- Verification of procedural programs
Cited in
(66)- A UTP approach for rTiMo
- Tournaments for mutual exclusion: verification and concurrent complexity
- Reasoning about actions with loops via Hoare logic
- Efficient verification of sequential and concurrent C programs
- Symbolic execution formally explained
- A proof system for disjoint parallel quantum programs
- Monadic second-order incorrectness logic for GP 2
- Incorrectness logic for graph programs
- Certified verification of relational properties
- Verification of concurrent programs using Petri net unfoldings
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Fifty years of Hoare's logic
- Proof pearl: The KeY to correct and stable sorting
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- Verification of programs with half-duplex communication
- Highly dependable concurrent programming using design for verification
- Specification and verification challenges for sequential object-oriented programs
- Concurrency verification. Introduction to compositional and noncompositional methods
- Verification of fine-grain concurrent programs
- A Hoare logic for SIMT programs
- UTP semantics for rTiMo
- Proving Quicksort Correct in Event-B
- Introduction to model checking
- Being and change: reasoning about invariance
- scientific article; zbMATH DE number 44976 (Why is no real title available?)
- scientific article; zbMATH DE number 50008 (Why is no real title available?)
- scientific article; zbMATH DE number 548908 (Why is no real title available?)
- Programmverifikation
- Experiments in program verification using Event-B
- Verification of object-oriented programs: a transformational approach
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Starvation-free mutual exclusion with semaphores
- scientific article; zbMATH DE number 1836374 (Why is no real title available?)
- A proof system for adaptable class hierarchies
- Automated Verification of Concurrent Search Structures
- scientific article; zbMATH DE number 7440211 (Why is no real title available?)
- scientific article; zbMATH DE number 7453193 (Why is no real title available?)
- scientific article; zbMATH DE number 7456049 (Why is no real title available?)
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Using Hoare logic in a process algebra setting
- A simple, verified validator for software pipelining
- A Hoare Logic for GPU Kernels
- Incremental reasoning with lazy behavioral subtyping for multiple inheritance
- Indexed and fibered structures for partial and total correctness assertions
- Semantic embedding for quantum algorithms
- Concise outlines for a complex logic: a proof outline checker for TaDA
- A dynamic logic with branching modalities
- Denotational and algebraic semantics for the CaIT calculus
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- Rely-guarantee reasoning for causally consistent shared memory
- When are software verification results valid for approximate hardware?
- Kleene algebra of weighted programs with domain
- SSCalc: a calculus for Solidity smart contracts
- Gale-Shapley verified
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Toward automatic verification of quantum programs
- Alignment complete relational Hoare logics for some and all
- Three ways of proving termination of loops
- Algebras for iteration and infinite computations
- Tony Hoare: his path to the ACM Turing Award
- ConcurrentHOL
- Building program construction and verification tools from algebraic principles
- Correctness and concurrent complexity of the black-white bakery algorithm
- Verifying traits: an incremental proof system for fine-grained reuse
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Proof systems for planning under 0-approximation semantics
This page was built for publication: Verification of sequential and concurrent programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q837527)
