Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Trust and Automation in Verification Tools
verfasst von : Natarajan Shankar
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
On the one hand, we would like verification tools to feature powerful automation, but on the other hand, we also want to be able to trust the results with a high degree of confidence. The question of trust in verification tools has been debated for a long time. One popular way of achieving trust in verification tools is through proof generation. However, proof generation could hamstring both the functionality and the efficiency of the automation that can be built into these tools. We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach where the results of untrusted verifiers are checked by a trusted offline checker. The trusted checker is a verified reference kernel that contains a satisfiability solver to support the robust and efficient checking of untrusted tools.