Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs

DOI10.1007/978-3-540-78127-1_29zbMath1133.68322OpenAlexW1805056271MaRDI QIDQ5452196

V. A. Nepomniaschy

Publication date: 25 March 2008

Published in: Pillars of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78127-1_29

Mathematics Subject Classification ID

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

Cites Work

• Elimination of loop invariants in program verification
• Problem-oriented program verification
• Symbolic verification method for definite iteration over data structures
• Problem-oriented verification system and its application to linear algebra programs
• Symbolic method of verification of definite iterations over altered data structures
• Verification of Array, Record, and Pointer Operations in Pascal
• Some ideas on data types in high-level languages
• Computer Aided Verification
• An axiomatic basis for computer programming
• A note on the for statement
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs