Automatic Constrained Rewriting Induction towards Verifying Procedural Programs

DOI10.1007/978-3-319-12736-1_18zbMath1453.68050OpenAlexW26731332MaRDI QIDQ2789055

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

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

Related Items (5)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Rewriting modulo SMT and open system analysis ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Generalized rewrite theories, coherence completion, and symbolic methods

This page was built for publication: Automatic Constrained Rewriting Induction towards Verifying Procedural Programs