Il settore della verifica automatica si occupa della elaborazione e validazione mediante elaboratori elettronici di certificati di correttezza. Gli strumenti in oggetto, chiamati abitualmente proof assistants o interactive provers, forniscono un ambiente interattivo per la costruzione di certificati formali la cui correttezza può essere determinata in modo completamente automatico. Questi strumenti hanno applicazioni sia in campo matematico, dove i certificati sono prove di teoremi, sia in campo informatico, dove i certificati argomentano la correttezza di un determinato software rispetto ad una sua specifica.
Andrea Asperti (2018). Verifica automatica e dimostrazione interattiva. Pisa : Edizioni ETS.
Verifica automatica e dimostrazione interattiva
Andrea Asperti
2018
Abstract
Il settore della verifica automatica si occupa della elaborazione e validazione mediante elaboratori elettronici di certificati di correttezza. Gli strumenti in oggetto, chiamati abitualmente proof assistants o interactive provers, forniscono un ambiente interattivo per la costruzione di certificati formali la cui correttezza può essere determinata in modo completamente automatico. Questi strumenti hanno applicazioni sia in campo matematico, dove i certificati sono prove di teoremi, sia in campo informatico, dove i certificati argomentano la correttezza di un determinato software rispetto ad una sua specifica.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
