FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers
| Autor: | David Sanán, Hao Xiao, Jun Sun, Henri Hansen, Yang Liu, Shang-Wei Lin |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Loop invariant
Computer science 020207 software engineering Forward backward 02 engineering and technology law.invention Program analysis Reachability law Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Invariant (mathematics) Transformer Algorithm |
| Zdroj: | ASE |
| DOI: | 10.1109/ase.2017.8115690 |
| Popis: | Loop invariant generation is a fundamental problem in program analysis and verification. In this work, we propose a new approach to automatically constructing inductive loop invariants. The key idea is to aggressively squeeze an inductive invariant based on Craig interpolants between forward and backward reachability analysis. We have evaluated our approach by a set of loop benchmarks, and experimental results show that our approach is promising. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|