scientific article; zbMATH DE number 3302923
From MaRDI portal
Publication:5584402
zbMath0189.50204MaRDI QIDQ5584402
Publication date: 1967
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (only showing first 100 items - show all)
Non-standard algorithmic and dynamic logic ⋮ Amorphous computing: examples, mathematics and theory ⋮ Mechanizing a process algebra for network protocols ⋮ Decision tree learning in CEGIS-based termination analysis ⋮ Analysis of linear definite iterative loops ⋮ A complete rule for equifair termination ⋮ On proving the termination of algorithms by machine ⋮ Generation of correctness conditions for imperative programs ⋮ Proof optimization for partial redundancy elimination ⋮ An algebraic approach to semantics of programming languages ⋮ On enumerating all minimal solutions of feedback problems ⋮ Controlling recursive inference ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ A method for computing the number of iterations in data dependent loops ⋮ Inductive assertion method for logic pograms ⋮ Program termination using Z-transform theory ⋮ An integrated approach to high integrity software verification ⋮ Recent advances in program verification through computer algebra ⋮ Formal correctness proofs of a nondeterministic program ⋮ The Schorr-Waite graph marking algorithm ⋮ A methodology for designing proof rules for fair parallel programs ⋮ Towards ``dynamic domains: totally continuous cocomplete \(\mathcal Q\)-categories ⋮ A language independent proof of the soundness and completeness of generalized Hoare logic ⋮ A compositional natural semantics and Hoare logic for low-level languages ⋮ Mechanical inference of invariants for FOR-loops ⋮ An elementary and unified approach to program correctness ⋮ An observationally complete program logic for imperative higher-order functions ⋮ On invariant checking ⋮ An approach for data type specification and its use in program verification ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ The validity of return address schemes ⋮ The structure of polynomial invariants of linear loops ⋮ Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II ⋮ Arithmetical completeness in first-order dynamic logic for concurrent programs ⋮ Mechanised wire-wise verification of Handel-C synthesis ⋮ A formal system for parallel programs in discrete time and space ⋮ Floyd's principle, correctness theories and program equivalence ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ A model of reconfiguration in communicating sequential processes ⋮ A survey of state vectors ⋮ Programs as partial graphs. I: Flow equivalence and correctness ⋮ Enabledness and termination in refinement algebra ⋮ Certifying algorithms ⋮ Verification conditions for source-level imperative programs ⋮ Hybrid I/O automata. ⋮ Nonlinear invariants for linear loops and eigenpolynomials of linear operators ⋮ Proving termination of nonlinear command sequences ⋮ A mechanical analysis of program verification strategies ⋮ Deductive verification of alternating systems ⋮ Property-directed incremental invariant generation ⋮ Dynamic algebras: Examples, constructions, applications ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Deriving bisimulation relations from path based equivalence checkers ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ Invariants for parameterised Boolean equation systems ⋮ A general criterion for avoiding infinite unfolding during partial deduction ⋮ Reasoning about programs ⋮ Proving assertions about parallel programs ⋮ Structured implementation of symbolic execution: A first part in a program verifier ⋮ Knowledge and reasoning in program synthesis ⋮ Alternating states for dual nondeterminism in imperative programming ⋮ SEMANOL (73), a metalanguage for programming the semantics of programming languages ⋮ The logical meaning of programs of a subrecursive language ⋮ Axiomatic approach to side effects and general jumps ⋮ A new look at the automatic synthesis of linear ranking functions ⋮ On the completeness of the inductive assertion method ⋮ Correctness of parallel programs: The Church-Rosser approach ⋮ On reduction of asynchronous systems ⋮ A proof method for cyclic programs ⋮ Proving programs correct through refinement ⋮ PASCAL in LCF: Semantics and examples of proof ⋮ Functional behavior in data spaces ⋮ A case for a forward predicate transformer ⋮ The correctness of the Schorr-Waite list marking algorithm ⋮ Formal derivation of strongly correct concurrent programs ⋮ Recursive assertions are not enough - or are they? ⋮ Program invariants as fixedpoints ⋮ Proving mutual termination ⋮ Constructive modal logics. I ⋮ The Hoare logic of concurrent programs ⋮ Semantics of algorithmic languages ⋮ Synthetic programming ⋮ Verifying programs by induction on their data structure: general format and applications ⋮ Verification, refinement and scheduling of real-time programs ⋮ Fair termination revisited - with delay ⋮ Deriving correctness properties of compiled code ⋮ Process logic with regular formulas ⋮ On verification of programs with goto statements ⋮ A functional logic for higher level reasoning about computation ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation ⋮ Translation and run-time validation of loop transformations ⋮ Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs ⋮ Constructing specification morphisms ⋮ On the mechanical derivation of loop invariants ⋮ Logical debugging ⋮ Computation of equilibria in noncooperative games ⋮ Nondeterministic semantics of compound diagrams ⋮ A simple fixpoint argument without the restriction to continuity
This page was built for publication:
