Software and Computational Systems Lab

Publications of year 2014

1. 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. doi:10.1007/s10009-014-0334-1 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   BibTeX Entry

   @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}, doi = {10.1007/s10009-014-0334-1}, sha256 = {}, url = {https://doi.org/10.1007/s10009-014-0334-1}, pdf = {https://www.sosy-lab.org/research/pub/2014-STTT.BDD-Based_Software_Verification.pdf}, keyword = {CPAchecker,Software Model Checking}, }
2. 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. doi:10.1007/s10009-014-0337-y Publisher's Version PDF Supplement
   BibTeX Entry

   @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}, doi = {10.1007/s10009-014-0337-y}, sha256 = {}, url = {https://doi.org/10.1007/s10009-014-0337-y}, pdf = {https://www.sosy-lab.org/research/pub/2014-STTT.Rigorous_Examination_of_Reactive_Systems.pdf}, }
3. 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. doi:10.4230/DagRep.4.4.1 Publisher's Version Supplement
   BibTeX Entry

   @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}, doi = {10.4230/DagRep.4.4.1}, sha256 = {}, url = {https://doi.org/10.4230/DagRep.4.4.1}, }
4. Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, and Wolfgang Reif. Compositional verification of a lock-free stack with RGITL. Electronic Communications of the Automated Verification of Critical Systems (EASST), 66, 2014.
   BibTeX Entry

   @article{ernst:east2014, author = {Bogdan Tofan and Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Wolfgang Reif}, title = {{Compositional verification of a lock-free stack with RGITL}}, journal = {Electronic Communications of the Automated Verification of Critical Systems (EASST)}, volume = {66}, year = {2014}, }
5. Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, and Wolfgang Reif. RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Annals of Mathematics and Artificial Intelligence (AMAI), 71:1-44, 2014. Springer.
   BibTeX Entry

   @article{ernst:amai2014, author = {Gerhard Schellhorn and Bogdan Tofan and Gidon Ernst and Jörg Pfähler and Wolfgang Reif}, title = {{RGITL: A temporal logic framework for compositional reasoning about interleaved programs}}, journal = {Annals of Mathematics and Artificial Intelligence (AMAI)}, volume = {71}, pages = {1--44}, year = {2014}, publisher = {Springer}, issue = {1--3}, }

6. 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. doi:10.1007/978-3-319-08867-9_21 Keyword(s): CPAchecker, Software Model Checking, Cloud-Based Software Verification Publisher's Version PDF Supplement
   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.
   BibTeX Entry

   @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)}, editor = {A.~Biere and R.~Bloem}, pages = {327-333}, year = {2014}, series = {LNCS~8559}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-08866-2}, doi = {10.1007/978-3-319-08867-9_21}, sha256 = {f92060721e703c8553d5420c34f07eea24fe25d36ae9c02217688606e1898704}, url = {http://www.sosy-lab.org/~dbeyer/cpa-appengine}, 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.}, keyword = {CPAchecker,Software Model Checking,Cloud-Based Software Verification}, }
7. 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. doi:10.1145/2597008.2597794 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Supplement
   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.
   BibTeX Entry

   @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)}, editor = {C.~Roy and A.~Begel and L.~Moonen}, pages = {258-261}, year = {2014}, publisher = {ACM}, isbn = {978-1-4503-2879-1}, doi = {10.1145/2597008.2597794}, url = {http://www.sosy-lab.org/~dbeyer/DepDegreeProperties}, pdf = {https://www.sosy-lab.org/research/pub/2014-ICPC.A_Formal_Evaluation_of_DepDegree_Based_on_Weyukers_Properties.pdf}, 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.}, keyword = {Structural Analysis and Comprehension}, }
8. 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 Analysis of Systems (TACAS 2014, Grenoble, France, April 5-13), LNCS 8413, pages 373-388, 2014. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-54862-8_25 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Publisher's Version PDF Supplement
   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.
   BibTeX Entry

   @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 Analysis of Systems (TACAS~2014, Grenoble, France, April 5-13)}, editor = {E.~Abraham and K. Havelund}, pages = {373-388}, year = {2014}, series = {LNCS~8413}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-54861-1}, doi = {10.1007/978-3-642-54862-8_25}, sha256 = {33d6c82695f46b11a762d5237608b7934f8bf664f5bd36ad3e1722591b398d7c}, url = {https://sv-comp.sosy-lab.org/2014/}, pdf = {https://www.sosy-lab.org/research/pub/2014-TACAS.Status_Report_on_Software_Verification.pdf}, 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.}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, }
9. 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. doi:10.1007/978-3-662-45231-8_37 Publisher's Version PDF Supplement
   BibTeX Entry

   @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)}, editor = {T.~Margaria and B.~Steffen}, pages = {479-481}, year = {2014}, series = {LNCS~8803}, publisher = {Springer-Verlag, Heidelberg}, doi = {10.1007/978-3-662-45231-8_37}, sha256 = {}, url = {https://doi.org/10.1007/978-3-662-45231-8_37}, }
10. 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. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    BibTeX Entry

    @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)}, editor = {W.~Hasselbring and N.~C.~Ehmke}, pages = {97--98}, year = {2014}, series = {{LNI}~227}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/30979/097.pdf?sequence=1&isAllowed=y}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2013.html#ESOP13">full article on this topic</a> that appeared in Proc. ESOP 2013.}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/30979}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. ESOP 2013.
