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

DOI10.1016/0304-3975(90)90201-RMaRDI QIDQ912596zbMATH OpenOpenAlexFDO

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

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)

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; zbMATH DE number 3883587
• 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

Cites work

• scientific article; zbMATH DE number 3140027 (Why is no real title available?)
• scientific article; zbMATH DE number 3576680 (Why is no real title available?)
• A variant of a recursively unsolvable problem
• Functional equivalence of discrete processors. II
• On formalised computer programs
• The equivalence problem for deterministic two-tape automata
• Äquivalente Transformationen für Flußdiagramme

Cited in

(8)

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

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)