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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) 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)

• Update schedules of sequential dynamical systems
• 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
• A dynamic logic with traces and coinduction
• Fluid updates: beyond strong vs. weak updates
• Predicate Abstraction in a Program Logic Calculus
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Verification by Parallelization of Parametric Code
• Predicate abstraction in a program logic calculus
• Partial updates
• Integration of a security type system into a program logic

Describes a project that uses

Uses Software

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

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)