Verification of sequential and concurrent programs

DOI10.1007/978-1-84882-745-5zbMATH Open1183.68361OpenAlexW2569787747MaRDI QIDQ837527FDOQ837527

Authors: Frank S. de Boer, Krzysztof R. Apt, Ernst-Rüdiger Olderog 

Publication date: 10 September 2009

Published in: Texts in Computer Science (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/14569

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

Mathematics Subject Classification ID

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

Cited In (60)

• A dynamic logic with branching modalities
• 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
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Concise outlines for a complex logic: a proof outline checker for TaDA
• Title not available (Why is that?)
• A UTP approach for rTiMo
• Proof pearl: The KeY to correct and stable sorting
• Title not available (Why is that?)
• Denotational and algebraic semantics for the CaIT calculus
• Reasoning about actions with loops via Hoare logic
• UTP semantics for rTiMo
• Fifty years of Hoare's logic
• A Hoare logic for SIMT programs
• Using Hoare logic in a process algebra setting
• 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?)
• 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
• Introduction to model checking
• 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
• Being and change: reasoning about invariance
• Specification and verification challenges for sequential object-oriented programs
• Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
• Concurrency verification. Introduction to compositional and noncompositional methods
• 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

Uses Software

• Isabelle/HOL
• PVS

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)