First-order dynamic logic

Publication date: 1979

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Semantics Correctness Axiomatizations Equivalence and Determinacy of Programs First-Order Dynamic Logic Flowchart Reasonning About Programs Recursive Programs

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Other nonclassical logic (03B60) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Algorithms in computer science (68W99)

Related Items (only showing first 100 items - show all)

Adding partial orders to linear temporal logic ⋮ Stateful Behavioral Types for Active Objects ⋮ Adversarial logic ⋮ Review of Logical Analysis of Hybrid Systems ⋮ Temporal stream logic modulo theories ⋮ A dynamic logic with branching modalities ⋮ A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3 ⋮ Unnamed Item ⋮ Proving correctness of labeled transition systems by semantic tableaux ⋮ Semantic models for total correctness and fairness ⋮ Regular database update logics ⋮ Reasoning in Dynamic Logic about Program Termination ⋮ Monadic dynamic algebras ⋮ Non-standard algorithmic and dynamic logic ⋮ Interval extensions of orders and temporal approximation spaces ⋮ Formal theories of knowledge in AI and robotics ⋮ A formalization of programs in first-order logic with a discrete linear order ⋮ Stratified least fixpoint logic ⋮ A model existence theorem in infinitary propositional modal logic ⋮ An algebraic study of well-foundedness ⋮ A simple dynamic logic ⋮ An overview of transaction logic ⋮ Positive program logics in systems with arithmetic ⋮ Combining Model Checking and Deduction ⋮ First-order approximation of algorithmic theories ⋮ Static and dynamic aspects of goal-oriented concurrency control ⋮ Predicate transformers as power operations ⋮ Arithmetical axiomatization of first-order temporal logic ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ Infinitary propositional normal modal logic ⋮ Intention is choice with commitment ⋮ Some relationships between logics of programs and complexity theory ⋮ An infinite pebble game and applications ⋮ Some general incompleteness results for partial correctness logics ⋮ Dynamic logic with program specifications and its relational proof system ⋮ Iterative and recursive matrix theories ⋮ Generalized hyperarithmetical computability over structures ⋮ An automata theoretic decision procedure for the propositional mu- calculus ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Free choice and contextually permitted actions ⋮ Towards reasoning about Hoare relations ⋮ Unnamed Item ⋮ Categories for Dynamic Epistemic Logic ⋮ Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic ⋮ On the total correctness of nondeterministic programs ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II ⋮ Arithmetical completeness in first-order dynamic logic for concurrent programs ⋮ Proving total correctness of nondeterministic programs in infinitary logic ⋮ On algebra of program correctness and incorrectness ⋮ A formal system for parallel programs in discrete time and space ⋮ Definability in dynamic logic ⋮ Branching versus linear logics yet again ⋮ Floyd's principle, correctness theories and program equivalence ⋮ A complete logic for reasoning about programs via nonstandard model theory. I ⋮ Proving total correctness of recursive procedures ⋮ On termination problems for finitely interpreted ALGOL-like programs ⋮ On logic of complex algorithms ⋮ Reuse of proofs in software verification ⋮ Mathematical modal logic: A view of its evolution ⋮ Process logic: Expressiveness, decidability, completeness ⋮ Étude et implémentation d'un système de déduction pour logique algorithmique ⋮ Unnamed Item ⋮ Domain theory in logical form ⋮ Precise quantitative information flow analysis -- a symbolic approach ⋮ Completing the temporal picture ⋮ Determinism and non-determinism in PDL ⋮ Toward automatic verification of quantum programs ⋮ On models for propositional dynamic logic ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ On the logic of UNITY ⋮ The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) ⋮ Axiomatizing fixpoint logics ⋮ Semantics and reasoning with free procedures ⋮ A compositional axiomatization of statecharts ⋮ Multimodal logic programming using equational and order-sorted logic ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ Semantic models for total correctness and fairness ⋮ Tableaux for constructive concurrent dynamic logic ⋮ Some applications of topology to program semantics ⋮ Modal logics for communicating systems ⋮ Predicative specifications for functional programs describing communicating networks ⋮ On strictly arithmetical completeness in logics of programs ⋮ A structured temporal logic language: XYZ/SE ⋮ Automata on infinite objects and their applications to logic and programming ⋮ On the Completeness of Dynamic Logic ⋮ Modelling knowledge and action in distributed systems ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Unnamed Item ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ Frame problem in dynamic logic ⋮ In Scott-Strachey style denotational semantics, parallelism implies nondeterminism ⋮ Differential dynamic logic for hybrid systems ⋮ Semantical analysis of constructive PDL ⋮ The temporal logic of branching time ⋮ On infinite computations in denotational semantics ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ The comparison of the expressive power of first-order dynamic logics ⋮ A probabilistic dynamic logic ⋮ Ten years of Hoare's logic: A survey. II: Nondeterminism ⋮ DAL -- a logic for data analysis

This page was built for publication: First-order dynamic logic