Gastvorträge am Mittwoch 27.11.: "Klimawandel und Extremereignisse – neue Erkenntnisse für die Klimafolgenforschung durch die Nutzung von HPC" im Rahmen der Public Climate School von Students for Future Munich.

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, H. Veith, and R. Bloem, 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 and R.~Bloem},
    publisher = {Springer},
    pages = {493-540},
    year = {2018},
    doi = {10.1007/978-3-319-10575-8_16},
    pdf = {https://www.sosy-lab.org/research/pub/2018-HBMC.Combining_Model_Checking_and_Data-Flow_Analysis.pdf},
    isbn = {978-3-319-10574-1},
    annote = {DOI: 10.1007/978-3-319-10575-8_16},
    
    }
    

  2. Marie-Christine Jakobs.
    Spontane Sicherheitsprüfung mittels individualisierter Programmzertifizierung oder Programmrestrukturierung.
    In S. Hölldobler, editor, Ausgezeichnete Informatikdissertationen 2017, volume D-18 of LNI, pages 91-100.
    Gesellschaft für Informatik (GI), 2018.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    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.
    This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.

    @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},
    pages = {91-100},
    series = {{LNI}},
    volume = {{D-18}},
    publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})},
    year = {2018},
    isbn = {978-3885799771},
    doi = {20.500.12116/19486},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19486/invited_paper_14.pdf?sequence=1&isAllowed=y},
    annote = {This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.},
    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. },
    
    }
    

  3. Philipp Wendler.
    Beiträge zu praktikabler Prädikatenanalyse.
    In S. Hölldobler, editor, Ausgezeichnete Informatikdissertationen 2017, volume D-18 of LNI, pages 261-270.
    Gesellschaft für Informatik (GI), 2018.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): Benchmarking, CPAchecker, Software Model Checking.
    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.
    This is a German summary of the dissertation Towards Practical Predicate Analysis.

    @incollection{DissZusammenfassungWendler,
    author = {Philipp Wendler},
    title = {Beitr{\"{a}}ge zu praktikabler Pr{\"{a}}dikatenanalyse},
    booktitle = {Ausgezeichnete Informatikdissertationen 2017},
    editor = {S. H{\"{o}}lldobler},
    pages = {261-270},
    series = {{LNI}},
    volume = {{D-18}},
    publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})},
    year = {2018},
    isbn = {978-3885799771},
    doi = {20.500.12116/19476},
    keyword = {Benchmarking,CPAchecker,Software Model Checking},
    pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19476/invited_paper_4.pdf?sequence=1&isAllowed=y},
    url = {https://www.sosy-lab.org/research/phd/wendler/},
    postscript= {https://www.sosy-lab.org/research/prs/2018-05-08_GiDiss_BeitraegeZuPraktikablerPraedikatenanalyse.pdf},
    annote = {This is a German summary of the dissertation Towards Practical Predicate Analysis.},
    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. },
    
    }
    

  4. Y. Bao, G. T. Leavens, and G. Ernst.
    Unifying separation logic and region logic to allow interoperability.
    Formal Aspects of Computing, 30(3--4):381--441, 2018.

    @article{ernst:bao2018,
    author = {Y. Bao and G. T. Leavens and G. Ernst},
    title = {Unifying separation logic and region logic to allow interoperability},
    journal = {Formal Aspects of Computing},
    pages = {381--441},
    volume = {30},
    number = {3--4},
    year = {2018},
    publisher = {Springer},
    
    }
    

  5. 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 ] [ Presentation ] 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.
    DOI: 10.1007/s10817-017-9432-6
    Publication appeared first online in December 2017
    CPAchecker is available at: https://cpachecker.sosy-lab.org/

    @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/},
    postscript= {https://www.sosy-lab.org/research/prs/Current_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},
    annote = {DOI: 10.1007/s10817-017-9432-6
    Publication appeared first online in December 2017
    CPAchecker is available at: https://cpachecker.sosy-lab.org/}, }

  6. G. Schellhorn, G. Ernst, J. Pfähler, S. Bodenmüller, and W. Reif.
    Symbolic execution for a clash-free subset of ASMs.
    Science of Computer Programming (SCP), 158:21--40, 2018.
    [ Article ]
    @article{ernst:scp2017,
    title = {{Symbolic execution for a clash-free subset of ASMs}},
    author = {G. Schellhorn and G. Ernst and J. Pf{\"a}hler and S. Bodenm{\"u}ller and W. Reif},
    journal = {Science of Computer Programming (SCP)},
    volume = {158},
    pages = {21--40},
    publisher = {Elsevier},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/pub/2017-SCP.Symbolic_Execution_for_a_Clash-Free_Subset_of_ASMs.pdf},
    
    }
    

  7. Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, and I. 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.
    [ Article ]
    @article{ernst:emsoft2018,
    author = {Z. Zhang and G. Ernst and S. Sedwards and P. Arcaini and I. 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)},
    publisher = {IEEE},
    volume={37},
    number={11},
    pages={2894--2905},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/pub/2018-TCAD.Two-Layered_Falsification_of_Hybrid_Systems_guided_by_Monte_Carlo_Tree_Search.pdf},
    
    }
    

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, 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.
    [ 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 = {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},
    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), LNCS 10889, pages 3-23, 2018.
    Springer.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main).
    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)},
    series = {LNCS~10889},
    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,Witness-Based Validation,Witness-Based Validation (main)},
    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.
    [ Material ] [ 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},
    url = {https://www.sosy-lab.org/research/bam-parallel/},
    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, 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.
    [ 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 = {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},
    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 ] [ Presentation ] 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/},
    postscript = {https://www.sosy-lab.org/research/prs/2018-06-01_ICSE18_ReducerBasedConstructionOfConditionalVerifiers_Marie.pdf},
    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), pages 900-903, 2018.
    ACM.
    [ Material ] [ Article ] [ Presentation ] 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)},
    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},
    postscript = {https://www.sosy-lab.org/research/prs/2018-09-07_ASE18_CPASymExec_Thomas.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. },
    
    }
    

  7. A. Dokhanchi, S. Yaghoubi, B. Hoxha, G. Fainekos, G. Ernst, Z. Zhang, P. Arcaini, I. Hasuo, and S. Sedwards.
    ARCH-COMP18 Category Report: Results on the Falsification Benchmarks.
    In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), volume 54 of EPiC, pages 104--109, 2018.
    EasyChair.
    [ Article ]
    @inproceedings{ernst:arch2018,
    title = {{ARCH-COMP18 Category Report: Results on the Falsification Benchmarks}},
    author = {A. Dokhanchi and S. Yaghoubi and B. Hoxha and G. Fainekos and G. Ernst and Z. Zhang and P. Arcaini and I. Hasuo and S. Sedwards},
    booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)},
    series = {EPiC},
    volume = {54},
    pages = {104--109},
    publisher = {EasyChair},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/pub/2018-ARCH.Results_on_the_Falsification_Benchmarks.pdf},
    
    }
    

  8. G. Ernst, I. Hasuo, Z. Zhang, and S. Sedwards.
    Time-staging Enhancement of Hybrid System Falsification.
    In Proc. of Symbolic and Numerical Methods for Reachability Analysis (SNR), EPTCS, 2018.
    [ Article ]
    @inproceedings{ernst:snr2018,
    author = {G. Ernst and I. Hasuo and Z. Zhang and S. Sedwards},
    title = {{Time-staging Enhancement of Hybrid System Falsification}},
    booktitle = {Proc. of Symbolic and Numerical Methods for Reachability Analysis (SNR)},
    series = {EPTCS},
    year = {2018},
    pdf = {https://www.sosy-lab.org/research/pub/2018-SNR.Time-staging_Enhancement_of_Hybrid_System_Falsification.pdf},
    
    }
    

  9. A. Issa, T. Murray, and G. 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.
    Work in Progress Report. [ Article ]
    @inproceedings{ernst:ozchi2018,
    title = {{In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces}},
    author = {A. Issa and T. Murray and G. Ernst},
    booktitle = {Proc. of Computer Human Interaction Australia (OzCHI)},
    year = {2018},
    pages = {572--576},
    publisher = {ACM},
    note = {Work in Progress Report.},
    pdf = {https://www.sosy-lab.org/research/pub/2018-OzCHI.In_Search_of_Perfect_Users.pdf},
    
    }
    

  10. 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.

    @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},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {T.~Margaria and B.~Steffen},
    series = {LNCS~11245},
    pages = {139-143},
    year = {2018},
    isbn = {978-3-030-03420-7},
    doi = {10.1007/978-3-030-03421-4_10},
    url = {},
    
    }
    

  11. Z. Zhang, G. Ernst, I. Hasuo, and S. Sedwards.
    Time-staging Enhancement of Hybrid System Falsification (Abstract).
    In Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS), 2018.
    IEEE.

    @inproceedings{ernst:mt-cps2018,
    author = {Z. Zhang and G. Ernst and I. Hasuo and S. Sedwards},
    title = {{Time-staging Enhancement of Hybrid System Falsification (Abstract)}},
    booktitle = {Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS)},
    publisher = {IEEE},
    year = {2018},
    
    }
    

