This case study shows the use of ACL2 for the design verification of a selected piece of safety-critical software, called an Embedded Verifier. The Embedded Verifier chacks on-line that each execution of a safety-critical translator is correct. This study originates from an industrial partnership project
Design Verification of a Safety-Critical Embedded Verifier
Bertoli, Piergiorgio;Traverso, Paolo
2000-01-01
Abstract
This case study shows the use of ACL2 for the design verification of a selected piece of safety-critical software, called an Embedded Verifier. The Embedded Verifier chacks on-line that each execution of a safety-critical translator is correct. This study originates from an industrial partnership projectFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
