On automated program construction and verification

DOI10.1007/978-3-642-13321-3_4MaRDI QIDQ3575262zbMATHOpenAlexFDO

Authors Rudolf Berghammer, Georg Struth

Publication date 26 July 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-13321-3_4

Mathematics Subject Classification ID

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

Recommendations

• Automated program verification
• Building program construction and verification tools from algebraic principles
• From program verification to program synthesis
• Automated verification of relational while-programs
• scientific article; zbMATH DE number 4024753

Cited in

(20)

• scientific article; zbMATH DE number 2040721 (Why is no real title available?)
• Efficient verification of imperative programs using auto2
• Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures
• Relation-algebraic verification of disjoint-set forests
• Cardinality of relations with applications
• Program semantics and verification technique for AI-centred programs
• Relational characterisations of paths
• An integrated approach to high integrity software verification
• Integrated approach to analysis and verification of imperative programs
• Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
• Theoretical Aspects of Computing - ICTAC 2004
• scientific article; zbMATH DE number 2217740 (Why is no real title available?)
• Using relation-algebraic means and tool support for investigating and computing bipartitions
• Second-order properties of undirected graphs
• A FOOLish encoding of the next state relations of imperative programs
• Automated program verification
• Simple rectangle-based functional programs for computing reflexive-transitive closures
• Automated verification of relational while-programs
• Cardinality of relations and relational approximation algorithms
• scientific article; zbMATH DE number 4074538 (Why is no real title available?)

Describes a project that uses

Uses Software

• RelView
• Prover9
• Mace4

This page was built for publication: On automated program construction and verification

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