11. 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. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    Abstract

    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.
    BibTeX Entry

    @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)}, editor = {W.~Hasselbring and N.~C.~Ehmke}, pages = {41--42}, year = {2014}, series = {{LNI}~227}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/30949/041.pdf?sequence=1&isAllowed=y}, abstract = {Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2013.html#FSE13">full article on this topic</a> that appeared in Proc. ESEC/FSE 2013.}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/30949}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. ESEC/FSE 2013.
12. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, and Wolfgang Reif. Modular refinement for submachines of ASMs. In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ), LNCS, pages 188-203, 2014. Springer. PDF
    BibTeX Entry

    @inproceedings{ernst:abz2014, author = {Gidon Ernst and Jörg Pfähler and Gerhard Schellhorn and Wolfgang Reif}, title = {{Modular refinement for submachines of ASMs}}, booktitle = {Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ)}, volume = {8477}, pages = {188--203}, year = {2014}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2014-ABZ.Modular_Refinement_for_Submachines_of_ASMs.pdf}, }
13. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, and Wolfgang Reif. Development of a verified Flash file system. In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ), LNCS, pages 9-24, 2014. Springer. Invited Paper PDF
    BibTeX Entry

    @inproceedings{ernst:abz2014-overview, author = {Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Dominik Haneberg and Wolfgang Reif}, title = {{Development of a verified Flash file system}}, booktitle = {Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ)}, volume = {8477}, pages = {9--24}, year = {2014}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2014-ABZ.Development_of_a_Verified_Flash_File_System.pdf}, note = {Invited Paper}, }
14. Stefan Löwe, Mikhail U. Mandrykin, and Philipp 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 Analysis of Systems (TACAS 2014, Grenoble, France, April 5-13), LNCS 8413, pages 392-394, 2014. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-54862-8_27 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    Abstract

    CPAchecker is a framework for software verification, built on the foundations of configurable program analysis (CPA). For the SV-COMP'14, we file a CPAchecker configuration that runs up to five analyses in sequence. The first two analyses of our approach utilize the explicit-value domain for modeling the state space, while the remaining analyses are based on predicate abstraction. In addition to that, a bit-precise counterexample checker comes into action whenever an analysis finds a counterexample. The combination of conceptually different analyses is key to the success of our verification approach, as the diversity of verification tasks is taken into account.
    BibTeX Entry

    @inproceedings{CPACHECKER-COMP14, author = {Stefan~L{\"{o}}we and Mikhail~U.~Mandrykin and Philipp~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 Analysis of Systems (TACAS~2014, Grenoble, France, April 5-13)}, editor = {E.~Abraham and K. Havelund}, pages = {392-394}, year = {2014}, series = {LNCS~8413}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-54861-1}, doi = {10.1007/978-3-642-54862-8_27}, sha256 = {}, url = {https://doi.org/10.1007/978-3-642-54862-8_27}, pdf = {https://www.sosy-lab.org/research/pub/2014-TACAS.CPAchecker_with_Sequential_Combination_of_Explicit-Value_Analyses_and_Predicate_Analyses.pdf}, abstract = {CPAchecker is a framework for software verification, built on the foundations of configurable program analysis (CPA). For the SV-COMP'14, we file a CPAchecker configuration that runs up to five analyses in sequence. The first two analyses of our approach utilize the explicit-value domain for modeling the state space, while the remaining analyses are based on predicate abstraction. In addition to that, a bit-precise counterexample checker comes into action whenever an analysis finds a counterexample. The combination of conceptually different analyses is key to the success of our verification approach, as the diversity of verification tasks is taken into account.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won categories ControlFlow, MemorySafety, and Simple, and received one silver and one bronze medal in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2014/">SV-COMP'14</a></span>}, }
    Additional Infos

    Won categories ControlFlow, MemorySafety, and Simple, and received one silver and one bronze medal in SV-COMP'14

15. Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif. Crash-safe refinement for a verified Flash file system. Technical report 2014-02, University of Augsburg, 2014. PDF
    BibTeX Entry

    @techreport{ernst:tr2014-02, author = {Jörg Pfähler and Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Wolfgang Reif}, title = {{Crash-safe refinement for a verified Flash file system}}, number = {2014-02}, year = {2014}, pdf = {https://www.sosy-lab.org/research/pub/2014-TR.Crash-Safe_Refinement_for_a_Verified_Flash_File_System.pdf}, institution = {University of Augsburg}, type = {Technical Report}, }
16. Yuyan Bao, Gary Leavens, and Gidon Ernst. Translating separation logic into dynamic frames using fine-grained region logic. Technical report CS-TR-13-02a, University of Central Florida, 2014.
    BibTeX Entry

    @techreport{ernst:bao2014, author = {Yuyan Bao and Gary Leavens and Gidon Ernst}, title = {{Translating separation logic into dynamic frames using fine-grained region logic}}, number = {CS-TR-13-02a}, year = {2014}, institution = {University of Central Florida}, type = {Technical Report}, }

17. Sebastian Ott. VerifierCloud: Implementierung eines Web-Service zur Software-Verifikation. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): Cloud-Based Software Verification PDF
    BibTeX Entry

    @misc{SebastianVerifierCloud, author = {Sebastian Ott}, title = {{{\sc VerifierCloud}}: Implementierung eines Web-Service zur Software-Verifikation}, year = {2014}, pdf = {https://www.sosy-lab.org/research/bsc/2014.Ott.VerifierCloud__Implementierung_eines_Web-Service_zur_Software-Verifikation.pdf}, keyword = {Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
18. Thomas Stieglmaier. Octagon-Based Software Verification with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{ThomasOctagon, author = {Thomas Stieglmaier}, title = {Octagon-Based Software Verification with {{\sc CPAchecker}}}, year = {2014}, pdf = {https://www.sosy-lab.org/research/bsc/2014.Stieglmaier.Octagon-Based_Software_Verification_with_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Internet Computing}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
19. Georg Dresler. A Google-App-Engine Implementation for CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. Keyword(s): CPAchecker, Software Model Checking Supplement
    BibTeX Entry

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