دورية أكاديمية
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
| العنوان: | Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays |
|---|---|
| المؤلفون: | Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett |
| المصدر: | Logical Methods in Computer Science, Vol Volume 18, Issue 3 (2022) |
| بيانات النشر: | Logical Methods in Computer Science e.V., 2022. |
| سنة النشر: | 2022 |
| المجموعة: | LCC:Logic LCC:Electronic computers. Computer science |
| مصطلحات موضوعية: | computer science - logic in computer science, Logic, BC1-199, Electronic computers. Computer science, QA75.5-76.95 |
| الوصف: | We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential. |
| نوع الوثيقة: | article |
| وصف الملف: | electronic resource |
| اللغة: | English |
| تدمد: | 1860-5974 |
| العلاقة: | https://lmcs.episciences.org/8436/pdfTest; https://doaj.org/toc/1860-5974Test |
| DOI: | 10.46298/lmcs-18(3:26)2022 |
| الوصول الحر: | https://doaj.org/article/af77f4ffff944dc5b9b4fa94be3184e8Test |
| رقم الانضمام: | edsdoj.f77f4ffff944dc5b9b4fa94be3184e8 |
| قاعدة البيانات: | Directory of Open Access Journals |
Full Text Finder | تدمد: | 18605974 |
|---|---|
| DOI: | 10.46298/lmcs-18(3:26)2022 |