AVR: Abstractly Verifying Reachability
| Autor: | Karem A. Sakallah, Aman Goel |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Model checking
Syntax (programming languages) State transition systems Programming language Computer science Design information 02 engineering and technology computer.software_genre 020202 computer hardware & architecture Reachability Scalability 0202 electrical engineering electronic engineering information engineering Key (cryptography) 020201 artificial intelligence & image processing Representation (mathematics) computer |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030451899 TACAS (1) |
| DOI: | 10.1007/978-3-030-45190-5_23 |
| Popis: | We present AVR, a push-button model checker for verifying state transition systems directly at the source-code level. AVR uses information embedded in the word-level syntax of the design representation to automatically perform scalable model checking by combining a novel syntax-guided abstraction-refinement technique with a word-level implementation of the IC3 algorithm. AVR provides independently-verifiable certificates that offer provable assurance and are easy to relate to the word-level system. Moreover, proof certificates can be further used in innovative ways to extract key design information and are useful in a growing number of applications. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|