دورية أكاديمية
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 |
تدمد: | 18605974 |
---|---|
DOI: | 10.46298/lmcs-18(3:26)2022 |