Publications of year 2016

Articles in conference or workshop proceedings

  1. Sven Apel, Dirk Beyer, Vitaly Mordan, Vadim Mutilin, and and Andreas Stahlbauer. On-the-Fly Decomposition of Specifications in Software Model Checking. In Proc. FSE, pages 349-361, 2016. ACM. [ PDF ]
    @InProceedings{FSE16a,
    author = {Sven Apel and Dirk Beyer and Vitaly Mordan and Vadim Mutilin and and Andreas Stahlbauer},
    title = {On-the-Fly Decomposition of Specifications in Software Model Checking},
    booktitle = {Proc.\ FSE},
    publisher = {ACM},
    pages = {349-361},
    year = {2016},
    isbn = {978-3-319-47165-5},
    doi = {10.1145/2950290.2950349},
    pdf = {https://www.sosy-lab.org/research/pub/2016-FSE.On-the-Fly_Decomposition_of_Specifications_in_Software_Model_Checking.pdf},
    
    }
    

  2. Dirk Beyer. Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques. In Proc. ISoLA (1), LNCS 9952, pages 874-880, 2016. Springer.
    @inproceedings{ISOLA16b,
    author = {Dirk Beyer},
    title = {Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques},
    booktitle = {Proc.\ ISoLA (1)},
    publisher = {Springer},
    series = {LNCS~9952},
    pages = {874-880},
    year = {2016},
    isbn = {978-3-319-47165-5},
    doi = {10.1007/978-3-319-47166-2},
    url = {},
    
    }
    

  3. D. Beyer. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). In Marsha Chechik and Jean-François Raskin, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2016, Eindhoven, The Netherlands, April 2-8), LNCS 9636, pages 887-904, 2016. Springer-Verlag, Heidelberg. [ Info ] [ PDF ]
    @inproceedings{TACAS16,
    author = {D.~Beyer},
    title = {Reliable and Reproducible Competition Results with {{\sc BenchExec}} and Witnesses ({R}eport on {SV-COMP} 2016)},
    booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2016, Eindhoven, The Netherlands, April 2-8)},
    editor = {Marsha Chechik and Jean{-}Fran{\c{c}}ois Raskin},
    series = {LNCS~9636},
    year = {2016},
    publisher = {Springer-Verlag, Heidelberg},
    pages = {887-904},
    isbn = {978-3-662-49674-9},
    doi = {10.1007/978-3-662-49674-9_55},
    pdf = {https://www.sosy-lab.org/research/pub/2016-TACAS.Reliable_and_Reproducible_Competition_Results_with_BenchExec_and_Witnesses.pdf},
    url = {http://sv-comp.sosy-lab.org/},
    
    }
    

  4. Dirk Beyer and Matthias Dangl. SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms. In Proc. VSTTE, LNCS 9971, pages 181--198, 2016. Springer.
    @InProceedings{VSTTE16b-AlgorithmComparison,
    author = {Dirk Beyer and Matthias Dangl},
    title = {{SMT}-based Software Model Checking: {A}n Experimental Comparison of Four Algorithms},
    booktitle = {Proc.\ VSTTE},
    publisher = {Springer},
    series = {LNCS~9971},
    pages = {181--198},
    year = {2016},
    doi = {10.1007/978-3-319-48869-1_14},
    url = {},
    
    }
    

  5. Dirk Beyer and Matthias Dangl. Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses. In Proc. CAV (2), LNCS 9780, pages 502-509, 2016. Springer. [ PDF ]
    @inproceedings{CAV16,
    author = {Dirk Beyer and Matthias Dangl},
    title = {Verification-Aided Debugging: {A}n Interactive Web-Service for Exploring Error Witnesses},
    booktitle = {Proc.\ CAV (2)},
    pages = {502-509},
    year = {2016},
    series = {LNCS~9780},
    publisher = {Springer},
    doi = {10.1007/978-3-319-41540-6_28},
    pdf = {https://www.sosy-lab.org/research/pub/2016-CAV.Verification-Aided_Debugging:_An_Interactive_Web-Service_for_Exploring_Error_Witnesses.pdf},
    
    }
    

  6. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Correctness Witnesses: Exchanging Verification Results Between Verifiers. In Proc. FSE, pages 326-337, 2016. ACM. [ PDF ]
    @InProceedings{FSE16b,
    author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann},
    title = {Correctness Witnesses: {E}xchanging Verification Results Between Verifiers},
    booktitle = {Proc.\ FSE},
    publisher = {ACM},
    pages = {326-337},
    year = {2016},
    doi = {10.1145/2950290.2950351},
    pdf = {https://www.sosy-lab.org/research/pub/2016-FSE.Correctness_Witnesses_Exchanging_Verification_Results_between_Verifiers.pdf},
    url = {},
    
    }
    

  7. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. Witness Validation and Stepwise Testification across Software Verifiers. In J. Knoop and U. Zdun, editors, Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, Österreich), LNI 252, pages 105-106, 2016. GI.
    @inproceedings{SE16b-VerificationWitnesses,
    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 = {Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, {\"O}sterreich)},
    publisher = {{GI}},
    editor = {J.~Knoop and U.~Zdun},
    series = {{LNI}~252},
    pages = {105-106},
    year = {2016},
    url = {},
    
    }
    

  8. Dirk Beyer and Karlheinz Friedberger. A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker. In J. Bouda, L. Holìk, J. Kofron, J. Strejcek, and A. Rambousek, editors, Proceedings of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016, Telc, Czechia, October 21-23), EPTCS 233, pages 61-71, 2016. ArXiV. [ PDF ]
    @inproceedings{MEMICS16-Multi-Threaded,
    author = {Dirk Beyer and Karlheinz Friedberger},
    title = {A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker},
    booktitle = {Proceedings of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS~2016, Tel\v{c}, Czechia, October 21-23)},
    publisher = {ArXiV},
    editor = {J.~Bouda and L.~Hol\'ik and J.~Kofro\v{n} and J.~Strej\v{c}ek and A.~Rambousek},
    series = {EPTCS~233},
    pages = {61-71},
    year = {2016},
    doi = {10.4204/EPTCS.233.6},
    pdf = {https://www.sosy-lab.org/research/pub/2016-MEMICS.A_Light-Weight_Approach_for_Verifying_Multi-Threaded_Programs_with_CPAchecker.pdf},
    
    }
    

  9. Dirk Beyer and Thomas Lemberger. Symbolic Execution with CEGAR. In Proc. ISoLA (1), LNCS 9952, pages 195-211, 2016. Springer. [ PDF ]
    @inproceedings{ISOLA16a,
    author = {Dirk Beyer and Thomas Lemberger},
    title = {Symbolic Execution with {CEGAR}},
    booktitle = {Proc.\ ISoLA (1)},
    publisher = {Springer},
    series = {LNCS~9952},
    pages = {195-211},
    year = {2016},
    doi = {10.1007/978-3-319-47166-2_14},
    pdf = {https://www.sosy-lab.org/research/pub/2016-ISoLA.Symbolic_Execution_with_CEGAR.pdf},
    
    }
    

  10. Karlheinz Friedberger. CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution). In Marsha Chechik and Jean-François Raskin, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2016, Eindhoven, The Netherlands, April 2-8), LNCS 9636, pages 912--915, 2016. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking.
    @inproceedings{CPABAM-COMP16,
    author = {Karlheinz Friedberger},
    title = {{CPA-BAM}: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution)},
    booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2016, Eindhoven, The Netherlands, April 2-8)},
    editor = {Marsha Chechik and Jean{-}Fran{\c{c}}ois Raskin},
    series = {LNCS~9636},
    pages = {912--915},
    year = {2016},
    publisher = {Springer-Verlag, Heidelberg},
    keyword = {Software Model Checking},
    isbn = {978-3-662-49673-2},
    url = {http://dx.doi.org/10.1007/978-3-662-49674-9_58},
    doi = {10.1007/978-3-662-49674-9_58},
    
    }
    

  11. Egor George Karpenkov, Karlheinz Friedberger, and Dirk Beyer. JavaSMT: A Unified Interface for SMT Solvers in Java. In Proc. VSTTE, LNCS 9971, pages 139--148, 2016. Springer.
    @inproceedings{VSTTE16a-JavaSMT,
    author = {Egor George Karpenkov and Karlheinz Friedberger and Dirk Beyer},
    title = {{{\sc JavaSMT}}: {A} Unified Interface for {SMT} Solvers in {Java}},
    booktitle = {Proc.\ VSTTE},
    series = {LNCS~9971},
    pages = {139--148},
    year = {2016},
    publisher = {Springer},
    doi = {10.1007/978-3-319-48869-1_11},
    url = {},
    
    }
    

  12. Egor George Karpenkov, David Monniaux, and Philipp Wendler. Program Analysis with Local Policy Iteration. In Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016, St. Petersburg, FL, USA, January 17-19), LNCS 9583, pages 127--146, 2016. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    @inproceedings{LPI,
    author = {Egor George Karpenkov and David Monniaux and Philipp Wendler},
    title = {Program Analysis with Local Policy Iteration},
    booktitle = {Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI~2016, St.~Petersburg, FL, USA, January 17-19)},
    pages = {127--146},
    year = {2016},
    series = {LNCS~9583},
    keyword = {Software Model Checking},
    publisher = {Springer-Verlag, Heidelberg},
    doi = {10.1007/978-3-662-49122-5_6},
    pdf = {https://arxiv.org/pdf/1509.03424},
    url = {http://lpi.metaworld.me},
    
    }
    

  13. Malte Lochau, Johannes Bürdek, Stefan Bauregger, Andreas Holzer, Alexander von Rhein, Sven Apel, and Dirk Beyer. On Facilitating Reuse in Multi-goal Test-Suite Generation for Software Product Lines. In J. Knoop and U. Zdun, editors, Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, Österreich), LNI 252, pages 81-82, 2016. GI.
    @inproceedings{SE16a-Test-SPL,
    author = {Malte Lochau and Johannes B{\"u}rdek and Stefan Bauregger and Andreas Holzer and Alexander von Rhein and Sven Apel and Dirk Beyer},
    title = {On Facilitating Reuse in Multi-goal Test-Suite Generation for Software Product Lines},
    booktitle = {Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, {\"O}sterreich)},
    publisher = {{GI}},
    editor = {J.~Knoop and U.~Zdun},
    series = {{LNI}~252},
    pages = {81-82},
    year = {2016},
    url = {},
    
    }
    

  14. Stefan Löwe. CPA-RefSel: CPAchecker with Refinement Selection (Competition Contribution). In Marsha Chechik and Jean-François Raskin, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2016, Eindhoven, The Netherlands, April 2-8), LNCS 9636, pages 916--919, 2016. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking.
    @inproceedings{CPAREFSEL-COMP16,
    author = {Stefan L{\"{o}}we},
    title = {{CPA-RefSel}: {{\sc CPAchecker}} with Refinement Selection (Competition Contribution)},
    booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2016, Eindhoven, The Netherlands, April 2-8)},
    editor = {Marsha Chechik and Jean{-}Fran{\c{c}}ois Raskin},
    series = {LNCS~9636},
    pages = {916--919},
    year = {2016},
    publisher = {Springer-Verlag, Heidelberg},
    keyword = {Software Model Checking},
    isbn = {978-3-662-49673-2},
    url = {http://dx.doi.org/10.1007/978-3-662-49674-9_59},
    doi = {10.1007/978-3-662-49674-9_59},
    
    }
    

  15. Markus Schordan, Dirk Beyer, and Jonas Lundberg. Evaluation and Reproducibility of Program Analysis and Verification (Track Introduction). In T. Margaria and B. Steffen, editors, Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2016, Corfu, Greece, October 10--14), LNCS 9952, pages 191-194, 2016. Springer-Verlag, Heidelberg.
    @inproceedings{ISOLA16-TrackIntro,
    author = {Markus Schordan and Dirk Beyer and Jonas Lundberg},
    title = {Evaluation and Reproducibility of Program Analysis and Verification (Track Introduction)},
    booktitle = {Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2016, Corfu, Greece, October 10--14)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {T.~Margaria and B.~Steffen},
    series = {LNCS~9952},
    pages = {191-194},
    year = {2016},
    isbn = {978-3-319-47165-5},
    doi = {10.1007/978-3-319-47166-2},
    url = {},
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Stephan Lukasczyk. Unbounded Heap Support for CPAchecker's Predicate Analysis Using SMT Arrays. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ Info ]
    @misc{LukasczykPredicateHeap,
    author = {Stephan Lukasczyk},
    title = {Unbounded Heap Support for {{\sc CPAchecker}}'s Predicate Analysis Using {SMT} Arrays},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    url = {https://research.lukasczyk.me/heaparray/},
    field = {Computer Science},
    
    }
    

  2. Magdalena Murr. Towards Understandable CPAchecker Counterexamples. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ]
    @misc{MurrCounterexampleReport,
    author = {Magdalena Murr},
    title = {Towards Understandable {{\sc CPAchecker}} Counterexamples},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    pdf = {https://www.sosy-lab.org/research/bsc/2016.Murr.Towards_Understandable_CPAchecker_Counterexamples.pdf},
    subject = {Mobile and Embedded Systems},
    
    }
    

  3. Sebastian Ott. Implementing a Termination Analysis using Configurable Software Analysis. Master's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ]
    @misc{SebastianTermination,
    author = {Sebastian Ott},
    title = {Implementing a Termination Analysis using Configurable Software Analysis},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    pdf = {https://www.sosy-lab.org/research/msc/2016.Ott.Implementing_a_Termination_Analysis_using_Configurable_Program_Analysis.pdf},
    
    }
    

  4. Thomas Stieglmaier. Augmenting Predicate Analysis with Auxiliary Invariants. Master's Thesis, University of Passau, Software Systems Lab, 2016. [ Info ] [ PDF ]
    @misc{ThomasInvariants,
    author = {Thomas Stieglmaier},
    title = {Augmenting Predicate Analysis with Auxiliary Invariants},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    pdf = {https://www.sosy-lab.org/research/msc/2016.Stieglmaier.Augmenting_Predicate_Analysis_with_Auxiliary_Invariants.pdf},
    url = {https://www.sosy-lab.org/research/msc/stieglmaier},
    
    }
    

  5. Maximilian Syri. Verification of Concurrent Programs by CFA Sequentialization. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016.
    @misc{SyriConcurrency,
    author = {Maximilian Syri},
    title = {Verification of Concurrent Programs by {CFA} Sequentialization},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    field = {Computer Science},
    
    }
    

  6. Stefan Weinzierl. Configurable Pointer-Alias Analysis in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ]
    @misc{WeinzierlPointerAliasing,
    author = {Stefan Weinzierl},
    title = {Configurable Pointer-Alias Analysis in {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2016},
    pdf = {https://www.sosy-lab.org/research/bsc/2016.Weinzierl.Configurable_Pointer-Alias_Analysis_for_CPAchecker.pdf},
    field = {Computer Science},
    
    }
    




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 18 13:27:46 2017


This document was translated from BibTEX by bibtex2html