Software and Computational Systems Lab

Publications of Karlheinz Friedberger

1. Dirk Beyer, Karlheinz Friedberger, and Stephan Holzner. PJBDD: A BDD Library for Java and Multi-Threading. In Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21 2021, Gold Coast (Online), Australia, October 18-22), 2021. Springer. doi:10.1007/978-3-030-88885-5_10 Keyword(s): PJBDD, BDD Funding: DFG-CONVEY Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.5070156
   Abstract

   PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.
   BibTeX Entry

   @inproceedings{ATVA21, author = {Dirk Beyer and Karlheinz Friedberger and Stephan Holzner}, title = {{PJBDD}: {A} {BDD} Library for {Java} and Multi-Threading}, booktitle = {Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21~2021, Gold Coast (Online), Australia, October 18-22)}, year = {2021}, publisher = {Springer}, doi = {10.1007/978-3-030-88885-5_10}, pdf = {https://www.sosy-lab.org/research/pub/2021-ATVA.PJBDD_A_BDD_Library_for_Java_and_Multi_Threading.pdf}, abstract = {PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.}, keyword = {PJBDD,BDD}, artifact = {10.5281/zenodo.5070156}, funding = {DFG-CONVEY}, }
2. Daniel Baier, Dirk Beyer, and Karlheinz Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In A. Silva and K. R. M. Leino, editors, Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021, Los Angeles, California, USA, July 18-24), LNCS 12760, pages 1-13, 2021. Springer. doi:10.1007/978-3-030-81688-9_9 Keyword(s): JavaSMT Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{CAV21, author = {Daniel Baier and Dirk Beyer and Karlheinz Friedberger}, title = {JavaSMT 3: Interacting with SMT Solvers in Java}, booktitle = {Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV~2021, Los Angeles, California, USA, July 18-24)}, editor = {A.~Silva and K.~R.~M.~Leino}, pages = {1-13}, year = {2021}, series = {LNCS~12760}, publisher = {Springer}, doi = {10.1007/978-3-030-81688-9_9}, sha256 = {6c0ff13c5dd8596e19be4176eefaafe5853d60a082b78ebd3f5e64381fdcb100}, url = {https://github.com/sosy-lab/java-smt}, abstract = {}, keyword = {JavaSMT}, _pdf = {https://www.sosy-lab.org/research/pub/2021-CAV.JavaSMT_3_Interacting_with_SMT_Solvers_in_Java.pdf}, funding = {DFG-CONVEY}, }
3. Dirk Beyer and Karlheinz Friedberger. Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization. In P. Devanbu, M. Cohen, and T. Zimmermann, editors, Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020, Virtual Event, USA, November 8-13), pages 50-62, 2020. ACM. doi:10.1145/3368089.3409718 Keyword(s): CPAchecker, Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.4024268
   BibTeX Entry

   @inproceedings{FSE20, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization}, booktitle = {Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE~2020, Virtual Event, USA, November 8-13)}, editor = {P.~Devanbu and M.~Cohen and T.~Zimmermann}, pages = {50-62}, year = {2020}, publisher = {ACM}, doi = {10.1145/3368089.3409718}, url = {https://cpachecker.sosy-lab.org}, keyword = {CPAchecker,Software Model Checking}, _sha256 = {36dc2a423425ee8bec03f0f4073e04f9121d299cc475e27190828e8276e00cb8}, artifact = {10.5281/zenodo.4024268}, funding = {DFG-CONVEY}, fundingid = {378803395}, }
4. Dirk Beyer and Karlheinz Friedberger. Violation Witnesses and Result Validation for Multi-Threaded Programs. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 449-470, 2020. Springer. doi:10.1007/978-3-030-61362-4_26 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
   BibTeX Entry

   @inproceedings{ISoLA20c, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Violation Witnesses and Result Validation for Multi-Threaded Programs}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {449-470}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_26}, sha256 = {65fc5325c4e77a80d8e47f9c0e7f0ac02379bfa15dcd9fb54d6587185b8efd77}, url = {https://www.sosy-lab.org/research/witnesses-concurrency/}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-25_ISOLA21_ValidationMultiThreaded_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, }
5. Dirk Beyer and Karlheinz Friedberger. In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching. In T. Margaria and B. Steffen, editors, Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2018, Part 2, Limassol, Cyprus, November 5-9), LNCS 11245, pages 197-215, 2018. Springer. doi:10.1007/978-3-030-03421-4_14 Keyword(s): CPAchecker, Software Model Checking, BAM Publisher's Version PDF Presentation Supplement
   Abstract

   Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, block summarization can be combined with counterexample-guided abstraction refinement (CEGAR). This causes the following problem: whenever CEGAR instructs the model checker to refine the abstraction along a path, several block summaries are affected and need to be updated. There exist two different refinement strategies: a destructive in-place approach that modifies the existing block abstractions and a constructive copy-on-write approach that does not change existing data. While the in-place approach is used in the field for several years, our new approach of copy-on-write refinement has the following important advantage: A complete exportable proof of the program is available after the analysis has finished. Due to the benefit from avoiding recomputations of missing information as necessary for in-place updates, the new approach causes almost no computational overhead overall. We perform a large experimental evaluation to compare the new approach with the previous one to show that full proofs can be achieved without overhead.
   BibTeX Entry

   @inproceedings{ISoLA18b, author = {Dirk Beyer and Karlheinz Friedberger}, title = {In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching}, booktitle = {Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2018, Part~2, Limassol, Cyprus, November 5-9)}, editor = {T.~Margaria and B.~Steffen}, pages = {197-215}, year = {2018}, series = {LNCS~11245}, publisher = {Springer}, doi = {10.1007/978-3-030-03421-4_14}, sha256 = {}, url = {https://www.sosy-lab.org/research/bam-cow-refinement/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ISoLA.In-Place_vs_Copy-on-Write_CEGAR_Refinement_for_Block_Summarization_with_Caching.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-11-06_ISoLA18_BAM-CoW-Refinement_Dirk.pdf}, abstract = {Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, block summarization can be combined with counterexample-guided abstraction refinement (CEGAR). This causes the following problem: whenever CEGAR instructs the model checker to refine the abstraction along a path, several block summaries are affected and need to be updated. There exist two different refinement strategies: a destructive in-place approach that modifies the existing block abstractions and a constructive copy-on-write approach that does not change existing data. While the in-place approach is used in the field for several years, our new approach of copy-on-write refinement has the following important advantage: A complete exportable proof of the program is available after the analysis has finished. Due to the benefit from avoiding recomputations of missing information as necessary for in-place updates, the new approach causes almost no computational overhead overall. We perform a large experimental evaluation to compare the new approach with the previous one to show that full proofs can be achieved without overhead.}, keyword = {CPAchecker,Software Model Checking,BAM}, }
6. Dirk Beyer and Karlheinz Friedberger. Domain-Independent Multi-threaded Software Model Checking. In Marianne Huchard, Christian Kästner, and Gordon Fraser, editors, Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pages 634-644, 2018. ACM. doi:10.1145/3238147.3238195 Keyword(s): CPAchecker, Software Model Checking, BAM Publisher's Version PDF Presentation Supplement
   Abstract

   Recent development of software aims at massively parallel execution, because of the trend to increase the number of processing units per CPU socket. But many approaches for program analysis are not designed to benefit from a multi-threaded execution and lack support to utilize multi-core computers. Rewriting existing algorithms is difficult and error-prone, and the design of new parallel algorithms also has limitations. An orthogonal problem is the granularity: computing each successor state in parallel seems too fine-grained, so the open question is to find the right structural level for parallel execution. We propose an elegant solution to these problems: Block summaries should be computed in parallel. Many successful approaches to software verification are based on summaries of control-flow blocks, large blocks, or function bodies. Block-abstraction memoization is a successful domain-independent approach for summary-based program analysis. We redesigned the verification approach of block-abstraction memoization starting from its original recursive definition, such that it can run in a parallel manner for utilizing the available computation resources without losing its advantages of being independent from a certain abstract domain. We present an implementation of our new approach for multi-core shared-memory machines. The experimental evaluation shows that our summary-based approach has no significant overhead compared to the existing sequential approach and that it has a significant speedup when using multi-threading.
   BibTeX Entry

   @inproceedings{ASE18a, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Domain-Independent Multi-threaded Software Model Checking}, booktitle = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated Software Engineering, {ASE} 2018, Montpellier, France, September 3-7, 2018}, editor = {Marianne Huchard and Christian K{\"{a}}stner and Gordon Fraser}, pages = {634-644}, year = {2018}, publisher = {ACM}, doi = {10.1145/3238147.3238195}, sha256 = {}, url = {https://www.sosy-lab.org/research/bam-parallel/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ASE.Domain-Independent_Multi-threaded_Software_Model_Checking.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-09-07_ASE18_ParallelBAM_Karlheinz.pdf}, abstract = {Recent development of software aims at massively parallel execution, because of the trend to increase the number of processing units per CPU socket. But many approaches for program analysis are not designed to benefit from a multi-threaded execution and lack support to utilize multi-core computers. Rewriting existing algorithms is difficult and error-prone, and the design of new parallel algorithms also has limitations. An orthogonal problem is the granularity: computing each successor state in parallel seems too fine-grained, so the open question is to find the right structural level for parallel execution. We propose an elegant solution to these problems: Block summaries should be computed in parallel. Many successful approaches to software verification are based on summaries of control-flow blocks, large blocks, or function bodies. Block-abstraction memoization is a successful domain-independent approach for summary-based program analysis. We redesigned the verification approach of block-abstraction memoization starting from its original recursive definition, such that it can run in a parallel manner for utilizing the available computation resources without losing its advantages of being independent from a certain abstract domain. We present an implementation of our new approach for multi-core shared-memory machines. The experimental evaluation shows that our summary-based approach has no significant overhead compared to the existing sequential approach and that it has a significant speedup when using multi-threading.}, keyword = {CPAchecker,Software Model Checking,BAM}, }
7. Pavel Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, and Anton Volkov. CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution). In Axel Legay and Tiziana Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 355-359, 2017. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-54580-5_22 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
   Abstract

   Our submission to SV-COMP'17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the version of SV-COMP'16. A novelty of our approach is usage of BnB memory model for predicate analysis, which efficiently divides the accessed memory into memory regions and thus leads to smaller formulas.
   BibTeX Entry

   @inproceedings{CPABAM-COMP17, author = {Pavel Andrianov and Karlheinz Friedberger and Mikhail U. Mandrykin and Vadim S. Mutilin and Anton Volkov}, title = {{CPA-BAM-BnB}: {Block}-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)}, booktitle = {Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2017, Uppsala, Sweden, April 22-29)}, editor = {Axel Legay and Tiziana Margaria}, pages = {355--359}, year = {2017}, series = {LNCS~10206}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-54579-9}, doi = {10.1007/978-3-662-54580-5_22}, sha256 = {}, url = {https://doi.org/10.1007/978-3-662-54580-5_22}, abstract = {Our submission to SV-COMP'17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the version of SV-COMP'16. A novelty of our approach is usage of BnB memory model for predicate analysis, which efficiently divides the accessed memory into memory regions and thus leads to smaller formulas.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, }
8. Dirk Beyer and Karlheinz Friedberger. A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker. In J. Bouda, L. Holík, J. Kofroň, J. Strejček, and A. Rambousek, editors, Proceedings of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016, Telč, Czechia, October 21-23), EPTCS 233, pages 61-71, 2016. ArXiV. doi:10.4204/EPTCS.233.6 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{MEMICS16-Multi-Threaded, author = {Dirk Beyer and Karlheinz Friedberger}, title = {A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker}, booktitle = {Proceedings of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS~2016, Tel\v{c}, Czechia, October 21-23)}, editor = {J.~Bouda and L.~Hol\'ik and J.~Kofro\v{n} and J.~Strej\v{c}ek and A.~Rambousek}, pages = {61-71}, year = {2016}, series = {EPTCS~233}, publisher = {ArXiV}, doi = {10.4204/EPTCS.233.6}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2016-MEMICS.A_Light-Weight_Approach_for_Verifying_Multi-Threaded_Programs_with_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, }
9. Egor George Karpenkov, Karlheinz Friedberger, and Dirk Beyer. JavaSMT: A Unified Interface for SMT Solvers in Java. In Proc. VSTTE, LNCS 9971, pages 139-148, 2016. Springer. doi:10.1007/978-3-319-48869-1_11 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{VSTTE16a-JavaSMT, author = {Egor George Karpenkov and Karlheinz Friedberger and Dirk Beyer}, title = {{{\sc JavaSMT}}: {A} Unified Interface for {SMT} Solvers in {Java}}, booktitle = {Proc.\ VSTTE}, pages = {139--148}, year = {2016}, series = {LNCS~9971}, publisher = {Springer}, doi = {10.1007/978-3-319-48869-1_11}, sha256 = {}, url = {https://github.com/sosy-lab/java-smt/}, pdf = {https://www.sosy-lab.org/research/pub/2016-VSTTE.JavaSMT_A_Unified_Interface_For_SMT_Solvers_in_Java.pdf}, }
10. Karlheinz Friedberger. CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution). In Marsha Chechik and Jean-François Raskin, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016, Eindhoven, The Netherlands, April 2-8), LNCS 9636, pages 912-915, 2016. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-49674-9_58 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{CPABAM-COMP16, author = {Karlheinz Friedberger}, title = {{CPA-BAM}: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution)}, booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2016, Eindhoven, The Netherlands, April 2-8)}, editor = {Marsha Chechik and Jean{-}Fran{\c{c}}ois Raskin}, pages = {912--915}, year = {2016}, series = {LNCS~9636}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-49673-2}, doi = {10.1007/978-3-662-49674-9_58}, sha256 = {}, url = {https://doi.org/10.1007/978-3-662-49674-9_58}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, }
11. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Abstract-Domain Selection Based on Variable Usage. In V. Bertacco and A. Legay, editors, Proceedings of the 9th Haifa Verification Conference (HVC 2013, Haifa, Israel, November 5-7), LNCS 8244, pages 262-278, 2013. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-03077-7_18 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., 'int' and 'long') to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.
    BibTeX Entry

    @inproceedings{HVC13, author = {Sven Apel and Dirk Beyer and Karlheinz Friedberger and Franco Raimondi and Alexander von Rhein}, title = {Domain Types: Abstract-Domain Selection Based on Variable Usage}, booktitle = {Proceedings of the 9th Haifa Verification Conference (HVC 2013, Haifa, Israel, November 5-7)}, editor = {V.~Bertacco and A.~Legay}, pages = {262-278}, year = {2013}, series = {LNCS~8244}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-03076-0}, doi = {10.1007/978-3-319-03077-7_18}, url = {https://www.sosy-lab.org/research/domaintypes/}, pdf = {https://www.sosy-lab.org/research/pub/2013-HVC.Domain_Types_Abstract-Domain_Selection_Based_on_Variable_Usage.pdf}, abstract = {The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., `int' and `long') to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.}, keyword = {CPAchecker,Software Model Checking}, }

12. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Selecting Abstractions Based on Variable Usage. Technical report MIP-1303, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. doi:10.48550/arXiv.1305.6640 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.
    BibTeX Entry

    @techreport{TR1303-PA13, author = {Sven Apel and Dirk Beyer and Karlheinz Friedberger and Franco Raimondi and Alexander von Rhein}, title = {Domain Types: Selecting Abstractions Based on Variable Usage}, number = {MIP-1303}, year = {2013}, doi = {10.48550/arXiv.1305.6640}, url = {https://www.sosy-lab.org/research/domaintypes/}, abstract = {The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.}, keyword = {CPAchecker,Software Model Checking}, annote = {}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {May}, }

13. Karlheinz Friedberger. Efficient Software Model Checking with Block-Abstraction Memoization. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.29976 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    BibTeX Entry

    @misc{FriedbergerBAM, author = {Karlheinz Friedberger}, title = {Efficient Software Model Checking with Block-Abstraction Memoization}, year = {2022}, doi = {10.5282/edoc.29976}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/29976/1/Friedberger_Karlheinz.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at MSG Systems, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-296471}, }
    Additional Infos

    Now at MSG Systems, Munich, Germany
14. Karlheinz Friedberger. Block-Abstraction Memoization as an Approach to Verify Recursive Procedures. Master's Thesis, University of Passau, Software Systems Lab, 2015. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{KarlheinzBAMRecursion, author = {Karlheinz Friedberger}, title = {Block-Abstraction Memoization as an Approach to Verify Recursive Procedures}, year = {2015}, pdf = {https://www.sosy-lab.org/research/msc/2015.Friedberger.Block-Abstraction_Memoization_as_an_Approach_to_Verify_Recursive_Procedures.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
15. Karlheinz Friedberger. Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{KarlheinzDomainTypes, author = {Karlheinz Friedberger}, title = {{Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken}}, year = {2012}, pdf = {https://www.sosy-lab.org/research/bsc/2012.Friedberger.Ein_typbasierter_Ansatz_zur_Kombination_verschiedener_Verifikationstechniken.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
    Additional Infos

    Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis