On automated program construction and verification

DOI10.1007/978-3-642-13321-3_4zbMATH Open1286.68068OpenAlexW1536773907MaRDI QIDQ3575262FDOQ3575262

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)

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

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)