Software Model Checking with a Combination of Explicit Values and Predicates. Bajkai, V. D. & Hajdu, Á. In Proceedings of the 26th PhD Mini-Symposium, pages 4–7, 2019. Budapest University of Technology and Economics, Department of Measurement and Information Systems. ![Software Model Checking with a Combination of Explicit Values and Predicates [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Pdf doi abstract bibtex Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.
@inproceedings{minisy2019,
author = {Bajkai, Vikt{\'o}ria Dorina and Hajdu, \'{A}kos},
title = {Software Model Checking with a Combination of Explicit Values and Predicates},
year = {2019},
booktitle = {Proceedings of the 26th PhD Mini-Symposium},
location = {Budapest, Hungary},
publisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
editor = {Pataki, B\'{e}la},
pages = {4--7},
isbn = {978-963-313-314-9},
doi = {10.5281/zenodo.2597969},
type = {Local event},
url_pdf = {minisy2019.pdf},
abstract = {Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.},
}
Downloads: 0
{"_id":"mu3cyhivFCqxMPWrT","bibbaseid":"bajkai-hajdu-softwaremodelcheckingwithacombinationofexplicitvaluesandpredicates-2019","downloads":0,"creationDate":"2019-03-18T14:36:21.081Z","title":"Software Model Checking with a Combination of Explicit Values and Predicates","author_short":["Bajkai, V. D.","Hajdu, Á."],"year":2019,"bibtype":"inproceedings","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","bibdata":{"bibtype":"inproceedings","type":"Local event","author":[{"propositions":[],"lastnames":["Bajkai"],"firstnames":["Viktória","Dorina"],"suffixes":[]},{"propositions":[],"lastnames":["Hajdu"],"firstnames":["Ákos"],"suffixes":[]}],"title":"Software Model Checking with a Combination of Explicit Values and Predicates","year":"2019","booktitle":"Proceedings of the 26th PhD Mini-Symposium","location":"Budapest, Hungary","publisher":"Budapest University of Technology and Economics, Department of Measurement and Information Systems","editor":[{"propositions":[],"lastnames":["Pataki"],"firstnames":["Béla"],"suffixes":[]}],"pages":"4–7","isbn":"978-963-313-314-9","doi":"10.5281/zenodo.2597969","url_pdf":"minisy2019.pdf","abstract":"Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.","bibtex":"@inproceedings{minisy2019,\n author = {Bajkai, Vikt{\\'o}ria Dorina and Hajdu, \\'{A}kos},\n title = {Software Model Checking with a Combination of Explicit Values and Predicates},\n year = {2019},\n booktitle = {Proceedings of the 26th PhD Mini-Symposium},\n location = {Budapest, Hungary},\n publisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n editor = {Pataki, B\\'{e}la},\n pages = {4--7},\n isbn = {978-963-313-314-9},\n doi = {10.5281/zenodo.2597969},\n \n type = {Local event},\n url_pdf = {minisy2019.pdf},\n abstract = {Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.},\n}\n\n","author_short":["Bajkai, V. D.","Hajdu, Á."],"editor_short":["Pataki, B."],"key":"minisy2019","id":"minisy2019","bibbaseid":"bajkai-hajdu-softwaremodelcheckingwithacombinationofexplicitvaluesandpredicates-2019","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/minisy2019.pdf"},"metadata":{"authorlinks":{"hajdu, á":"https://hajduakos.github.io/publications.html"}},"downloads":0},"search_terms":["software","model","checking","combination","explicit","values","predicates","bajkai","hajdu"],"keywords":[],"authorIDs":["3MgKtuPWy9PwMYJmr","577d789d0fdaf8c97d0003e6","5LYbkbBcDuR3siWzy","5e00c3ba7a90b3de0100009b","5e0f08ae070585df01000057","5e1c2d686e1491df0100002d","5e38c96887bbe9de010000ce","5e42ecf8a6f4a6f2010001c2","5e4c2a7a2dc400de01000299","HaK67Q23SshcjnTTJ","KGDotEjHj6T9WPqWk","Nx3HmAKrog3NAxfzT","QGBCW6qyw4PZtbyhs","WhrpES4wBCtbFpLNM","XPzgtGXr6ehWupiqm","crKHGkb8tkwAiL2Kh","nsScN9wDXKgPDgG8Q","ycJpDkYPhR3b9ATbm"],"dataSources":["WFubm6dru5DutkSZW","7MDizr2BZojXoNdPN"]}