Publications of year 2015

(All PublicationsIndex)

Articles in conference or workshop proceedings

  1. Dirk Beyer.
    Software Verification and Verifiable Witnesses (Report on SV-COMP 2015).
    In C. Baier and C. Tinelli, editors, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015, London, UK, April 13-17), LNCS 9035, pages 401-416, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): Competition on Software Verification (SV-COMP), Software Model Checking.

    @InProceedings{TACAS15,
    author = {Dirk Beyer},
    title = {Software Verification and Verifiable Witnesses (Report on {SV-COMP} 2015)},
    booktitle = {Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2015, London, UK, April 13-17)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {C.~Baier and C.~Tinelli},
    series = {LNCS~9035},
    pages = {401-416},
    year = {2015},
    isbn = {978-3-662-46680-3},
    keyword = {Competition on Software Verification (SV-COMP),Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-TACAS.Software_Verification_and_Verifiable_Witnesses.pdf},
    doi = {10.1007/978-3-662-46681-0_31},
    url = {http://sv-comp.sosy-lab.org/},
    
    }
    

  2. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer.
    Witness Validation and Stepwise Testification across Software Verifiers.
    In E. Di Nitto, M. Harman, and P. Heymans, editors, Proceedings of the 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2015, Bergamo, Italy, August 31 - September 4), pages 721-733, 2015.
    ACM, New York.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @InProceedings{FSE15,
    author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Andreas Stahlbauer},
    title = {Witness Validation and Stepwise Testification across Software Verifiers},
    booktitle = {Proceedings of the 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2015, Bergamo, Italy, August 31 - September 4)},
    publisher = {ACM, New York},
    editor = {E.~Di~Nitto and M.~Harman and P.~Heymans},
    pages = {721-733},
    year = {2015},
    isbn = {978-1-4503-3675-8},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-FSE15.Witness_Validation_and_Stepwise_Testification_across_Software_Verifiers.pdf},
    url = {},
    doi = {10.1145/2786805.2786867},
    
    }
    

  3. Dirk Beyer, Matthias Dangl, and Philipp Wendler.
    Boosting k-Induction with Continuously-Refined Invariants.
    In D. Kröning and C. S. Pasareanu, editors, Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015, San Francisco, CA, USA, July 18-24), LNCS 9206, pages 622-640, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    k-Induction is a promising technique to extend bounded model checking from falsification to verification. In software verification, k-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a k-induction proof. We boost the k-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to k-induction a data-flow-based invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The k-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based verification of C programs in terms of successful results.

    @InProceedings{CAV15,
    author = {Dirk Beyer and Matthias Dangl and Philipp Wendler},
    title = {Boosting k-Induction with Continuously-Refined Invariants},
    booktitle = {Proceedings of the 27th International Conference on Computer Aided Verification (CAV~2015, San Francisco, CA, USA, July 18-24)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {D.~Kr{\"o}ning and C.~S.~Pasareanu},
    series = {LNCS~9206},
    pages = {622-640},
    year = {2015},
    isbn = {978-3-319-21689-8},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-CAV.Boosting_k-Induction_with_Continuously-Refined_Invariants.pdf},
    url = {https://www.sosy-lab.org/research/cpa-k-induction/},
    doi = {10.1007/978-3-319-21690-4_42},
    abstract = { k-Induction is a promising technique to extend bounded model checking from falsification to verification. In software verification, k-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a k-induction proof. We boost the k-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to k-induction a data-flow-based invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The k-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based verification of C programs in terms of successful results. },
    
    }
    

  4. Dirk Beyer and Stefan Löwe.
    Interpolation for Value Analysis.
    In U. Assmann, B. Demuth, T. Spitta, G. Püschel, and R. Kaiser, editors, Tagungsband Software Engineering 2015, Fachtagung des GI-Fachbereichs Softwaretechnik (17. März - 20. März 2015, Dresden, Deutschland), LNI 239, pages 73-74, 2015.
    Gesellschaft für Informatik (GI).
    Keyword(s): CPAchecker, Software Model Checking.

    @inproceedings{SE15-ExplicitCEGAR,
    author = {Dirk Beyer and Stefan L{\"{o}}we},
    title = {Interpolation for Value Analysis},
    booktitle = {Tagungsband Software Engineering 2015, Fachtagung des GI-Fachbereichs Softwaretechnik (17. M{\"{a}}rz - 20. M{\"{a}}rz 2015, Dresden, Deutschland)},
    publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})},
    editor = {U.~A{\ss}mann and B.~Demuth and T.~Spitta and G.~P{\"{u}}schel and R.~Kaiser},
    series = {{LNI}~239},
    pages = {73-74},
    year = {2015},
    url = {},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  5. Dirk Beyer, Stefan Löwe, and Philipp Wendler.
    Benchmarking and Resource Measurement.
    In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 160-178, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): Benchmarking.
    Abstract

    Proper benchmarking and resource measurement is an important topic, because benchmarking is a widely-used method for the comparative evaluation of tools and algorithms in many research areas. It is essential for researchers, tool developers, and users, as well as for competitions. We formulate a set of requirements that are indispensable for reproducible benchmarking and reliable resource measurement of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework is complex and can (on Linux) currently only be done by using the cgroups feature of the kernel. We provide BenchExec, a ready-to-use, tool-independent, and free implementation of a benchmarking framework that fulfills all presented requirements, making reproducible benchmarking and reliable resource measurement easy. Our framework is able to work with a wide range of different tools and has proven its reliability and usefulness in the International Competition on Software Verification.
    An extended version of this article appeared in STTT.

    @InProceedings{SPIN15a,
    author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler},
    title = {Benchmarking and Resource Measurement},
    booktitle = {Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN~2015, Stellenbosch, South Africa, August 24-26)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {B.~Fischer and J.~Geldenhuys},
    series = {LNCS~9232},
    pages = {160-178},
    year = {2015},
    isbn = {978-3-319-23403-8},
    keyword = {Benchmarking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-SPIN.Benchmarking_and_Resource_Measurement.pdf},
    url = {https://www.sosy-lab.org/research/benchmarking/},
    doi = {10.1007/978-3-319-23404-5_12},
    annote = {An extended version of this article appeared in STTT.},
    abstract = { Proper benchmarking and resource measurement is an important topic, because benchmarking is a widely-used method for the comparative evaluation of tools and algorithms in many research areas. It is essential for researchers, tool developers, and users, as well as for competitions. We formulate a set of requirements that are indispensable for reproducible benchmarking and reliable resource measurement of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework is complex and can (on Linux) currently only be done by using the cgroups feature of the kernel. We provide BenchExec, a ready-to-use, tool-independent, and free implementation of a benchmarking framework that fulfills all presented requirements, making reproducible benchmarking and reliable resource measurement easy. Our framework is able to work with a wide range of different tools and has proven its reliability and usefulness in the International Competition on Software Verification. },
    
    }
    

  6. Dirk Beyer, Stefan Löwe, and Philipp Wendler.
    Refinement Selection.
    In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 20-38, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    Counterexample-guided abstraction refinement is a property-directed approach for the automatic construction of an abstract model for a given system. The approach learns information from infeasible error paths in order to refine the abstract model. We address the problem of selecting which information to learn from a given infeasible error path. In previous work, we presented a method that enables refinement selection by extracting a set of sliced prefixes from a given infeasible error path, each of which represents a different reason for infeasibility of the error path and thus, a possible way to refine the abstract model. In this work, we (1) define and investigate several promising heuristics for selecting an appropriate precision for refinement, and (2) propose a new combination of a value analysis and a predicate analysis that does not only find out which information to learn from an infeasible error path, but automatically decides which analysis should be preferred for a refinement. These contributions allow a more systematic refinement strategy for CEGAR-based analyses. We evaluated the idea on software verification. We provide an implementation of the new concepts in the verification framework CPAchecker and make it publicly available. In a thorough experimental study, we show that refinement selection often avoids state-space explosion where existing approaches diverge, and that it can be even more powerful if applied on a higher level, where it decides which analysis of a combination should be favored for a refinement.

    @InProceedings{SPIN15b,
    author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler},
    title = {Refinement Selection},
    booktitle = {Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN~2015, Stellenbosch, South Africa, August 24-26)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {B.~Fischer and J.~Geldenhuys},
    series = {LNCS~9232},
    pages = {20-38},
    year = {2015},
    isbn = {978-3-319-23403-8},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-SPIN.Refinement_Selection.pdf},
    url = {https://www.sosy-lab.org/research/cpa-ref-sel/},
    doi = {10.1007/978-3-319-23404-5_3},
    abstract = { Counterexample-guided abstraction refinement is a property-directed approach for the automatic construction of an abstract model for a given system. The approach learns information from infeasible error paths in order to refine the abstract model. We address the problem of selecting which information to learn from a given infeasible error path. In previous work, we presented a method that enables refinement selection by extracting a set of sliced prefixes from a given infeasible error path, each of which represents a different reason for infeasibility of the error path and thus, a possible way to refine the abstract model. In this work, we (1) define and investigate several promising heuristics for selecting an appropriate precision for refinement, and (2) propose a new combination of a value analysis and a predicate analysis that does not only find out which information to learn from an infeasible error path, but automatically decides which analysis should be preferred for a refinement. These contributions allow a more systematic refinement strategy for CEGAR-based analyses. We evaluated the idea on software verification. We provide an implementation of the new concepts in the verification framework CPAchecker and make it publicly available. In a thorough experimental study, we show that refinement selection often avoids state-space explosion where existing approaches diverge, and that it can be even more powerful if applied on a higher level, where it decides which analysis of a combination should be favored for a refinement. },
    
    }
    

  7. Dirk Beyer, Stefan Löwe, and Philipp Wendler.
    Sliced Path Prefixes: An Effective Method to Enable Refinement Selection.
    In S. Graf and M. Viswanathan, editors, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015, Grenoble, France, June 2-4), LNCS 9039, pages 228-243, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches ---including our previous work--- do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification framework CPAchecker and made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency.

    @InProceedings{FORTE15,
    author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler},
    title = {Sliced Path Prefixes: An Effective Method to Enable Refinement Selection},
    booktitle = {Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE~2015, Grenoble, France, June 2-4)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {S.~Graf and M.~Viswanathan},
    series = {LNCS~9039},
    pages = {228-243},
    year = {2015},
    isbn = {978-3-319-19194-2},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-FORTE.Sliced_Path_Prefixes_An_Effective_Method_to_Enable_Refinement_Selection.pdf},
    url = {https://www.sosy-lab.org/research/cpa-ref-sel/#FORTE15},
    doi = {10.1007/978-3-319-19195-9_15},
    abstract = { Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches ---including our previous work--- do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification framework CPAchecker and made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency. },
    
    }
    

  8. Johannes Bürdek, Malte Lochau, Stefan Bauregger, Andreas Holzer, Alexander von Rhein, Sven Apel, and Dirk Beyer.
    Facilitating Reuse in Multi-Goal Test-Suite Generation for Software Product Lines.
    In A. Egyed and I. Schaefer, editors, Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015, London, UK, April 13-15), LNCS 9033, pages 84-99, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @InProceedings{FASE15,
    author = {Johannes B{\"u}rdek and Malte Lochau and Stefan Bauregger and Andreas Holzer and Alexander von Rhein and Sven Apel and Dirk Beyer},
    title = {Facilitating Reuse in Multi-Goal Test-Suite Generation for Software Product Lines},
    booktitle = {Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE~2015, London, UK, April 13-15)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {A.~Egyed and I.~Schaefer},
    series = {LNCS~9033},
    pages = {84-99},
    year = {2015},
    isbn = {978-3-662-46674-2},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-FASE.Facilitating_Reuse_in_Multi-Goal_Test-Suite_Generation_for_Software_Product_Lines.pdf},
    url = {http://forsyte.at/software/cpatiger/},
    doi = {10.1007/978-3-662-46675-9_6},
    
    }
    

  9. Matthias Dangl, Stefan Löwe, and Philipp Wendler.
    CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution).
    In C. Baier and C. Tinelli, editors, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015, London, UK, April 13-17), LNCS 9035, pages 423--425, 2015.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking.
    Abstract

    We submit to SV-COMP'15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustable-block encoding, bounded model checking, invariant generation, and block-abstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP.
    Won categories ControlFlow, MemorySafety, and Overall, and received three silver and two bronze medals in SV-COMP'15

    @inproceedings{CPACHECKER-COMP15,
    author = {Matthias Dangl and Stefan L{\"{o}}we and Philipp Wendler},
    title = {{{\sc CPAchecker}} with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution)},
    booktitle = {Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2015, London, UK, April 13-17)},
    editor = {C.~Baier and C.~Tinelli},
    series = {LNCS~9035},
    pages = {423--425},
    year = {2015},
    publisher = {Springer-Verlag, Heidelberg},
    keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking},
    isbn = {978-3-662-46680-3},
    url = {http://dx.doi.org/10.1007/978-3-662-46681-0_34},
    doi = {10.1007/978-3-662-46681-0_34},
    pdf = {https://www.sosy-lab.org/research/pub/2015-TACAS.CPAchecker_with_Support_for_Recursive_Programs_and_Floating-Point_Arithmetic.pdf},
    annote = {Won categories ControlFlow, MemorySafety, and Overall, and received three silver and two bronze medals in SV-COMP'15},
    abstract = { We submit to SV-COMP'15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustable-block encoding, bounded model checking, invariant generation, and block-abstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP. },
    
    }
    

  10. Alexander von Rhein, Alexander Grebhahn, Sven Apel, Norbert Siegmund, Dirk Beyer, and Thorsten Berger.
    Presence-Condition Simplification in Highly Configurable Systems.
    In A. Bertolino, G. Canfora, and S. Elbaum, editors, Proceedings of the 37th International Conference on Software Engineering (ICSE 2015, Florence, Italy, May 16-24), pages 178-188, 2015.
    IEEE.
    [ Article ] Keyword(s): Software Model Checking.

    @InProceedings{ICSE15,
    author = {Alexander von Rhein and Alexander Grebhahn and Sven Apel and Norbert Siegmund and Dirk Beyer and Thorsten Berger},
    title = {Presence-Condition Simplification in Highly Configurable Systems},
    booktitle = {Proceedings of the 37th International Conference on Software Engineering (ICSE~2015, Florence, Italy, May 16-24)},
    publisher = {IEEE},
    editor = {A.~Bertolino and G.~Canfora and S.~Elbaum},
    pages = {178-188},
    year = {2015},
    isbn = {978-1-4799-1934-5},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-ICSE.Presence-Condition_Simplification_in_Highly_Configurable_Systems.pdf},
    url = {},
    doi = {10.1109/ICSE.2015.39},
    
    }
    

Internal reports

  1. Dirk Beyer, Matthias Dangl, and Philipp Wendler.
    Combining k-Induction with Continuously-Refined Invariants.
    Technical report MIP-1503, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Online: http://arxiv.org/abs/1502.00096
    An abbreviated version of this article appeared in Proc. CAV 2015.

    @TechReport{TR1503-PA15,
    author = {Dirk Beyer and Matthias Dangl and Philipp Wendler},
    title = {Combining k-Induction with Continuously-Refined Invariants},
    institution ={Department of Computer Science and Mathematics (FIM), University of Passau (PA)},
    number = {MIP-1503},
    month = {January},
    year = {2015},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-PA-TR1503.Combining_k-Induction_with_Continuously-Refined_Invariants.pdf},
    url = {https://www.sosy-lab.org/research/cpa-k-induction/},
    annote = {Online:  http://arxiv.org/abs/1502.00096 
    An abbreviated version of this article appeared in Proc. CAV 2015. }, }

  2. Dirk Beyer, Stefan Löwe, and Philipp Wendler.
    Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes.
    Technical report MIP-1501, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.
    Online: http://arxiv.org/abs/1502.00045
    Extended publications based on this article appeared in Proc. FORTE 2015 and Proc. SPIN 2015.

    @TechReport{TR1501-PA15,
    author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler},
    title = {Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes},
    institution ={Department of Computer Science and Mathematics (FIM), University of Passau (PA)},
    number = {MIP-1501},
    month = {January},
    year = {2015},
    keyword = {CPAchecker,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2015-PA-TR1501.Domain-Type-Guided_Refinement_Selection_Based_on_Sliced_Path_Prefixes.pdf},
    url = {https://www.sosy-lab.org/research/cpa-ref-sel/},
    annote = {Online:  http://arxiv.org/abs/1502.00045 
    Extended publications based on this article appeared in Proc. FORTE 2015 and Proc. SPIN 2015. }, }

Theses (PhD, MSc, BSc, Project)

  1. Karlheinz Friedberger.
    Block-Abstraction Memoization as an Approach to Verify Recursive Procedures.
    Master's Thesis, University of Passau, Software Systems Lab, 2015.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{KarlheinzBAMRecursion,
    author = {Karlheinz Friedberger},
    title = {Block-Abstraction Memoization as an Approach to Verify Recursive Procedures},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2015},
    pdf = {https://www.sosy-lab.org/research/msc/2015.Friedberger.Block-Abstraction_Memoization_as_an_Approach_to_Verify_Recursive_Procedures.pdf},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  2. Thomas Lemberger.
    Efficient Symbolic Execution using CEGAR over Two Abstract Domains.
    Bachelor's Thesis, University of Passau, Software Systems Lab, 2015.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{ThomasSymbolicExecution,
    author = {Thomas Lemberger},
    title = {Efficient Symbolic Execution using {CEGAR} over Two Abstract Domains},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2015},
    pdf = {https://www.sosy-lab.org/research/bsc/2015.Lemberger.Efficient_Symbolic_Execution_using_CEGAR_over_Two_Abstract_Domains.pdf},
    field = {Computer Science},
    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: Fri Feb 22 05:04:16 2019


This document was translated from BibTEX by bibtex2html