Combining top-down and bottom-up techniques in program derivation

DOI10.1007/978-3-319-27436-2_15zbMATH Open1362.68042OpenAlexW2396953794MaRDI QIDQ5743597FDOQ5743597

Authors: Dipak L. Chaudhari, Om P. Damani 

Publication date: 5 February 2016

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-27436-2_15

Recommendations

• Assumption propagation through annotated programs
• Systematic program development
• scientific article; zbMATH DE number 1926610
• scientific article; zbMATH DE number 1302060
• scientific article; zbMATH DE number 1303991

zbMATH Keywords

program derivationcalculational style

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Cocktail: A tool for deriving correct programs
• Title not available (Why is that?)
• Why3 -- where programs meet provers
• Title not available (Why is that?)
• Refinement Calculus
• Title not available (Why is that?)
• Exercises in Quantifier Manipulation
• Guarded commands, nondeterminacy and formal derivation of programs
• A program refinement tool
• The derivation of systolic computations
• Title not available (Why is that?)

Cited In (2)

• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Assumption propagation through annotated programs

Uses Software

• Cocktail
• SPASS
• Why3
• cvc3
• z3
• Alt-Ergo
• WhyML

This page was built for publication: Combining top-down and bottom-up techniques in program derivation

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