scientific article; zbMATH DE number 3740740
From MaRDI portal
Publication:3925859
Cited in
(only showing first 100 items - show all)- Mathematics for reasoning about loop functions
- Programs as proofs: A synopsis
- A presentation of the Fibonacci algorithm
- On the decomposition of sequences into ascending subsequences
- Equivalence of the Gries and Martin proof rules for procedure calls
- A categorical treatment of pre- and post-conditions
- The formal development of a parallel program performing LU-decomposition
- A sharp proof rule for procedures in WP semantics
- Generation of convex polygons with individual angular constraints
- A calculus of refinements for program derivations
- An exercise in proving self-stabilization with a variant function
- Finite generation of ambiguity in context-free languages
- Datalogy - the Copenhagen tradition of computer science
- Repetitions, known or unknown?
- Weakest preconditions for progress
- Alternative developments of cyclic-permutation algorithms
- Random list permutations in place
- Non-associative parallel prefix computation
- A proof rule for while loop in VDM
- Theories for mechanical proofs of imperative programs
- Formal derivation of graph algorithmic programs using partition-and-recur
- Convergence of iteration systems
- On the mechanical derivation of loop invariants
- Program refinement in fair transition systems
- Normal form approach to compiler design
- A Gentzen system for conditional logic
- Proof rules for recursive procedures
- Correct translation of data parallel assignment onto array processors
- Modularity and reusability in attribute grammars
- Formal specification of parallel SIMD execution
- Implementing (nondeterministic) parallel assignments
- The formal specification of abstract data types and their implementation in Fortran 90
- A theory of nonmonotonic rule systems I
- Running programs backwards: The logical inversion of imperative computation
- Optimal algorithms for generalized searching in sorted matrices
- Automatic differentiation of algorithms
- Convergence: integrating termination and abort-freedom
- Power structures
- Weakest pre-condition reasoning for Java programs with JML annotations
- S- and T-invariants in cyber net systems
- Unification: A case-study in data refinement
- Predicate transformers as power operations
- A logical framework for evolving software systems
- The co-invariant generator: An aid in deriving loop bodies
- Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
- Determinization of inverted grammar programs via context-free expressions
- Algorithm design through the optimization of reuse-based generation
- Symbolic execution formally explained
- A unified approach of program verification
- Differentiators and detectors
- Verifying Whiley programs with Boogie
- Algorithmically broad languages for polynomial time and space
- Why there is no general solution to the problem of software verification
- General correctness: A unification of partial and total correctness
- Fifty years of Hoare's logic
- Quasi-boolean equivalence
- A relational division operator: The conjugate kernel
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Specification and verification challenges for sequential object-oriented programs
- Reversible computing from a programming language perspective
- Non-deterministic expressions and predicate transformers
- Weakest preconditions for pure Prolog programs
- A relation-algebraic approach to multirelations and predicate transformers
- Computing Preconditions and Postconditions of While Loops
- Loop invariants, exploration of regularities, and mathematical games
- The use of hoare logic in the verification of horizontal microprograms
- Program development by inductive stepwise refinement
- Forced termination of loops
- Reversing parallel programs with blocks and procedures
- Inferring Loop Invariants Using Postconditions
- Bisimilarity Minimization in O(m logn) Time
- A Formal Derivation of an 0(log n) Algorithm for Computing Fibonacci Numbers
- Some Variants of the Weakest Precondition in Nondeterminism
- Formal Techniques for Deriving Binary Search Algorithms
- Control problems in a temporal logic framework
- A New Programming Technique Derived from Dijkstra’s Methodology
- Programming with generators
- Tight Ω(nlgn) lower bound for finding a longest increasing subsequence
- A versatile concept for the analysis of loops
- AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
- Deriving dense linear algebra libraries
- Program derivation with verified transformations — a case study
- Definite descriptions and Dijkstra's odd powers of odd integers problem
- Reversing imperative parallel programs
- Clean reversible simulations of ranking binary trees
- Loop invariants: analysis, classification, and examples
- Representing proof transformations for program optimization
- Primitive recursion in the abstract
- Polynomial-time inverse computation for accumulative functions with multiple data traversals
- Toward an Automatic Approach to Greedy Algorithms
- An independent axiomatisation for free short-circuit logic
- Reasoning in Dynamic Logic about Program Termination
- Auxiliary variables in partial correctness programming logics
- An axiomatic treatment of SIMD assignment
- Non-commutative propositional logic with short-circuit evaluation
- On calculational proofs
- Cardinality of relations and relational approximation algorithms
- Reflexive transitive invariant relations: A basis for computing loop functions
- An elementary and unified approach to program correctness
- \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3925859)
