Software and Computational Systems Lab

Publications of year 2010

1. Dirk Beyer, M. Erkan Keremoglu, and Philipp Wendler. Predicate Abstraction with Adjustable-Block Encoding. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20-23), pages 189-197, 2010. FMCAD. Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   Several successful software model checkers are based on a technique called single-block encoding (SBE), which computes costly predicate abstractions after every single program operation. Large-block encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustable-block encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.
   BibTeX Entry

   @inproceedings{FMCAD10, author = {Dirk Beyer and M.~Erkan Keremoglu and Philipp Wendler}, title = {Predicate Abstraction with Adjustable-Block Encoding}, booktitle = {Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2010, Lugano, October 20-23)}, pages = {189-197}, year = {2010}, publisher = {FMCAD}, isbn = {}, url = {http://www.sosy-lab.org/~dbeyer/cpa-abe/}, pdf = {https://www.sosy-lab.org/research/pub/2010-FMCAD.Predicate_Abstraction_with_Adjustable-Block_Encoding.pdf}, abstract = {Several successful software model checkers are based on a technique called single-block encoding (SBE), which computes costly predicate abstractions after every single program operation. Large-block encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustable-block encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems}, doinone = {DOI not available}, urlpub = {https://ieeexplore.ieee.org/document/5770949/}, }
   Additional Infos

   Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems
2. Dirk Beyer and Ashgan Fararooy. CheckDep: A Tool for Tracking Software Dependencies. In Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC 2010, Braga, June 30 - July 2), pages 42-43, 2010. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICPC.2010.51 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF
   Abstract

   Many software developers use a syntactical 'diff' in order to perform a quick review before committing changes to the repository. Others are notified of the change by e-mail (containing diffs or change logs), and they review the received information to determine if their work is affected. We lift this simple process from the code level to the more abstract level of dependencies: a software developer can use CheckDep to inspect introduced and removed dependencies before committing new versions, and other developers receive summaries of the changed dependencies via e-mail. We find the tool useful in our software-development activities and now make the tool publicly available.
   BibTeX Entry

   @inproceedings{ICPC10c, author = {Dirk Beyer and Ashgan Fararooy}, title = {{{\sc CheckDep}}: A Tool for Tracking Software Dependencies}, booktitle = {Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC~2010, Braga, June 30 - July 2)}, pages = {42-43}, year = {2010}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {978-0-7695-4113-6}, doi = {10.1109/ICPC.2010.51}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.CheckDep_A_Tool_for_Tracking_Software_Dependencies.pdf}, abstract = {Many software developers use a syntactical `diff' in order to perform a quick review before committing changes to the repository. Others are notified of the change by e-mail (containing diffs or change logs), and they review the received information to determine if their work is affected. We lift this simple process from the code level to the more abstract level of dependencies: a software developer can use CheckDep to inspect introduced and removed dependencies before committing new versions, and other developers receive summaries of the changed dependencies via e-mail. We find the tool useful in our software-development activities and now make the tool publicly available.}, keyword = {Structural Analysis and Comprehension}, }
3. Dirk Beyer and Ashgan Fararooy. DepDigger: A Tool for Detecting Complex Low-Level Dependencies. In Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC 2010, Braga, June 30 - July 2), pages 40-41, 2010. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICPC.2010.52 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF
   Abstract

   We present a tool that identifies complex data-flow dependencies on code-level, based on the measure dep-degree. Low-level dependencies between program operations are modeled by the use-def graph, which is generated from reaching definitions of variables. The tool annotates program operations with their dep-degree values, such that 'difficult' program operations are easy to locate. We hope that this tool helps detecting and preventing code degeneration, which is often a challenge in today's software projects, due to the high refactoring and restructuring frequency.
   BibTeX Entry

   @inproceedings{ICPC10b, author = {Dirk Beyer and Ashgan Fararooy}, title = {{{\sc DepDigger}}: A Tool for Detecting Complex Low-Level Dependencies}, booktitle = {Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC~2010, Braga, June 30 - July 2)}, pages = {40-41}, year = {2010}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {978-0-7695-4113-6}, doi = {10.1109/ICPC.2010.52}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.DepDigger_A_Tool_for_Detecting_Complex_Low-Level_Dependencies.pdf}, abstract = {We present a tool that identifies complex data-flow dependencies on code-level, based on the measure dep-degree. Low-level dependencies between program operations are modeled by the use-def graph, which is generated from reaching definitions of variables. The tool annotates program operations with their dep-degree values, such that `difficult' program operations are easy to locate. We hope that this tool helps detecting and preventing code degeneration, which is often a challenge in today's software projects, due to the high refactoring and restructuring frequency.}, keyword = {Structural Analysis and Comprehension}, }
