We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
2 papers accepted at ASE 2024: BenchCloud and CoVeriTeam GUI

Publications of year 2018

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 2. LNCS 10806, 2018. Springer. doi:10.1007/978-3-319-89963-3 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TACAS18b, title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 2}, editor = {Dirk Beyer and Marieke Huisman}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, isbn = {978-3-319-89962-6}, doi = {10.1007/978-3-319-89963-3}, sha256 = {}, url = {https://www.etaps.org/index.php/2018/tacas}, pdf = {https://doi.org/10.1007/978-3-319-89963-3}, }
  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 1. LNCS 10805, 2018. Springer. doi:10.1007/978-3-319-89960-2 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TACAS18a, title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 1}, editor = {Dirk Beyer and Marieke Huisman}, year = {2018}, series = {LNCS~10805}, publisher = {Springer}, isbn = {978-3-319-89959-6}, doi = {10.1007/978-3-319-89960-2}, sha256 = {}, url = {https://www.etaps.org/index.php/2018/tacas}, pdf = {https://doi.org/10.1007/978-3-319-89960-2}, }

Articles in journal or book chapters
  1. Dirk Beyer, Matthias Dangl, and Philipp Wendler. A Unifying View on SMT-Based Software Verification. Journal of Automated Reasoning, 60(3):299-335, 2018. doi:10.1007/s10817-017-9432-6 Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    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.
    BibTeX Entry
    @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}, volume = {60}, number = {3}, pages = {299--335}, year = {2018}, doi = {10.1007/s10817-017-9432-6}, sha256 = {5fab3eafacd7fef9c655afc9cd78bbb419ea47361a81633fb551fbf496875d84}, url = {https://www.sosy-lab.org/research/k-ind-compare/}, presentation = {https://www.sosy-lab.org/research/prs/Latest_UnifyingViewSmtBasedSoftwareVerification.pdf}, 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}, _pdf = {https://www.sosy-lab.org/research/pub/2018-JAR.A_Unifying_View_on_SMT-Based_Software_Verification.pdf}, annote = {Publication appeared first online in December 2017<BR/> CPAchecker is available at: <a href="https://cpachecker.sosy-lab.org/"> https://cpachecker.sosy-lab.org/</a>}, issn = {1573-0670}, }
    Additional Infos
    Publication appeared first online in December 2017
    CPAchecker is available at: https://cpachecker.sosy-lab.org/
  2. Yuyan Bao, Gary Leavens, and Gidon Ernst. Unifying separation logic and region logic to allow interoperability. Formal Aspects of Computing, 30(3--4):381-441, 2018. Springer. Link to this entry
    BibTeX Entry
    @article{ernst:bao2018, author = {Yuyan Bao and Gary Leavens and Gidon Ernst}, title = {Unifying separation logic and region logic to allow interoperability}, journal = {Formal Aspects of Computing}, volume = {30}, number = {3--4}, pages = {381--441}, year = {2018}, publisher = {Springer}, }
  3. Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, and Ichiro Hasuo. Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 37(11):2894-2905, 2018. IEEE. Link to this entry Nominated for best paper PDF
    BibTeX Entry
    @article{ernst:emsoft2018, author = {Zhenya Zhang and Gidon Ernst and Sean Sedwards and Paolo Arcaini and Ichiro Hasuo}, title = {{Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search}}, journal = {Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)}, volume = {37}, number = {11}, pages = {2894--2905}, year = {2018}, publisher = {IEEE}, pdf = {https://www.sosy-lab.org/research/pub/2018-TCAD.Two-Layered_Falsification_of_Hybrid_Systems_guided_by_Monte_Carlo_Tree_Search.pdf}, note = {Nominated for best paper}, }
  4. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, and Wolfgang Reif. Symbolic execution for a clash-free subset of ASMs. Science of Computer Programming (SCP), 158:21-40, 2018. Elsevier. Link to this entry PDF
    BibTeX Entry
    @article{ernst:scp2017, author = {Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Stefan Bodenmüller and Wolfgang Reif}, title = {{Symbolic execution for a clash-free subset of ASMs}}, journal = {Science of Computer Programming (SCP)}, volume = {158}, pages = {21--40}, year = {2018}, publisher = {Elsevier}, pdf = {https://www.sosy-lab.org/research/pub/2017-SCP.Symbolic_Execution_for_a_Clash-Free_Subset_of_ASMs.pdf}, }
  5. Dirk Beyer, Sumit Gulwani, and David Schmidt. Combining Model Checking and Data-Flow Analysis. In E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors, Handbook on Model Checking, pages 493-540, 2018. Springer. doi:10.1007/978-3-319-10575-8_16 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @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 and R.~Bloem}, pages = {493-540}, year = {2018}, publisher = {Springer}, isbn = {978-3-319-10574-1}, doi = {10.1007/978-3-319-10575-8_16}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2018-HBMC.Combining_Model_Checking_and_Data-Flow_Analysis.pdf}, annote = {<a href="https://www.sosy-lab.org/research/pub/2018-HBMC.Combining_Model_Checking_and_Data-Flow_Analysis.Errata.txt"> Errata</a> available.}, }
    Additional Infos
    Errata available.
  6. Marie-Christine Jakobs. Spontane Sicherheitsprüfung mittels individualisierter Programmzertifizierung oder Programmrestrukturierung. In S. Hölldobler, editors, Ausgezeichnete Informatikdissertationen 2017, LNI, pages 91-100, 2018. Gesellschaft für Informatik (GI). Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    Abstract
    Korrekt funktionierende Software gewinnt immer mehr an Bedeutung. Im Vergleich zu früher ist es heutzutage schwieriger einzuschätzen, wie gut eine Software funktioniert. Dies liegt unter anderem daran, dass Endnutzer häufiger Software unbekannter Hersteller installieren. Endnutzer sollten sich also aktiv von der Softwarekorrektheit überzeugen, zum Beispiel in Form einer spontanen Sicherheitsprüfung. Übliche Verifikationstechniken zur Korrektheitsprüfung kommen für Endnutzer, in der Regel Laien, nicht in Frage. Die zentrale Frage ist daher, wie man einem Laien eine solche spontane Sicherheitsprüfung ermöglicht. Die Antwort der Dissertation sind einfache, automatische und generelle Verfahren zur Sicherheitsprüfung. In der Dissertation werden verschiedene Verfahren vorgeschlagen und sowohl theoretisch als auch praktisch untersucht. Die vorgeschlagenen Verfahren lassen sich in zwei Forschungsrichtungen einsortieren, nämlich in die Gruppe der Proof-Carrying Code Verfahren bzw. in die Gruppe des alternativen Programs from Proofs Verfahren. Einige Verfahren kombinieren beide Forschungsrichtungen.
    BibTeX Entry
    @incollection{DissZusammenfassungJakobs, author = {Marie-Christine Jakobs}, title = {Spontane Sicherheitspr{\"{u}}fung mittels individualisierter Programmzertifizierung oder Programmrestrukturierung}, booktitle = {Ausgezeichnete Informatikdissertationen 2017}, editor = {S. H{\"{o}}lldobler}, volume = {{D-18}}, pages = {91-100}, year = {2018}, series = {{LNI}}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, isbn = {978-3885799771}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19486/invited_paper_14.pdf?sequence=1&isAllowed=y}, abstract = {Korrekt funktionierende Software gewinnt immer mehr an Bedeutung. Im Vergleich zu fr&uuml;her ist es heutzutage schwieriger einzusch&auml;tzen, wie gut eine Software funktioniert. Dies liegt unter anderem daran, dass Endnutzer h&auml;ufiger Software unbekannter Hersteller installieren. Endnutzer sollten sich also aktiv von der Softwarekorrektheit &uuml;berzeugen, zum Beispiel in Form einer spontanen Sicherheitspr&uuml;fung. &Uuml;bliche Verifikationstechniken zur Korrektheitspr&uuml;fung kommen f&uuml;r Endnutzer, in der Regel Laien, nicht in Frage. Die zentrale Frage ist daher, wie man einem Laien eine solche spontane Sicherheitspr&uuml;fung erm&ouml;glicht. Die Antwort der Dissertation sind einfache, automatische und generelle Verfahren zur Sicherheitspr&uuml;fung. In der Dissertation werden verschiedene Verfahren vorgeschlagen und sowohl theoretisch als auch praktisch untersucht. Die vorgeschlagenen Verfahren lassen sich in zwei Forschungsrichtungen einsortieren, n&auml;mlich in die Gruppe der Proof-Carrying Code Verfahren bzw. in die Gruppe des alternativen Programs from Proofs Verfahren. Einige Verfahren kombinieren beide Forschungsrichtungen.}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.}, doifalse = {20.500.12116/19486}, urlpub = {https://dl.gi.de/handle/20.500.12116/19486}, }
    Additional Infos
    This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.
  7. Philipp Wendler. Beiträge zu praktikabler Prädikatenanalyse. In S. Hölldobler, editors, Ausgezeichnete Informatikdissertationen 2017, LNI, pages 261-270, 2018. Gesellschaft für Informatik (GI). Link to this entry Keyword(s): Benchmarking, CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    Abstract
    Der Stand der Forschung im Bereich der automatischen Software-Verifikation ist fragmentiert. Verschiedene Verfahren existieren nebeneinander in unterschiedlichen Darstellungen und mit wenig Bezug zueinander, aussagekräftige Vergleiche sind selten. Die Dissertation adressiert dieses Problem. Ein konfigurierbares und flexibles Rahmenwerk zur Vereinheitlichung solcher Verfahren wird entwickelt und mehrere vorhandene Verfahren werden in diesem Rahmenwerk ausgedrückt. Dies bringt neue Erkenntnisse über die Kernideen dieser Verfahren, ermöglicht experimentelle Studien in einer neuartigen Qualität, und erleichtert die Forschung an Kombinationen und Weiterentwicklungen dieser Verfahren. Die Implementierung dieses Rahmenwerks im erfolgreichen Verifizierer CPAchecker wird in der bisher größten derartigen experimentellen Studie (120 verschiedene Konfigurationen, 671280 Ausführungen) evaluiert. Hierzu wird ein Benchmarking-System präsentiert, das mit Hilfe moderner Technologien signifikante qualitative Messfehler existierender Systeme vermeidet.
    BibTeX Entry
    @incollection{DissZusammenfassungWendler, author = {Philipp Wendler}, title = {Beitr{\"{a}}ge zu praktikabler Pr{\"{a}}dikatenanalyse}, booktitle = {Ausgezeichnete Informatikdissertationen 2017}, editor = {S. H{\"{o}}lldobler}, volume = {{D-18}}, pages = {261-270}, year = {2018}, series = {{LNI}}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, isbn = {978-3885799771}, url = {https://www.sosy-lab.org/research/phd/wendler/}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19476/invited_paper_4.pdf?sequence=1&isAllowed=y}, presentation = {https://www.sosy-lab.org/research/prs/2018-05-08_GiDiss_BeitraegeZuPraktikablerPraedikatenanalyse.pdf}, abstract = {Der Stand der Forschung im Bereich der automatischen Software-Verifikation ist fragmentiert. Verschiedene Verfahren existieren nebeneinander in unterschiedlichen Darstellungen und mit wenig Bezug zueinander, aussagekr&auml;ftige Vergleiche sind selten. Die Dissertation adressiert dieses Problem. Ein konfigurierbares und flexibles Rahmenwerk zur Vereinheitlichung solcher Verfahren wird entwickelt und mehrere vorhandene Verfahren werden in diesem Rahmenwerk ausgedr&uuml;ckt. Dies bringt neue Erkenntnisse &uuml;ber die Kernideen dieser Verfahren, erm&ouml;glicht experimentelle Studien in einer neuartigen Qualit&auml;t, und erleichtert die Forschung an Kombinationen und Weiterentwicklungen dieser Verfahren. Die Implementierung dieses Rahmenwerks im erfolgreichen Verifizierer CPAchecker wird in der bisher gr&ouml;&szlig;ten derartigen experimentellen Studie (120 verschiedene Konfigurationen, 671280 Ausf&uuml;hrungen) evaluiert. Hierzu wird ein Benchmarking-System pr&auml;sentiert, das mit Hilfe moderner Technologien signifikante qualitative Messfehler existierender Systeme vermeidet.}, keyword = {Benchmarking,CPAchecker,Software Model Checking}, annote = {This is a German summary of the dissertation <a href="https://www.sosy-lab.org/research/bib/Year/2017.complete.html#PhilippPredicateAnalysis">Towards Practical Predicate Analysis</a>.}, doifalse = {20.500.12116/19476}, urlpub = {https://dl.gi.de/handle/20.500.12116/19476}, }
    Additional Infos
    This is a German summary of the dissertation Towards Practical Predicate Analysis.

Articles in conference or workshop proceedings
  1. 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 Link to this entry 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}, }
  2. 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, 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 144-159, 2018. Springer. doi:10.1007/978-3-030-03421-4_11 Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation
    BibTeX Entry
    @inproceedings{ISoLA18a, author = {Dirk Beyer and Matthias Dangl}, title = {Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach}, 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 = {144-159}, year = {2018}, series = {LNCS~11245}, publisher = {Springer}, doi = {10.1007/978-3-030-03421-4_11}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2018-ISoLA.Strategy_Selection_for_Software_Verification_Based_on_Boolean_Features.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-11-05_ISoLA18_StrategySelection_Dirk.pdf}, keyword = {CPAchecker,Software Model Checking}, }
  3. 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), pages 900-903, 2018. ACM. doi:10.1145/3238147.3240478 Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Video Supplement
    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.
    BibTeX Entry
    @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)}, editor = {Marianne Huchard and Christian K{\"{a}}stner and Gordon Fraser}, pages = {900-903}, year = {2018}, publisher = {ACM}, doi = {10.1145/3238147.3240478}, sha256 = {}, url = {https://www.sosy-lab.org/research/cpa-symexec-tool/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ASE.CPA-SymExec_Efficient_Symbolic_Execution_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-09-07_ASE18_CPASymExec_Thomas.pdf}, 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.}, keyword = {CPAchecker,Software Model Checking}, video = {https://youtu.be/7o7EtpbV8NM}, }
  4. 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 Link to this entry 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}, }
  5. 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), LNCS 10889, pages 3-23, 2018. Springer. doi:10.1007/978-3-319-92994-1_1 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF Presentation Supplement
    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.
    BibTeX Entry
    @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}, pages = {3-23}, year = {2018}, series = {LNCS~10889}, publisher = {Springer}, doi = {10.1007/978-3-319-92994-1_1}, sha256 = {}, url = {https://www.sosy-lab.org/research/tests-from-witnesses/}, pdf = {https://www.sosy-lab.org/research/pub/2018-TAP.Tests_from_Witnesses_Execution-Based_Validation_of_Verification_Results.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-06-27_TAP18-Keynote-CooperativeVerification_Dirk.pdf}, 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.}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
  6. 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. doi:10.1145/3180155.3180259 Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    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.
    BibTeX Entry
    @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)}, pages = {1182-1193}, year = {2018}, publisher = {ACM}, isbn = {978-1-4503-5638-1}, doi = {10.1145/3180155.3180259}, sha256 = {}, url = {https://www.sosy-lab.org/research/reducer/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ICSE.Reducer-Based_Construction_of_Conditional_Verifiers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-06-01_ICSE18_ReducerBasedConstructionOfConditionalVerifiers_Marie.pdf}, 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.}, keyword = {CPAchecker,Software Model Checking}, }
  7. Markus Schordan, Dirk Beyer, and Stephen F. Siegel. Evaluating Tools for Software Verification (Track Introduction). In T. Margaria and B. Steffen, editors, Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2018, Limassol, Cyprus, November 5-9), Part 2, LNCS 11245, pages 139-143, 2018. Springer-Verlag, Heidelberg. doi:10.1007/978-3-030-03421-4_10 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ISOLA18-TrackIntro, author = {Markus Schordan and Dirk Beyer and Stephen F. Siegel}, title = {Evaluating Tools for Software Verification (Track Introduction)}, booktitle = {Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2018, Limassol, Cyprus, November 5--9), Part 2}, editor = {T.~Margaria and B.~Steffen}, pages = {139-143}, year = {2018}, series = {LNCS~11245}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-030-03420-7}, doi = {10.1007/978-3-030-03421-4_10}, sha256 = {}, url = {}, keyword = {}, }
  8. Abdullah Issa, Toby Murray, and Gidon Ernst. In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces. In Proc. of Computer Human Interaction Australia (OzCHI), pages 572-576, 2018. ACM. Link to this entry Work in Progress Report. PDF
    BibTeX Entry
    @inproceedings{ernst:ozchi2018, author = {Abdullah Issa and Toby Murray and Gidon Ernst}, title = {{In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces}}, booktitle = {Proc. of Computer Human Interaction Australia (OzCHI)}, pages = {572--576}, year = {2018}, publisher = {ACM}, pdf = {https://www.sosy-lab.org/research/pub/2018-OzCHI.In_Search_of_Perfect_Users.pdf}, note = {Work in Progress Report.}, }
  9. Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, and Sean Sedwards. ARCH-COMP18 Category Report: Results on the Falsification Benchmarks. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 104-109, 2018. EasyChair. Link to this entry PDF
    BibTeX Entry
    @inproceedings{ernst:arch2018, author = {Adel Dokhanchi and Shakiba Yaghoubi and Bardh Hoxha and Georgios Fainekos and Gidon Ernst and Zhenya Zhang and Paolo Arcaini and Ichiro Hasuo and Sean Sedwards}, title = {{ARCH-COMP18 Category Report: Results on the Falsification Benchmarks}}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {54}, pages = {104--109}, year = {2018}, series = {EPiC}, publisher = {EasyChair}, pdf = {https://www.sosy-lab.org/research/pub/2018-ARCH.Results_on_the_Falsification_Benchmarks.pdf}, }
  10. Zhenya Zhang, Gidon Ernst, Ichiro Hasuo, and Sean Sedwards. Time-staging Enhancement of Hybrid System Falsification (Abstract). In Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS), 2018. IEEE. Link to this entry
    BibTeX Entry
    @inproceedings{ernst:mt-cps2018, author = {Zhenya Zhang and Gidon Ernst and Ichiro Hasuo and Sean Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification (Abstract)}}, booktitle = {Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS)}, year = {2018}, publisher = {IEEE}, }

Internal reports
  1. Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and Gidon Ernst. VerifyThis 2018: A Program Verification Competition. Technical report hal-01981937, Université Paris-Saclay, 2018. Link to this entry PDF Supplement
    BibTeX Entry
    @techreport{ernst:verifythis2018, author = {Marieke Huisman and Rosemary Monahan and Peter Müller and Andrei Paskevich and Gidon Ernst}, title = {{VerifyThis 2018: A Program Verification Competition}}, number = {hal-01981937}, year = {2018}, url = {https://hal.inria.fr/hal-01981937}, pdf = {https://www.sosy-lab.org/research/pub/2018-HAL.VerifyThis_2018.pdf}, institution = {Universit{\'e} Paris-Saclay}, }

Theses and projects (PhD, MSc, BSc, Project)
  1. Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, and Sean Sedwards. Time-staging Enhancement of Hybrid System Falsification. 2018. Link to this entry Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021. PDF
    BibTeX Entry
    @misc{ernst:snr2018, author = {Gidon Ernst and Ichiro Hasuo and Zhenya Zhang and Sean Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/pub/2018-SNR.Time-staging_Enhancement_of_Hybrid_System_Falsification.pdf}, note = {Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021.}, }
  2. Johannes Knaut. Symbolic Heap Abstraction with Automatic Refinement. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry
    @misc{JohannesSymbolicHeapRefinement, author = {Johannes Knaut}, title = {Symbolic Heap Abstraction with Automatic Refinement}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Knaut.Symbolic_Heap_Abstraction_with_Automatic_Refinement.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  3. Martin Spiessl. Configurable Software Verification based on Slicing Abstractions. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry
    @misc{MartinSplitting, author = {Martin Spiessl}, title = {Configurable Software Verification based on Slicing Abstractions}, 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}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  4. Thomas Lemberger. Abstraction Refinement for Model Checking: Program Slicing + CEGAR. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry
    @misc{ThomasSlicing, author = {Thomas Lemberger}, title = {Abstraction Refinement for Model Checking: Program Slicing + {CEGAR}}, 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}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
  5. Matthias Gerlach. Newton Refinement as Alternative to Craig Interpolation in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry
    @misc{GerlachNewtonRefinement, author = {Matthias Gerlach}, title = {Newton Refinement as Alternative to {Craig} Interpolation in {{\sc CPAchecker}}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/bsc/2018.Gerlach.Newton_Refinement_as_Alternative_to_Craig_Interpolation_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-01-09_BA_NewtonRefinementAsAlternativeToCraigInterpolationInCPAchecker_Gerlach.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  6. Flutura Estler. Heuristics-Based Selection of Verification Configurations. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{EstlerHeuristic, author = {Flutura Estler}, title = {Heuristics-Based Selection of Verification Configurations}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  7. Balthasar Schuess. Flexible Online Job Scheduling in a Multi-User Environment. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): Cloud-Based Software Verification
    BibTeX Entry
    @misc{SchuessScheduling, author = {Balthasar Schuess}, title = {Flexible Online Job Scheduling in a Multi-User Environment}, year = {2018}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  8. Dominik Friedrich. Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker
    BibTeX Entry
    @misc{FriedrichStatistics, author = {Dominik Friedrich}, title = {{Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker}}, year = {2018}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  9. Moritz Buhl. Application of Software Verification to OpenBSD Network Modules. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{BuhlOpenBSD, author = {Moritz Buhl}, title = {Application of Software Verification to {{\sc OpenBSD}} Network Modules}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  10. Nicholas Reyes. Integrating a Witness Store into a Distributed Verification System. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): Witness-Based Validation, Cloud-Based Software Verification
    BibTeX Entry
    @misc{ReyesWitnessStore, author = {Nicholas Reyes}, title = {Integrating a Witness Store into a Distributed Verification System}, year = {2018}, keyword = {Witness-Based Validation,Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  11. 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. Link to this entry Keyword(s): Cloud-Based Software Verification
    BibTeX Entry
    @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}, year = {2018}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  12. Karam Shabita. String Analysis for Java Programs in CPAchecker. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{SharamStrings, author = {Karam Shabita}, title = {String Analysis for {Java} Programs in {{\sc CPAchecker}}}, year = {2018}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }

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 Nov 18 19:35:54 2024 UTC