Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.
Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System
BERNARDESCHI, CINZIA;DOMENICI, ANDREA
2016-01-01
Abstract
Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
ipl16pp.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
180.08 kB
Formato
Adobe PDF
|
180.08 kB | Adobe PDF | Visualizza/Apri |
|
1-s2.0-S0020019016300072-main.pdf
solo utenti autorizzati
Tipologia:
Versione finale editoriale
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
326.21 kB
Formato
Adobe PDF
|
326.21 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