4. Dirk Beyer and Ashgan Fararooy. A Simple and Effective Measure for Complex Low-Level Dependencies. In Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC 2010, Braga, June 30 - July 2), pages 80-83, 2010. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICPC.2010.49 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Presentation
   Abstract

   The measure dep-degree is a simple indicator for structural problems and complex dependencies on code-level. We model low-level dependencies between program operations as use-def graph, which is generated from reaching definitions of variables. The more dependencies a program operation has, the more different program states have to be considered and the more difficult it is to understand the operation. Dep-degree is simple to compute and interpret, flexible and scalable in its application, and independently complementing other indicators. Preliminary experiments suggest that the measure dep-degree, which simply counts the number of dependency edges in the use-def graph, is a good indicator for readability and understandablity.
   BibTeX Entry

   @inproceedings{ICPC10a, author = {Dirk Beyer and Ashgan Fararooy}, title = {A Simple and Effective Measure for Complex Low-Level Dependencies}, booktitle = {Proceedings of the 18th IEEE International Conference on Program Comprehension (ICPC~2010, Braga, June 30 - July 2)}, pages = {80-83}, year = {2010}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {978-0-7695-4113-6}, doi = {10.1109/ICPC.2010.49}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.A_Simple_and_Effective_Measure_for_Complex_Low-Level_Dependencies.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2010-06_DepDegree.pdf}, abstract = {The measure dep-degree is a simple indicator for structural problems and complex dependencies on code-level. We model low-level dependencies between program operations as use-def graph, which is generated from reaching definitions of variables. The more dependencies a program operation has, the more different program states have to be considered and the more difficult it is to understand the operation. Dep-degree is simple to compute and interpret, flexible and scalable in its application, and independently complementing other indicators. Preliminary experiments suggest that the measure dep-degree, which simply counts the number of dependency edges in the use-def graph, is a good indicator for readability and understandablity.}, keyword = {Structural Analysis and Comprehension}, }
5. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz, and Damien Zufferey. Shape Refinement through Explicit Heap Analysis. In D.S. Rosenblum and G. Taentzer, editors, Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010, Paphos, Cyprus, March 22-26), LNCS 6013, pages 263-277, 2010. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-12029-9_19 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.
   BibTeX Entry

   @inproceedings{FASE10, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz and Damien Zufferey}, title = {Shape Refinement through Explicit Heap Analysis}, booktitle = {Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE~2010, Paphos, Cyprus, March 22-26)}, editor = {D.S.~Rosenblum and G.~Taentzer}, pages = {263-277}, year = {2010}, series = {LNCS~6013}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-12028-2}, doi = {10.1007/978-3-642-12029-9_19}, sha256 = {60468f681028a3ac427897405ee5c99894c5baa340896454d378d55267be304f}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2010-FASE.Shape_Refinement_through_Explicit_Heap_Analysis.pdf}, abstract = {Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.}, keyword = {BLAST,Software Model Checking}, }
