Verification of sequential and concurrent programs

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (57)

Gale-Shapley verified
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
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
Symbolic execution formally explained
RGITL: a temporal logic framework for compositional reasoning about interleaved programs
Unifying Operational Weak Memory Verification: An Axiomatic Approach
Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
Being and Change: Reasoning About Invariance
A proof system for disjoint parallel quantum programs
Title not available (Why is that?)
Concise outlines for a complex logic: a proof outline checker for TaDA
A dynamic logic with branching modalities
Title not available (Why is that?)
A UTP approach for rTiMo
Proof pearl: The KeY to correct and stable sorting
Denotational and algebraic semantics for the CaIT calculus
Reasoning about actions with loops via Hoare logic
Fifty years of Hoare's logic
Experiments in program verification using Event-B
Semantic embedding for quantum algorithms
Automated Verification of Concurrent Search Structures
Efficient verification of sequential and concurrent C programs
Verification of object-oriented programs: a transformational approach
Building program construction and verification tools from algebraic principles
A simple, verified validator for software pipelining
Highly dependable concurrent programming using design for verification
Indexed and fibered structures for partial and total correctness assertions
Algebras for iteration and infinite computations
Correctness and concurrent complexity of the black-white bakery algorithm
Title not available (Why is that?)
UTP Semantics for rTiMo
A Hoare Logic for SIMT Programs
Starvation-free mutual exclusion with semaphores
Proof systems for planning under 0-approximation semantics
Verification of fine-grain concurrent programs
Certified verification of relational properties
A proof system for adaptable class hierarchies
Incremental reasoning with lazy behavioral subtyping for multiple inheritance
Verification of programs with half-duplex communication
Verifying traits: an incremental proof system for fine-grained reuse
Proving correctness of imperative programs by linearizing constrained Horn clauses
Title not available (Why is that?)
Tournaments for mutual exclusion: verification and concurrent complexity
Proving Quicksort Correct in Event-B
Verification of concurrent programs using Petri net unfoldings
Specification and verification challenges for sequential object-oriented programs
Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
Using Hoare Logic in a Process Algebra Setting
Toward automatic verification of quantum programs
A Hoare Logic for GPU Kernels
Monadic second-order incorrectness logic for GP 2
Incorrectness logic for graph programs
Introduction to Model Checking

Uses Software

Isabelle/HOL
PVS

Recommendations

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)