Generation of correctness conditions for imperative programs

DOI10.1134/S0361768808060029zbMath1185.68424OpenAlexW2152238685MaRDI QIDQ840060

I. S. Anureev, E. V. Bodin, N. V. Shilov

Publication date: 4 September 2009

Published in: Programming and Computer Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1134/s0361768808060029

zbMATH Keywords

Floyd-Hoare

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Uses Software

• F@BOOL@

Cites Work

• An axiomatic definition of the programming language Pascal
• Avoiding exponential explosion
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item