Abstract
Software verification is the task of checking that computer programs work correctly on any valid input. Software verification is a basic concern of computer science and has been around since the first software was written.
This chapter shows that constraint databases can be useful for software verification.
Section 26.1 describes addition bound matrices, which are useful as a constraint representation in software verification.
Section 26.2 presents the abstract interpretation approach to software verification.
The octogonal abstract domain is used as an example of abstract interpretation methods. Section 26.3 describes the constraint database approach to software verification and compares it to the abstract interpretation approach.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag London
About this chapter
Cite this chapter
Revesz, P. (2010). Software Verification. In: Introduction to Databases. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84996-095-3_26
Download citation
DOI: https://doi.org/10.1007/978-1-84996-095-3_26
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-84996-094-6
Online ISBN: 978-1-84996-095-3
eBook Packages: Computer ScienceComputer Science (R0)