Sequential, Parallel, and Quantified Updates of First-Order Structures

DOI10.1007/11916277_29zbMath1165.68376OpenAlexW1598846073MaRDI QIDQ5387908

Philipp Rümmer

Publication date: 27 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11916277_29

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A Dynamic Logic with Traces and Coinduction, Integration of a security type system into a program logic, Verification by Parallelization of Parametric Code, Predicate abstraction in a program logic calculus, Predicate Abstraction in a Program Logic Calculus, Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas, Specifying Imperative ML-Like Programs Using Dynamic Logic, Dynamic Frames in Java Dynamic Logic, Could We Have Chosen a Better Loop Invariant or Method Contract?, Abstract Interpretation of Symbolic Execution with Explicit State Updates

Uses Software

• Isabelle/HOL
• PVS
• Spec#
• ESC/Java
• KeY