Treffer: Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction

Title:
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction
Authors:
Weiß, Benjamin
Publisher Information:
KIT Scientific Publishing
Publication Year:
2011
Collection:
Expeditio - Repositorio Institucional Universidad de Bogotá Jorge Tadeo Lozano (UTADEO)
Subject Terms:
Design by contract, Software specification, Software verification, Arquitectura de software, Desarrollo de software, Ingeniería de software
Document Type:
Buch book
File Description:
xxi, 269 páginas; application/pdf
Language:
English
ISBN:
978-3-86644-623-6
3-86644-623-3
Relation:
https://directory.doabooks.org/handle/20.500.12854/44626; http://hdl.handle.net/20.500.12010/17576
DOI:
10.5445/KSP/1000021694
Availability:
https://hdl.handle.net/20.500.12010/17576
https://directory.doabooks.org/handle/20.500.12854/44626
https://hdl.handle.net/20.500.12854/44626
https://doi.org/10.5445/KSP/1000021694
Rights:
info:eu-repo/semantics/openAccess ; Abierto (Texto Completo) ; https://creativecommons.org/licenses/by-nc-nd/4.0/
Accession Number:
edsbas.F9AE20EF
Database:
BASE

Weitere Informationen

Software systems play a central role in modern society, and their correctness is often crucially important. Formal specification and verification are promising approaches for ensuring correctness more rigorously than just by testing. This work presents an approach for deductively verifying design-by-contract specifications of object-oriented programs. The approach is based on dynamic logic, and addresses the challenges of modularity and automation using dynamic frames and predicate abstraction.