Automated verification of relational while-programs

DOI10.1007/978-3-319-06251-8_11MaRDI QIDQ5410484zbMATH OpenOpenAlexFDO

Authors Rudolf Berghammer, Peter Höfner, Insa Stucke

Publication date 16 April 2014

Published in Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-06251-8_11

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On automated program construction and verification
• Exploiting synchrony and symmetry in relational verification
• Automated verification of recursive programs with pointers
• scientific article; zbMATH DE number 1696591
• scientific article; zbMATH DE number 1953018

Cited in

(13)

• Solving quantifier-free first-order constraints over finite sets and binary relations
• Tool-Based Verification of a Relational Vertex Coloring Program
• Exploiting synchrony and symmetry in relational verification
• Cryptomorphic topological structures: a computational, relation-algebraic approach
• Using relation-algebraic means and tool support for investigating and computing bipartitions
• Cardinality of relations with applications
• Control of Condorcet voting: complexity and a relation-algebraic approach
• Relational characterisations of paths
• Cardinality of relations and relational approximation algorithms
• On automated program construction and verification
• Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures
• A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
• Automated verification of reactive and concurrent programs by calculation

Describes a project that uses

Uses Software

• RALL
• ARA
• Ralf
• Mace4
• Prover9
• SPASS
• Isabelle/HOL
• RelView

This page was built for publication: Automated verification of relational while-programs

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