CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis
| Autor: | Karlheinz Friedberger |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
LOOP (programming language)
Computer science Programming language Memoization Value (computer science) 020207 software engineering 02 engineering and technology computer.software_genre CPAchecker 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer Software verification Abstraction (linguistics) Interpolation Block (data storage) |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662496732 TACAS |
| DOI: | 10.1007/978-3-662-49674-9_58 |
| Popis: | The software verification framework CPAchecker is built on basic approaches like CPA and CEGAR. The configuration for the SV-COMP'16 uses the concept of block-abstraction memoization and combines it with the parallel execution of value analysis and predicate analysis. The CEGAR loop uses a refinement strategy that prefers to refine the precision of the lightweight value analysis, such that the precision of the predicate analysis remains abstract and concise as long as possible. The usage of mature analyses like value analysis and predicate analysis allows us to bring together the potential of lazy abstraction and interpolation and the benefits of block-abstraction memoization. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|