6. Markus Schordan, Dirk Beyer, and Irena Bojanova. Software Verification Tools (Track Introduction). In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodes, Greece, October 20-30), part 4, LNCS 12479, pages 177-181, 2010. Springer-Verlag, Heidelberg. doi:10.1007/978-3-030-83723-5_12 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{ISOLA20d-TrackIntro, author = {Markus Schordan and Dirk Beyer and Irena Bojanova}, title = {Software Verification Tools (Track Introduction)}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodes, Greece, October 20--30), part 4}, editor = {T.~Margaria and B.~Steffen}, pages = {177-181}, year = {2010}, series = {LNCS~12479}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-030-03420-7}, doi = {10.1007/978-3-030-83723-5_12}, sha256 = {}, url = {}, keyword = {}, }
7. Faisal Aslam, Luminous Fennell, Christian Schindelhauer, Peter Thiemann, Gidon Ernst, Elmar Haussmann, Stefan Rührup, and and Zastash A. Uzmi. Optimized Java binary and virtual machine for tiny motes. In Proc. of Distributed Computing in Sensor Systems (DCOSS), LNCS, pages 15-30, 2010. Springer.
   BibTeX Entry

   @inproceedings{ernst:dcoss2010, author = {Faisal Aslam and Luminous Fennell and Christian Schindelhauer and Peter Thiemann and Gidon Ernst and Elmar Haussmann and Stefan Rührup and and Zastash A. Uzmi}, title = {{Optimized Java binary and virtual machine for tiny motes}}, booktitle = {Proc. of Distributed Computing in Sensor Systems (DCOSS)}, volume = {6131}, pages = {15--30}, year = {2010}, series = {LNCS}, publisher = {Springer}, }

8. CheckDep: Tracking Software Dependencies. 2010. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{CheckDep, title = {{{\sc CheckDep}}: Tracking Software Dependencies}, year = {2010}, url = {http://www.sosy-lab.org/~dbeyer/CheckDep/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer, architect, and maintenance}, }
9. DepDigger: Detecting Complex Low-Level Dependencies. 2010. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{DepDigger, title = {{{\sc DepDigger}}: Detecting Complex Low-Level Dependencies}, year = {2010}, url = {http://www.sosy-lab.org/~dbeyer/DepDigger/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer, architect, and maintenance}, }
10. Grégory Théoduloz. Software Verification by Combining Program Analyses of Adjustable Precision. PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger, 2010. Keyword(s): BLAST, Software Model Checking PDF
    BibTeX Entry

    @misc{GregoryCPA, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Software Verification by Combining Program Analyses of Adjustable Precision}, year = {2010}, pdf = {https://doi.org/10.5075/epfl-thesis-4781}, keyword = {BLAST,Software Model Checking}, howpublished = {PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger}, }
11. Dmitry Balzer. Werkzeugunterstützung für Verstehen und Monitoring von Software-Abhängigkeiten. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{BalzerDependencies, author = {Dmitry Balzer}, title = {{Werkzeugunterst{\"u}tzung f{\"u}r Verstehen und Monitoring von Software-Abh{\"a}ngigkeiten}}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
12. Alexander von Rhein. Verification Tasks for Software Model Checking. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{AlexQuery, author = {Alexander~von~Rhein}, title = {Verification Tasks for Software Model Checking}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
13. Ashgan Fararooy. Performing Static Structure Analysis using Software Dependencies. Master's Thesis, Simon Fraser University, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{FararooyStructureAnalysis, author = {Ashgan Fararooy}, title = {Performing Static Structure Analysis using Software Dependencies}, year = {2010}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, Simon Fraser University, Software Systems Lab}, }
14. Philipp Wendler. Software Verification based on Adjustable Large-Block Encoding. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{PhilippABE, author = {Philipp Wendler}, title = {Software Verification based on Adjustable Large-Block Encoding}, year = {2010}, pdf = {https://www.sosy-lab.org/research/msc/2010.Wendler.Software_Verification_based_on_Adjustable_Large-Block_Encoding.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
    Additional Infos

    Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis