On algebras of algorithms and specifications over uninterpreted data

DOI10.2478/FORMA-2018-0011zbMath1422.68033OpenAlexW2907318475WikidataQ128651680 ScholiaQ128651680MaRDI QIDQ2311521

Ievgen Ivanov, Artur Korniłowicz, Mykola Nikitchenko

Publication date: 10 July 2019

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2018-0011

zbMATH Keywords

Glushkov algorithmic algebrauninterpreted data

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) General topics in the theory of algorithms (68W01) General topics in the theory of data (68P01)

Related Items (5)

General theory and tools for proving algorithms in nominative data systems ⋮ Partial correctness of an algorithm computing Lucas sequences ⋮ Partial correctness of a factorial algorithm ⋮ Partial correctness of a power algorithm ⋮ Partial correctness of a Fibonacci algorithm

Uses Software

• Mizar

Cites Work

• Event-based proof of the mutual exclusion property of Peterson's algorithm
• Four decades of {\textsc{Mizar}}. Foreword
• Proving properties of programs on hierarchical nominative data
• Implementation of the composition-nominative approach to program formalization in Mizar
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Simple-named complex-valued nominative data -- definition and basic operations
• Kleene algebra of partial predicates
• On Representations of Abstract Systems with Partial Inputs and Outputs
• On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems

This page was built for publication: On algebras of algorithms and specifications over uninterpreted data