Program derivation with verified transformations — a case study

DOI10.1002/CPA.3160480906MaRDI QIDQ4884666zbMATH OpenOpenAlexFDO

Authors

Publication date 7 July 1996

Published in Communications on Pure and Applied Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/cpa.3160480906

zbMATH Keywords

verified program transformations

Mathematics Subject Classification ID

Theory of programming languages (68N15) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Publication:3034803
• Fast brief practical DFA minimization
• Proof-directed program transformation: a functional account of efficient regular expression matching
• The transformational approach to program development
• Representing proof transformations for program optimization

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A Transformation System for Developing Recursive Programs
• An algorithm for reduction of operator strength
• An Automatic Technique for Selection of Data Representations in SETL Programs
• An axiomatic basis for computer programming
• Automatic data structure choice in a language of very high level
• Constructive versions of Tarski's fixed point theorems
• scientific article; zbMATH DE number 3976287 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1331926 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3241254 (Why is no real title available?)
• Testing flow graph reducibility

Cited in

(7)

• Program derivation through transformations: The evolution of list-copying algorithms
• Formative processes with applications to the decision problem in set theory. I: Powerset and singleton operators
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• scientific article; zbMATH DE number 4133471 (Why is no real title available?)
• Verification of object-oriented programs: a transformational approach
• Goals and benchmarks for automated map reasoning
• Provably correct derivation of algorithms using FermaT

Describes a project that uses

Uses Software

• LARCH

This page was built for publication: Program derivation with verified transformations — a case study

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