Publications of year 2010

Articles in conference or workshop proceedings

  1. 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). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    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.

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {80-83},
    year = {2010},
    isbn = {978-0-7695-4113-6},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.A_Simple_and_Effective_Measure_for_Complex_Low-Level_Dependencies.pdf},
    url = {},
    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. },
    
    }
    

  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). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    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.

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {42-43},
    year = {2010},
    isbn = {978-0-7695-4113-6},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.CheckDep_A_Tool_for_Tracking_Software_Dependencies.pdf},
    url = {},
    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. },
    
    }
    

  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). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    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.

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {40-41},
    year = {2010},
    isbn = {978-0-7695-4113-6},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2010-ICPC.DepDigger_A_Tool_for_Detecting_Complex_Low-Level_Dependencies.pdf},
    url = {},
    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. },
    
    }
    

  4. 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. [ PDF ] Keyword(s): Software Model Checking.
    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.

    @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)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {D.S.~Rosenblum and G.~Taentzer},
    series = {LNCS~6013},
    pages = {263-277},
    year = {2010},
    isbn = {978-3-642-12028-2},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2010-FASE.Shape_Refinement_through_Explicit_Heap_Analysis.pdf},
    url = {},
    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. },
    
    }
    

  5. 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. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    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.

    @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)},
    publisher = {FMCAD},
    pages = {189-197},
    year = {2010},
    isbn = {},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2010-FMCAD.Predicate_Abstraction_with_Adjustable-Block_Encoding.pdf},
    url = {http://www.sosy-lab.org/~dbeyer/cpa-abe/},
    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. },
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Philipp Wendler. Software Verification based on Adjustable Large-Block Encoding. Master's Thesis, University of Passau, Software Systems Lab, 2010. [ PDF ]
    @misc{PhilippABE,
    author = {Philipp Wendler},
    title = {Software Verification based on Adjustable Large-Block Encoding},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2010},
    pdf = {https://www.sosy-lab.org/research/msc/2010.Wendler.Software_Verification_based_on_Adjustable_Large-Block_Encoding.pdf},
    awards = {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 industrial association of the region Niederbayern IHK},
    
    }
    

  2. Alexander von Rhein. Verification Tasks for Software Model Checking. Master's Thesis, University of Passau, Software Systems Lab, 2010.
    @misc{AlexQuery,
    author = {Alexander~von~Rhein},
    title = {Verification Tasks for Software Model Checking},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2010},
    
    }
    




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