An algorithm deciding functional equivalence in a new class of program schemes

DOI10.1016/0304-3975(90)90201-RzbMATH Open0698.68016OpenAlexW2048338103MaRDI QIDQ912596FDOQ912596

Authors: Viktor K. Sabelfeld 

Publication date: 1990

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(90)90201-r

Recommendations

• Equivalence checking of two functional programs using inductive theorem provers
• Weak equivalence in a class of structured program schemes
• The equivalence problem and correctness formulas for a simple class of programs
• scientific article
• Program equivalence in linear contexts
• A polynomial-time algorithm that recognizes the commutative equivalence of program schemata
• Proving properties of functional programs by equality saturation
• An algebraic approach to schemes of structured programs
• scientific article; zbMATH DE number 4094778
• Implementation and Application of Automata

zbMATH Keywords

verificationtransformationdecidabilityprogram optimizationdecision algorithmequivalence of program schemes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Cites Work

• A variant of a recursively unsolvable problem
• On formalised computer programs
• The equivalence problem for deterministic two-tape automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Äquivalente Transformationen für Flußdiagramme
• Functional equivalence of discrete processors. II

Cited In (8)

• Equivalence of conservative, free, linear program schemas is decidable
• On the computational complexity of dynamic slicing problems for program schemas
• Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas
• Equivalence of linear, free, liberal, structured program schemas is decidable in polynomial time
• Algorithm for verifying the equivalence of linear unary recursive programs on ordered semigroup scales
• Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas
• Weak equivalence in a class of structured program schemes
• On the Decidability of the Equivalence Problem for Monadic Recursive Programs

This page was built for publication: An algorithm deciding functional equivalence in a new class of program schemes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q912596)