Automatic constrained rewriting induction towards verifying procedural programs

DOI10.1007/978-3-319-12736-1_18MaRDI QIDQ2789055zbMATH OpenOpenAlexFDO

Authors Cynthia Kop, Naoki Nishida

Publication date 26 February 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-12736-1_18

Mathematics Subject Classification ID

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

Recommendations

• Verifying procedural programs via constrained rewriting induction
• Verification of procedural programs
• Logic programs as specifications in the inductive verification of logic programs
• scientific article; zbMATH DE number 4024753
• Program verification using constraint handling rules and array constraint generalizations

Cited in

(8)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
• Verifying procedural programs via constrained rewriting induction
• Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
• Automatically proving termination and memory safety for programs with pointer arithmetic
• scientific article; zbMATH DE number 1540615 (Why is no real title available?)
• Rewriting modulo SMT and open system analysis
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems

This page was built for publication: Automatic constrained rewriting induction towards verifying procedural programs

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