Publications of year 2018

(All PublicationsIndex)

Books and proceedings

  1. Dirk Beyer and Marieke Huisman, editors.
    Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 1, LNCS 10805, 2018.
    Springer.
    [ Material ] [ Article ]
    @Proceedings{TACAS18a,
    editor = {Dirk Beyer and Marieke Huisman},
    title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 1},
    publisher = {Springer},
    series = {LNCS~10805},
    year = {2018},
    isbn = {978-3-319-89959-6},
    doi = {10.1007/978-3-319-89960-2},
    pdf = {https://doi.org/10.1007/978-3-319-89960-2},
    url = {https://www.etaps.org/index.php/2018/tacas},
    
    }
    

  2. Dirk Beyer and Marieke Huisman, editors.
    Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 2, LNCS 10806, 2018.
    Springer.
    [ Material ] [ Article ]
    @Proceedings{TACAS18b,
    editor = {Dirk Beyer and Marieke Huisman},
    title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 2},
    publisher = {Springer},
    series = {LNCS~10806},
    year = {2018},
    isbn = {978-3-319-89962-6},
    doi = {10.1007/978-3-319-89963-3},
    pdf = {https://doi.org/10.1007/978-3-319-89963-3},
    url = {https://www.etaps.org/index.php/2018/tacas},
    
    }
    

Articles in journal or book chapters

  1. Dirk Beyer, Sumit Gulwani, and David Schmidt.
    Combining Model Checking and Data-Flow Analysis.
    In E. M. Clarke, T. A. Henzinger, and H. Veith, editors, Handbook on Model Checking, pages 493-540.
    Springer, 2018.
    [ Article ]
    @InCollection{HBMC18,
    author = {Dirk Beyer and Sumit Gulwani and David Schmidt},
    title = {Combining Model Checking and Data-Flow Analysis},
    booktitle = {Handbook on Model Checking},
    editor = {E.~M.~Clarke and T.~A.~Henzinger and H.~Veith},
    publisher = {Springer},
    pages = {493-540},
    year = {2018},
    doi = {10.1007/978-3-319-10575-8_16},
    isbn = {978-3-319-10574-1},
    pdf = {https://www.sosy-lab.org/research/pub/2018-HBMC.Combining_Model_Checking_and_Data-Flow_Analysis.pdf},
    
    }
    

  2. Dirk Beyer, Matthias Dangl, and Philipp Wendler.
    A Unifying View on SMT-Based Software Verification.
    Journal of Automated Reasoning, 60(3):299--335, 2018.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different ``schools of thought'' of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.

    @Article{AlgorithmComparison-JAR,
    author = {Dirk Beyer and Matthias Dangl and Philipp Wendler},
    title = {A Unifying View on {SMT}-Based Software Verification},
    journal = {Journal of Automated Reasoning},
    year = {2018},
    volume = {60},
    number = {3},
    pages = {299--335},
    issn = {1573-0670},
    doi = {10.1007/s10817-017-9432-6},
    pdf = {https://www.sosy-lab.org/research/pub/2018-JAR.A_Unifying_View_on_SMT-Based_Software_Verification.pdf},
    url = {https://www.sosy-lab.org/research/k-ind-compare/},
    abstract = {After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different ``schools of thought'' of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions. },
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

Articles in conference or workshop proceedings

  1. Dirk Beyer and Matthias Dangl.
    Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach.
    In T. Margaria and B. Steffen, editors, 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2018, Part 2, Limassol, Cyprus, November 5-9), LNCS 11245, pages 144-159, 2018.
    Springer.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.

    @inproceedings{ISoLA18a,
    author = {Dirk Beyer and Matthias Dangl},
    title = {Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach},
    booktitle = {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},
    publisher = {Springer},
    series = {LNCS~11245},
    pages = {144-159},
    year = {2018},
    doi = {10.1007/978-3-030-03421-4_11},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ISoLA.Strategy_Selection_for_Software_Verification_Based_on_Boolean_Features.pdf},
    postscript= {https://www.sosy-lab.org/research/prs/2018-11-05_ISoLA18_StrategySelection_Dirk.pdf},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  2. Dirk Beyer, Matthias Dangl, Thomas Lemberger, and Michael Tautschnig.
    Tests from Witnesses: Execution-Based Validation of Verification Results.
    In Catherine Dubois and Burkhart Wolff, editors, Proceedings of the 12th International Conference on Tests and Proofs (TAP 2018, Toulouse, France, June 27-29), pages 3-23, 2018.
    Springer.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    The research community made enormous progress in the past years in developing algorithms for verifying software, as shown by verification competitions (SV-COMP). However, the ultimate goal is to design certifying algorithms, which produce for a given input not only the output but in addition a witness. This makes it possible to validate that the output is a correct solution for the input problem. The advantage of certifying algorithms is that the validation of the result is —thanks to the witness— easier than the computation of the result. Unfortunately, the transfer to industry is slow, one of the reasons being that some verifiers report a considerable number of false alarms. The verification community works towards this ultimate goal using exchangeable violation witnesses, i.e., an independent validator can be used to check whether the produced witness indeed represents a bug. This reduces the required trust base from the complex verification tool to a validator that may be less complex, and thus, more easily trustable. But existing witness validators are based on model-checking technology — which does not solve the problem of reducing the trust base. To close this gap, we present a simple concept that is based on program execution: We extend witness validation by generating a test vector from an error path that is reconstructed from the witness. Then, we generate a test harness (similar to unit-test code) that can be compiled and linked together with the original program. We then run the executable program in an isolating container. If the execution violates the specification (similar to runtime verification) we confirm that the witness indeed represents a bug. This method reduces the trust base to the execution system, which seems appropriate for avoiding false alarms. To show feasibility and practicality, we implemented execution-based witness validation in two completely independent analysis frameworks, and performed a large experimental study.

    @InProceedings{TAP18,
    author = {Dirk Beyer and Matthias Dangl and Thomas Lemberger and Michael Tautschnig},
    title = {Tests from Witnesses: Execution-Based Validation of Verification Results},
    booktitle = {Proceedings of the 12th International Conference on Tests and Proofs (TAP~2018, Toulouse, France, June 27-29)},
    editor = {Catherine Dubois and Burkhart Wolff},
    publisher = {Springer},
    pages = {3-23},
    year = {2018},
    doi = {10.1007/978-3-319-92994-1_1},
    pdf = {https://www.sosy-lab.org/research/pub/2018-TAP.Tests_from_Witnesses_Execution-Based_Validation_of_Verification_Results.pdf},
    url = {https://www.sosy-lab.org/research/tests-from-witnesses/},
    postscript= {https://www.sosy-lab.org/research/prs/2018-06-27_TAP18-Keynote-CooperativeVerification_Dirk.pdf},
    keyword = {CPAchecker,Software Model Checking},
    abstract = { The research community made enormous progress in the past years in developing algorithms for verifying software, as shown by verification competitions (SV-COMP). However, the ultimate goal is to design certifying algorithms, which produce for a given input not only the output but in addition a witness. This makes it possible to validate that the output is a correct solution for the input problem. The advantage of certifying algorithms is that the validation of the result is —thanks to the witness— easier than the computation of the result. Unfortunately, the transfer to industry is slow, one of the reasons being that some verifiers report a considerable number of false alarms. The verification community works towards this ultimate goal using exchangeable violation witnesses, i.e., an independent validator can be used to check whether the produced witness indeed represents a bug. This reduces the required trust base from the complex verification tool to a validator that may be less complex, and thus, more easily trustable. But existing witness validators are based on model-checking technology — which does not solve the problem of reducing the trust base. To close this gap, we present a simple concept that is based on program execution: We extend witness validation by generating a test vector from an error path that is reconstructed from the witness. Then, we generate a test harness (similar to unit-test code) that can be compiled and linked together with the original program. We then run the executable program in an isolating container. If the execution violates the specification (similar to runtime verification) we confirm that the witness indeed represents a bug. This method reduces the trust base to the execution system, which seems appropriate for avoiding false alarms. To show feasibility and practicality, we implemented execution-based witness validation in two completely independent analysis frameworks, and performed a large experimental study. },
    
    }
    

  3. 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.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.
    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.

    @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},
    publisher = {ACM},
    pages = {634-644},
    year = {2018},
    doi = {10.1145/3238147.3238195},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ASE.Domain-Independent_Multi-threaded_Software_Model_Checking.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2018-09-07_ASE18_ParallelBAM_Karlheinz.pdf},
    keyword = {CPAchecker,Software Model Checking},
    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. },
    
    }
    

  4. 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, 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.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.
    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.

    @inproceedings{ISoLA18b,
    author = {Dirk Beyer and Karlheinz Friedberger},
    title = {In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching},
    booktitle = {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},
    publisher = {Springer},
    series = {LNCS~11245},
    pages = {197-215},
    year = {2018},
    doi = {10.1007/978-3-030-03421-4_14},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ISoLA.In-Place_vs_Copy-on-Write_CEGAR_Refinement_for_Block_Summarization_with_Caching.pdf},
    postscript= {https://www.sosy-lab.org/research/prs/2018-11-06_ISoLA18_BAM-CoW-Refinement_Dirk.pdf},
    url = {https://www.sosy-lab.org/research/bam-cow-refinement/},
    keyword = {CPAchecker,Software Model Checking},
    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. },
    
    }
    

  5. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim.
    Reducer-Based Construction of Conditional Verifiers.
    In Proceedings of the 40th International Conference on Software Engineering (ICSE 2018, Gothenburg, Sweden, May 27 - June 3), pages 1182-1193, 2018.
    ACM.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.

    @InProceedings{ICSE18,
    author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim},
    title = {Reducer-Based Construction of Conditional Verifiers},
    booktitle = {Proceedings of the 40th International Conference on Software Engineering (ICSE~2018, Gothenburg, Sweden, May 27 - June 3)},
    publisher = {ACM},
    pages = {1182-1193},
    year = {2018},
    isbn = {978-1-4503-5638-1},
    doi = {10.1145/3180155.3180259},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ICSE.Reducer-Based_Construction_of_Conditional_Verifiers.pdf},
    url = {https://www.sosy-lab.org/research/reducer/},
    keyword = {CPAchecker,Software Model Checking},
    abstract = { Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication. },
    
    }
    

  6. Dirk Beyer and Thomas Lemberger.
    CPA-SymExec: Efficient Symbolic Execution in CPAchecker.
    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 900-903, 2018.
    ACM.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at https://cpachecker.sosy-lab.org. A demonstration video is available at https://youtu.be/qoBHtvPKtnw.

    @inproceedings{ASE18b,
    author = {Dirk Beyer and Thomas Lemberger},
    title = {{CPA-SymExec}: Efficient Symbolic Execution in {CPAchecker}},
    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},
    publisher = {ACM},
    pages = {900-903},
    year = {2018},
    doi = {10.1145/3238147.3240478},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ASE.CPA-SymExec_Efficient_Symbolic_Execution_in_CPAchecker.pdf},
    keyword = {CPAchecker,Software Model Checking},
    url = {https://www.sosy-lab.org/research/cpa-symexec-tool/},
    abstract = { We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at https://cpachecker.sosy-lab.org. A demonstration video is available at https://youtu.be/qoBHtvPKtnw. },
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Moritz Buhl.
    Application of Software Verification to OpenBSD Network Modules.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): CPAchecker, Software Model Checking.

    @misc{BuhlOpenBSD,
    author = {Moritz Buhl},
    title = {Application of Software Verification to {O}pen{BSD} Network Modules},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking} 
    }
    

  2. Dominik Friedrich.
    Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): CPAchecker.

    @misc{FriedrichStatistics,
    author = {Dominik Friedrich},
    title = {Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {CPAchecker} 
    }
    

  3. Johannes Knaut.
    Symbolic Heap Abstraction with Automatic Refinement.
    Master's Thesis, LMU Munich, Software Systems Lab, 2018.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{MartinSplitting,
    author = {Johannes Knaut},
    title = {Symbolic Heap Abstraction with Automatic Refinement},
    howpublished = {Master's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/msc/2018.Knaut.Symbolic_Heap_Abstraction_with_Automatic_Refinement.pdf},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  4. Thomas Lemberger.
    Abstraction Refinement for Model Checking: Program Slicing + CEGAR.
    Master's Thesis, LMU Munich, Software Systems Lab, 2018.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{ThomasSlicing,
    author = {Thomas Lemberger},
    title = {Abstraction Refinement for Model Checking: Program Slicing + CEGAR},
    howpublished = {Master's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/msc/2018.Lemberger.Abstraction_Refinement_for_Model_Checking_Program_Slicing_and_Cegar.pdf},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  5. Dominik Pastau.
    Implementation of a Generic Cloud-Based File-Storage Solution and its Integration into a Web-Based Distributed Verification System.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): Cloud-Based Software Verification.

    @misc{PastauWitnessStore,
    author = {Dominik Pastau},
    title = {Implementation of a Generic Cloud-Based File-Storage Solution and its Integration into a Web-Based Distributed Verification System},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {Cloud-Based Software Verification} 
    }
    

  6. Nicholas Reyes.
    Integrating a Witness Store into a Distributed Verification System.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): Witness Validation, Cloud-Based Software Verification.

    @misc{ReyesWitnessStore,
    author = {Nicholas Reyes},
    title = {Integrating a Witness Store into a Distributed Verification System},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {Witness Validation,Cloud-Based Software Verification} 
    }
    

  7. Karam Shabita.
    String Analysis for Java Programs in CPAchecker.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): CPAchecker, Software Model Checking.

    @misc{SharamStrings,
    author = {Karam Shabita},
    title = {String Analysis for Java Programs in {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  8. Martin Spiessl.
    Configurable Software Verification based on Slicing Abstractions.
    Master's Thesis, LMU Munich, Software Systems Lab, 2018.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{MartinSplitting,
    author = {Martin Spiessl},
    title = {Configurable Software Verification based on Slicing Abstractions},
    howpublished = {Master's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/msc/2018.Spiessl.Configurable_Software_Verification_based_on_Slicing_Abstractions.pdf},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

(All PublicationsIndex)



Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.




Last modified: Mon Dec 10 02:12:10 2018


This document was translated from BibTEX by bibtex2html