scientific article; zbMATH DE number 3302923

Cited in

(only showing first 100 items - show all)

Verifying programs by induction on their data structure: general format and applications
Process logic with regular formulas
Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
A simple fixpoint argument without the restriction to continuity
Non-standard algorithmic and dynamic logic
A complete rule for equifair termination
Controlling recursive inference
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
Inductive assertion method for logic pograms
Program termination using Z-transform theory
A language independent proof of the soundness and completeness of generalized Hoare logic
An approach for data type specification and its use in program verification
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
Arithmetical completeness in first-order dynamic logic for concurrent programs
A formal system for parallel programs in discrete time and space
Floyd's principle, correctness theories and program equivalence
Programs as partial graphs. I: Flow equivalence and correctness
Dynamic algebras: Examples, constructions, applications
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
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
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
Deriving correctness properties of compiled code
A functional logic for higher level reasoning about computation
Constructing specification morphisms
On the mechanical derivation of loop invariants
Logical debugging
On proving the termination of algorithms by machine
An algebraic approach to semantics of programming languages
On enumerating all minimal solutions of feedback problems
A methodology for designing proof rules for fair parallel programs
The validity of return address schemes
Hybrid I/O automata.
Verification, refinement and scheduling of real-time programs
Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
A tree-based approach to data flow proofs
Nominative data with ordered set of names
Implementation of the composition-nominative approach to program formalization in Mizar
Automatic synthesis of logical models for order-sorted first-order theories
VST-Floyd: a separation logic tool to verify correctness of C programs
Designing a semantic model for a wide-spectrum language with concurrency
Simple-named complex-valued nominative data -- definition and basic operations
An assertion-based proof system for multithreaded Java
A brief history of process algebra
Relation algebra as programming language using the Ampersand compiler
Kleene algebra of partial predicates
A ``geometric view of the dynamics of trajectories of computer programs
Hoare's logic for nondeterministic regular programs: A nonstandard approach
A formal model of atomicity in asynchronous systems
On homomorphisms, correctness, termination, unfoldments, and equivalence of flow diagram programs
Distributed automata in an assumption-commitment framework
Module checking
Applying abstraction and formal specification in numerical software design
Unifying theories of reactive design contracts
Turing's 1949 paper in context
Many-sorted hybrid modal languages
An abstract contract theory for programs with procedures
Partial correctness of a Fibonacci algorithm
Why there is no general solution to the problem of software verification
Empowering the Event-B method using external theories
Certified verification of relational properties
Parameterized synthesis for fragments of first-order logic over data words
A learning-based approach to synthesizing invariants for incomplete verification engines
Graded Hoare logic and its categorical semantics
RGITL: a temporal logic framework for compositional reasoning about interleaved programs
Compositional reasoning using intervals and time reversal
A method of proving the invariance of linear inequalities for linear loops
Fifty years of Hoare's logic
Using well-founded relations for proving operational termination
Partial correctness of a factorial algorithm
Partial correctness of a power algorithm
Credible autocoding of convex optimization algorithms
Closed-form upper bounds in static cost analysis
Matrix Code
Predicate transformers in the context of symbolic modeling of transition systems
Polynomial invariants for linear loops
Tableaux for constructive concurrent dynamic logic
Induced acyclic tournaments in random digraphs: sharp concentration, thresholds and algorithms
REF-ARF: A system for solving problems stated as procedures
Mathematical theory of partial correctness
Pair grammars, graph languages and string-to-graph translations
Algorithmic approximations
Translating recursion equations into flow charts

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 Q5584402)