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