Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). Ádam, Z., Levente, B., Dobos-Kovács, M., Hajdu, Á., & Molnár, V. In Tools and Algorithms for the Construction and Analysis of Systems, volume 13244, of Lecture Notes in Computer Science, pages 474–478. Springer, 2022.
Pdf
Link doi abstract bibtex 2 downloads Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.
@incollection{tacas2022,
author = {{\'A}dam, Zs{\'o}fia and Levente, Bajczi and Dobos-Kov{\'a}cs, Mih{\'a}ly and Hajdu, {\'A}kos and Moln{\'a}r, Vince},
title = {{T}heta: portfolio of {CEGAR}-based analyses with dynamic algorithm selection (Competition Contribution)},
year = {2022},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
series = {Lecture Notes in Computer Science},
volume = {13244},
pages = {474--478},
publisher = {Springer},
doi = {10.1007/978-3-030-99527-0_34},
type = {Conference},
url_pdf = {https://hajduakos.github.io/publications/tacas2022.pdf},
url_link = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_34},
abstract = {Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.},
}
Downloads: 2
{"_id":"LTBmXgZBm2wJqczS5","bibbaseid":"dam-levente-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022","author_short":["Ádam, Z.","Levente, B.","Dobos-Kovács, M.","Hajdu, Á.","Molnár, V."],"bibdata":{"bibtype":"incollection","type":"Conference","author":[{"propositions":[],"lastnames":["Ádam"],"firstnames":["Zsófia"],"suffixes":[]},{"propositions":[],"lastnames":["Levente"],"firstnames":["Bajczi"],"suffixes":[]},{"propositions":[],"lastnames":["Dobos-Kovács"],"firstnames":["Mihály"],"suffixes":[]},{"propositions":[],"lastnames":["Hajdu"],"firstnames":["Ákos"],"suffixes":[]},{"propositions":[],"lastnames":["Molnár"],"firstnames":["Vince"],"suffixes":[]}],"title":"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)","year":"2022","booktitle":"Tools and Algorithms for the Construction and Analysis of Systems","series":"Lecture Notes in Computer Science","volume":"13244","pages":"474–478","publisher":"Springer","doi":"10.1007/978-3-030-99527-0_34","url_pdf":"https://hajduakos.github.io/publications/tacas2022.pdf","url_link":"https://link.springer.com/chapter/10.1007/978-3-030-99527-0_34","abstract":"Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.","bibtex":"@incollection{tacas2022,\n author = {{\\'A}dam, Zs{\\'o}fia and Levente, Bajczi and Dobos-Kov{\\'a}cs, Mih{\\'a}ly and Hajdu, {\\'A}kos and Moln{\\'a}r, Vince},\n title = {{T}heta: portfolio of {CEGAR}-based analyses with dynamic algorithm selection (Competition Contribution)},\n year = {2022},\n booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\n series = {Lecture Notes in Computer Science},\n volume = {13244},\n pages = {474--478},\n publisher = {Springer},\n doi = {10.1007/978-3-030-99527-0_34},\n\n type = {Conference},\n\n url_pdf = {https://hajduakos.github.io/publications/tacas2022.pdf},\n url_link = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_34},\n abstract = {Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.},\n}\n\n","author_short":["Ádam, Z.","Levente, B.","Dobos-Kovács, M.","Hajdu, Á.","Molnár, V."],"key":"tacas2022","id":"tacas2022","bibbaseid":"dam-levente-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022","role":"author","urls":{" pdf":"https://hajduakos.github.io/publications/tacas2022.pdf"," link":"https://link.springer.com/chapter/10.1007/978-3-030-99527-0_34"},"metadata":{"authorlinks":{}},"downloads":2},"bibtype":"incollection","biburl":"https://hajduakos.github.io/publications.bib","dataSources":["WFubm6dru5DutkSZW"],"keywords":[],"search_terms":["theta","portfolio","cegar","based","analyses","dynamic","algorithm","selection","competition","contribution","ádam","levente","dobos-kovács","hajdu","molnár"],"title":"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)","year":2022,"downloads":2}