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

DOI10.1007/11916277_29MaRDI QIDQ5387908zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Partial updates
• Fluid updates: beyond strong vs. weak updates
• scientific article; zbMATH DE number 1951184
• Computer Aided Verification
• Logic for Programming, Artificial Intelligence, and Reasoning

Cited in

(13)

• Predicate abstraction in a program logic calculus
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Verification by Parallelization of Parametric Code
• Dynamic frames in Java dynamic logic
• Partial updates
• Fluid updates: beyond strong vs. weak updates
• Update schedules of sequential dynamical systems
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Specifying imperative ML-like programs using dynamic logic
• Integration of a security type system into a program logic
• Predicate Abstraction in a Program Logic Calculus
• Satisfiability solving and model generation for quantified first-order logic formulas
• A dynamic logic with traces and coinduction

Describes a project that uses

Uses Software

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

This page was built for publication: Sequential, Parallel, and Quantified Updates of First-Order Structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5387908)