Publications of year 2014

Articles in journal or book chapters

  1. Dirk Beyer, Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan. Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171). Dagstuhl Reports, 4(4):1-19, 2014. [ Info ]
    @article{Dagstuhl14,
    author = {Dirk Beyer and Marieke Huisman and Vladimir Klebanov and Rosemary Monahan},
    title = {Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171)},
    journal = {Dagstuhl Reports},
    volume = {4},
    number = {4},
    pages = {1-19},
    year = {2014},
    url = {http://dx.doi.org/10.4230/DagRep.4.4.1},
    doi = {10.4230/DagRep.4.4.1},
    
    }
    

  2. Dirk Beyer and Andreas Stahlbauer. BDD-Based Software Verification: Applications to Event-Condition-Action Systems. International Journal on Software Tools for Technology Transfer (STTT), 16(5):507--518, 2014. [ Info ] [ PDF ]
    @article{STTT14-BDD,
    author = {Dirk Beyer and Andreas Stahlbauer},
    title = {{BDD}-Based Software Verification: Applications to Event-Condition-Action Systems},
    journal = {International Journal on Software Tools for Technology Transfer (STTT)},
    volume = {16},
    number = {5},
    pages = {507--518},
    year = {2014},
    pdf = {https://www.sosy-lab.org/research/pub/2014-STTT.BDD-Based_Software_Verification.pdf},
    url = {http://dx.doi.org/10.1007/s10009-014-0334-1},
    doi = {10.1007/s10009-014-0334-1},
    
    }
    

  3. Falk Howar, Malte Isberner, Maik Merten, Bernhard Steffen, Dirk Beyer, and Corina S. Pasareanu. Rigorous examination of reactive systems: The RERS challenges 2012 and 2013. International Journal on Software Tools for Technology Transfer (STTT), 16(5):457--464, 2014. [ Info ] [ PDF ]
    @article{STTT14-Intro,
    author = {Falk Howar and Malte Isberner and Maik Merten and Bernhard Steffen and Dirk Beyer and Corina S. Pasareanu},
    title = {Rigorous examination of reactive systems: The {RERS} challenges 2012 and 2013},
    journal = {International Journal on Software Tools for Technology Transfer (STTT)},
    volume = {16},
    number = {5},
    pages = {457--464},
    year = {2014},
    pdf = {https://www.sosy-lab.org/research/pub/2014-STTT.Rigorous_Examination_of_Reactive_Systems.pdf},
    url = {http://dx.doi.org/10.1007/s10009-014-0337-y},
    doi = {10.1007/s10009-014-0337-y},
    
    }
    

Articles in conference or workshop proceedings

  1. Dirk Beyer. Status Report on Software Verification (Competition Summary SV-COMP 2014). In E. Abraham and K. Havelund, editors, Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2014, Grenoble, France, April 5-13), LNCS 8413, pages 373-388, 2014. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    This report describes the 3rd International Competition on Software Verification (SV-COMP 2014), which is the third edition of a thorough comparative evaluation of fully automatic software verifiers. The reported results represent the state of the art in automatic software verification, in terms of effectiveness and efficiency. The verification tasks of the competition consist of nine categories containing a total of 2868 C programs, covering bit-vector operations, concurrent execution, control-flow and integer data-flow, device-drivers, heap data structures, memory manipulation via pointers, recursive functions, and sequentialized concurrency. The specifications include reachability of program labels and memory safety. The competition is organized as a satellite event at TACAS 2014 in Grenoble, France.

    @InProceedings{TACAS14,
    author = {Dirk Beyer},
    title = {Status Report on Software Verification (Competition Summary {SV-COMP} 2014)},
    booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2014, Grenoble, France, April 5-13)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {E.~Abraham and K. Havelund},
    series = {LNCS~8413},
    pages = {373-388},
    year = {2014},
    isbn = {978-3-642-54861-1},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2014-TACAS.Status_Report_on_Software_Verification.pdf},
    url = {http://sv-comp.sosy-lab.org/},
    doi = {10.1007/978-3-642-54862-8_25},
    abstract = { This report describes the 3rd International Competition on Software Verification (SV-COMP 2014), which is the third edition of a thorough comparative evaluation of fully automatic software verifiers. The reported results represent the state of the art in automatic software verification, in terms of effectiveness and efficiency. The verification tasks of the competition consist of nine categories containing a total of 2868 C programs, covering bit-vector operations, concurrent execution, control-flow and integer data-flow, device-drivers, heap data structures, memory manipulation via pointers, recursive functions, and sequentialized concurrency. The specifications include reachability of program labels and memory safety. The competition is organized as a satellite event at TACAS 2014 in Grenoble, France. },
    
    }
    

  2. Dirk Beyer, Georg Dresler, and Philipp Wendler. Software Verification in the Google App-Engine Cloud. In A. Biere and R. Bloem, editors, Proceedings of the 26th International Conference on Computer-Aided Verification (CAV 2014, Vienna, Austria, July 18-22), LNCS 8559, pages 327-333, 2014. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Software verification often requires a large amount of computing resources. In the last years, cloud services emerged as an inexpensive, flexible, and energy-efficient source of computing power. We have investigated if such cloud resources can be used effectively for verification. We chose the platform-as-a-service offer Google App Engine and ported the open-source verification framework CPAchecker to it. We provide our new verification service as a web front-end to users who wish to solve single verification tasks (tutorial usage), and an API for integrating the service into existing verification infrastructures (massively parallel bulk usage). We experimentally evaluate the effectiveness of this service and show that it can be successfully used to offload verification work to the cloud, considerably sparing local verification resources.

    @InProceedings{CAV14,
    author = {Dirk Beyer and Georg Dresler and Philipp Wendler},
    title = {Software Verification in the {Google} {App-Engine} Cloud},
    booktitle = {Proceedings of the 26th International Conference on Computer-Aided Verification (CAV~2014, Vienna, Austria, July 18-22)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {A.~Biere and R.~Bloem},
    series = {LNCS~8559},
    pages = {327-333},
    year = {2014},
    isbn = {978-3-319-08866-2},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2014-CAV.Software_Verification_in_the_Google_App-Engine_Cloud.pdf},
    url = {http://www.sosy-lab.org/~dbeyer/cpa-appengine},
    doi = {10.1007/978-3-319-08867-9_21},
    abstract = { Software verification often requires a large amount of computing resources. In the last years, cloud services emerged as an inexpensive, flexible, and energy-efficient source of computing power. We have investigated if such cloud resources can be used effectively for verification. We chose the platform-as-a-service offer Google App Engine and ported the open-source verification framework CPAchecker to it. We provide our new verification service as a web front-end to users who wish to solve single verification tasks (tutorial usage), and an API for integrating the service into existing verification infrastructures (massively parallel bulk usage). We experimentally evaluate the effectiveness of this service and show that it can be successfully used to offload verification work to the cloud, considerably sparing local verification resources. },
    
    }
    

  3. Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith. Reusing Information in Multi-Goal Reachability Analyses. In W. Hasselbring and N. C. Ehmke, editors, Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland), LNI 227, pages 97--98, 2014. GI. [ Info ]
    @inproceedings{SE14-MultiGoal,
    author = {Dirk Beyer and Andreas Holzer and Michael Tautschnig and Helmut Veith},
    title = {Reusing Information in Multi-Goal Reachability Analyses},
    booktitle = {Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland)},
    publisher = {{GI}},
    editor = {W.~Hasselbring and N.~C.~Ehmke},
    series = {{LNI}~227},
    pages = {97--98},
    year = {2014},
    url = {http://eprints.uni-kiel.de/23752/},
    
    }
    

  4. Dirk Beyer and Peter Häring. A Formal Evaluation of DepDegree Based on Weyuker's Properties. In C. Roy, A. Begel, and L. Moonen, editors, Proceedings of the 22nd International Conference on Program Comprehension (ICPC 2014, Hyderabad, India, June 2-3), pages 258-261, 2014. ACM. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Complexity of source code is an important characteristic that software engineers aim to quantify using static software measurement. Several measures used in practice as indicators for software complexity have theoretical flaws. In order to assess the quality of a software measure, Weyuker established a set of properties that an indicator for program-code complexity should satisfy. It is known that several well-established complexity indicators do not fulfill Weyuker's properties. We show that DepDegree, a measure for data-flow dependencies, satisfies all of Weyuker's properties.

    @InProceedings{ICPC14,
    author = {Dirk Beyer and Peter H{\"a}ring},
    title = {A Formal Evaluation of {DepDegree} Based on {Weyuker}'s Properties},
    booktitle = {Proceedings of the 22nd International Conference on Program Comprehension (ICPC~2014, Hyderabad, India, June 2-3)},
    publisher = {ACM},
    editor = {C.~Roy and A.~Begel and L.~Moonen},
    pages = {258-261},
    year = {2014},
    isbn = {978-1-4503-2879-1},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2014-ICPC.A_Formal_Evaluation_of_DepDegree_Based_on_Weyukers_Properties.pdf},
    url = {http://www.sosy-lab.org/~dbeyer/DepDegreeProperties},
    doi = {10.1145/2597008.2597794},
    abstract = { Complexity of source code is an important characteristic that software engineers aim to quantify using static software measurement. Several measures used in practice as indicators for software complexity have theoretical flaws. In order to assess the quality of a software measure, Weyuker established a set of properties that an indicator for program-code complexity should satisfy. It is known that several well-established complexity indicators do not fulfill Weyuker's properties. We show that DepDegree, a measure for data-flow dependencies, satisfies all of Weyuker's properties. },
    
    }
    

  5. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse in CPAchecker. In W. Hasselbring and N. C. Ehmke, editors, Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland), LNI 227, pages 41--42, 2014. GI. [ Info ]
    @inproceedings{SE14-Reuse,
    author = {Dirk Beyer and Stefan L{\"{o}}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler},
    title = {Precision Reuse in CPAchecker},
    booktitle = {Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland)},
    publisher = {{GI}},
    editor = {W.~Hasselbring and N.~C.~Ehmke},
    series = {{LNI}~227},
    pages = {41--42},
    year = {2014},
    url = {http://eprints.uni-kiel.de/23752/},
    
    }
    

  6. S. Löwe, M. U. Mandrykin, and P. Wendler. CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution). In E. Abraham and K. Havelund, editors, Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2014, Grenoble, France, April 5-13), LNCS 8413, pages 392-394, 2014. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking.
    @inproceedings{CPACHECKER-COMP14,
    author = {S.~L{\"{o}}we and M.~U.~Mandrykin and P.~Wendler},
    title = {{{\sc CPAchecker}} with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution)},
    booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2014, Grenoble, France, April 5-13)},
    editor = {E.~Abraham and K. Havelund},
    series = {LNCS~8413},
    year = {2014},
    pages = {392-394},
    publisher = {Springer-Verlag, Heidelberg},
    keyword = {Software Model Checking},
    isbn = {978-3-642-54861-1},
    url = {https://doi.org/10.1007/978-3-642-54862-8_27},
    doi = {10.1007/978-3-642-54862-8_27},
    
    }
    

  7. Markus Schordan, Welf Löwe, and Dirk Beyer. Evaluation and Reproducibility of Program Analysis (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 2014, Corfu, Greece, October 8-11), LNCS 8803, pages 479-481, 2014. Springer-Verlag, Heidelberg. [ Info ]
    @inproceedings{ISOLA14-TrackIntro,
    author = {Markus Schordan and Welf L{\"{o}}we and Dirk Beyer},
    title = {Evaluation and Reproducibility of Program Analysis (Track Introduction)},
    booktitle = {Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2014, Corfu, Greece, October 8-11)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {T.~Margaria and B.~Steffen},
    series = {LNCS~8803},
    pages = {479-481},
    year = {2014},
    url = {http://dx.doi.org/10.1007/978-3-662-45231-8_37},
    doi = {10.1007/978-3-662-45231-8_37},
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Georg Dresler. A Google-App-Engine Implementation for CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ Info ]
    @misc{DreslerAppEngine,
    author = {Georg Dresler},
    title = {A Google-App-Engine Implementation for {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2014},
    url = {https://www.sosy-lab.org/download/appengine.pdf},
    field = {Computer Science},
    
    }
    

  2. Sebastian Ott. VerifierCloud: Implementierung eines Web-Service zur Software-Verifikation. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ PDF ]
    @misc{SebastianVerifierCloud,
    author = {Sebastian Ott},
    title = {{{\sc VerifierCloud}}: Implementierung eines Web-Service zur Software-Verifikation},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2014},
    pdf = {https://www.sosy-lab.org/research/bsc/2014.Ott.VerifierCloud__Implementierung_eines_Web-Service_zur_Software-Verifikation.pdf},
    field = {Computer Science},
    
    }
    

  3. Thomas Stieglmaier. Octagon-Based Software Verification with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ PDF ]
    @misc{ThomasOctagon,
    author = {Thomas Stieglmaier},
    title = {Octagon-Based Software Verification with {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2014},
    pdf = {https://www.sosy-lab.org/research/bsc/2014.Stieglmaier.Octagon-Based_Software_Verification_with_CPAchecker.pdf},
    field = {Internet Computing},
    
    }
    




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 14:34:44 2017


This document was translated from BibTEX by bibtex2html