Internal reports

  1. M. Huisman, R. Monahan, P. Müller, A. Paskevich, and G. Ernst.
    VerifyThis 2018: A Program Verification Competition.
    Technical report hal-01981937, Université Paris-Saclay, 2018.
    [ Material ] [ Article ]
    @techreport{ernst:verifythis2018,
    title = {{VerifyThis 2018: A Program Verification Competition}},
    author = {M. Huisman and R. Monahan and P. M{\"u}ller and A. Paskevich and G. Ernst},
    year = {2018},
    url = {https://hal.inria.fr/hal-01981937},
    institution = {Universit{\'e} Paris-Saclay},
    number = {hal-01981937},
    pdf = {https://www.sosy-lab.org/research/pub/2018-HAL.VerifyThis_2018.pdf},
    
    }
    

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. Flutura Estler.
    Heuristics-Based Selection of Verification Configurations.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): CPAchecker, Software Model Checking.

    @misc{EstlerHeuristic,
    author = {Flutura Estler},
    title = {Heuristics-Based Selection of Verification Configurations},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking} 
    }
    

  3. 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} 
    }
    

  4. Matthias Gerlach.
    Newton Refinement as Alternative to Craig Interpolation in CPAchecker.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{GerlachNewtonRefinement,
    author = {Matthias Gerlach},
    title = {Newton Refinement as Alternative to Craig Interpolation in CPAchecker},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/bsc/2018.Gerlach.Newton_Refinement_as_Alternative_to_Craig_Interpolation_in_CPAchecker.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2019-01-09_BA_NewtonRefinementAsAlternativeToCraigInterpolationInCPAchecker_Gerlach.pdf},
    
    }
    

  5. 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{JohannesSymbolicHeapRefinement,
    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},
    
    }
    

  6. 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},
    
    }
    

  7. 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} 
    }
    

  8. Nicholas Reyes.
    Integrating a Witness Store into a Distributed Verification System.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): Witness-Based 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-Based Validation,Cloud-Based Software Verification} 
    }
    

  9. Balthasar Schuess.
    Flexible Online Job Scheduling in a Multi-User Environment.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018.
    Keyword(s): Cloud-Based Software Verification.

    @misc{SchuessScheduling,
    author = {Balthasar Schuess},
    title = {Flexible Online Job Scheduling in a Multi-User Environment},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2018},
    field = {Computer Science},
    keyword = {Cloud-Based Software Verification} 
    }
    

  10. 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},
    
    }
    

  11. 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 16 10:15:29 2019


This document was translated from BibTEX by bibtex2html