Skip to Main Content (Press Enter)

Logo UNITO
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione

UNI-FIND
Logo UNITO

|

UNI-FIND

unito.it
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione
  1. Pubblicazioni

Proof repositories for compositional verification of evolving software systems managing change when proving software correct

Capitolo di libro
Data di Pubblicazione:
2016
Abstract:
We propose a new and systematic framework for proof reuse in the context of deductive software verification. The framework generalizes abstract contracts into incremental proof repositories. Abstract contracts enable a separation of concerns between called methods and their implementations, facilitating proof reuse. Proof repositories allow the systematic caching of partial proofs that can be adapted to different method implementations. The framework provides flexible support for compositional verification in the context of, e.g., partly developed programs, evolution of programs and contracts, and product variability.
Tipologia CRIS:
02A-Contributo in volume
Keywords:
Theoretical Computer Science; Computer Science (all)
Elenco autori:
Bubel, Richard; Damiani, Ferruccio; Hähnle, Reiner; Johnsen, Einar Broch; Owe, Olaf; Schaefer, Ina; Yu, Ingrid Chieh
Autori di Ateneo:
DAMIANI Ferruccio
Link alla scheda completa:
https://iris.unito.it/handle/2318/1614422
Link al Full Text:
https://iris.unito.it/retrieve/handle/2318/1614422/267657/FoMaC-bdhjosy-2016-OPEN.pdf
Titolo del libro:
Transactions on Foundations for Mastering Change I
Pubblicato in:
LECTURE NOTES IN COMPUTER SCIENCE
Journal
LECTURE NOTES IN COMPUTER SCIENCE
Series
  • Dati Generali

Dati Generali

URL

http://springerlink.com/content/0302-9743/copyright/2005/
  • Utilizzo dei cookie

Realizzato con VIVO | Designed by Cineca | 25.6.1.0