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
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 ⋮ Program Verification with Separation Logic ⋮ A constructive approach to the problem of program correctness ⋮ Programming by action clusters ⋮ Proving programs correct: Some techniques and examples ⋮ An experiment in structured programming ⋮ Algebra-Based Loop Analysis ⋮ From interface automata to hypercontracts ⋮ Embedded domain specific verifiers ⋮ Limits and difficulties in the design of under-approximation abstract domains ⋮ Semantic embedding for quantum algorithms ⋮ Formal verification of termination criteria for first-order recursive functions ⋮ A note on the for statement ⋮ Liminf progress measures ⋮ Symbolic computation in automated program reasoning ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Unnamed Item ⋮ Logical models of discrete even systems: a comparative exposition ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation ⋮ Credible autocoding of convex optimization algorithms ⋮ Unnamed Item ⋮ The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Specifications can make programs run faster ⋮ Trees, ordinals and termination ⋮ A tree-based approach to data flow proofs ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Testing ⋮ Combining Model Checking and Deduction ⋮ Transfer of Model Checking to Industrial Practice ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Hoare Logic for the State Monad ⋮ An Introduction to Certificate Translation ⋮ Why there is no general solution to the problem of software verification ⋮ Unnamed Item ⋮ Recursion Equations as a Programming Language ⋮ Nominative data with ordered set of names ⋮ Implementation of the composition-nominative approach to program formalization in Mizar ⋮ Applying abstraction and formal specification in numerical software design ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Unnamed Item ⋮ Empowering the Event-B method using external theories ⋮ Certified verification of relational properties ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Parallélisation sémantique ⋮ The refinement calculus of reactive systems ⋮ Horn Clause Solvers for Program Verification ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Méthode axiomatique sur les propriétés de fatalité des programmes parallèles ⋮ Separation logics and modalities: a survey ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ WhyMP, a formally verified arbitrary-precision integer library ⋮ Unnamed Item ⋮ Simple-named complex-valued nominative data -- definition and basic operations ⋮ Weakest preconditioned goto axiom ⋮ Closed-form upper bounds in static cost analysis ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ DISTANCES BETWEEN FORMAL THEORIES ⋮ Unnamed Item ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Type-theoretic approaches to ordinals ⋮ Matrix Code ⋮ Unnamed Item ⋮ Action systems in incremental and aspect-oriented modeling ⋮ A Formalized Theory for Verifying Stability and Convergence of Automata in PVS ⋮ Predicate transformers in the context of symbolic modeling of transition systems ⋮ Polynomial invariants for linear loops ⋮ How to Brew-up a Refinement Ordering ⋮ The new programming discipline ⋮ Computation of resource requirements ⋮ Graded Hoare logic and its categorical semantics ⋮ A linked forest manipulation system semantics rules for an attributed translation grammar for PL/0 ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ Unifying theories of reactive design contracts ⋮ Verification of Concurrent Systems with VerCors ⋮ Loop invariants ⋮ Tableaux for constructive concurrent dynamic logic ⋮ A method of proving the invariance of linear inequalities for linear loops ⋮ Turing's 1949 paper in context ⋮ Mechanised Wire-wise Verification of Handel-C Synthesis ⋮ An assertion-based proof system for multithreaded Java ⋮ Meanings of Model Checking ⋮ Unnamed Item ⋮ A brief history of process algebra ⋮ Relation algebra as programming language using the Ampersand compiler ⋮ Fifty years of Hoare's logic ⋮ Induced acyclic tournaments in random digraphs: sharp concentration, thresholds and algorithms ⋮ From Proposition to Program ⋮ Many-sorted hybrid modal languages ⋮ Invariant Synthesis for Combined Theories ⋮ Kleene algebra of partial predicates ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ SAT-Based Model Checking without Unrolling ⋮ Decision Procedures for Automating Termination Proofs ⋮ The geometry of conservative programs ⋮ An abstract contract theory for programs with procedures ⋮ Using well-founded relations for proving operational termination ⋮ A ``geometric view of the dynamics of trajectories of computer programs ⋮ REF-ARF: A system for solving problems stated as procedures ⋮ Mathematical theory of partial correctness ⋮ Current methods for proving program correctness ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ Pair grammars, graph languages and string-to-graph translations ⋮ Algorithmic approximations ⋮ Translating recursion equations into flow charts ⋮ An interpretation-oriented theorem prover over integers ⋮ A formal model of atomicity in asynchronous systems ⋮ Dynamic Epistemic Logics ⋮ On homomorphisms, correctness, termination, unfoldments, and equivalence of flow diagram programs ⋮ Distributed automata in an assumption-commitment framework ⋮ Partial correctness of a factorial algorithm ⋮ Partial correctness of a power algorithm ⋮ Module checking ⋮ Blame and coercion: Together again for the first time ⋮ Partial correctness of a Fibonacci algorithm
