Verification of Array, Record, and Pointer Operations in Pascal

DOI10.1145/357073.357078zbMath0452.68014OpenAlexW2048168398MaRDI QIDQ3899469

Norihisa Suzuki, David C. Luckham

Publication date: 1979

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/357073.357078

zbMATH Keywords

formal semanticsPascaldata structuresaxiomatic semanticsprogram verificationarrayrecordstorage allocationpointers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items (7)

Doomed program points ⋮ Hoare's logic and Peano's arithmetic ⋮ A program logic for resources ⋮ Verification of finite iterations over collections of variable data structures ⋮ Symbolic method of verification of definite iterations over altered data structures ⋮ Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs ⋮ A logical analysis of aliasing in imperative higher-order functions

This page was built for publication: Verification of Array, Record, and Pointer Operations in Pascal