Publications

2017

  1. Dirk Beyer, Sumit Gulwani, and David Schmidt. Combining Model Checking and Data-Flow Analysis. In E. M. Clarke, T. A. Henzinger, and H. Veith, editors, Handbook on Model Checking. Springer, 2017, to appear. [ PDF ] [bibtex-entry]

  2. Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, and Martin Wirsing. Software-Verifikation. In A. Bode, M. Broy, H.-J. Bungartz, and F. Matthes, editors, 50 Jahre Universitäts-Informatik in München, pages 75-86. Springer, 2017. [bibtex-entry]

  3. Dirk Beyer, Matthias Dangl, and Philipp Wendler. A Unifying View on SMT-Based Software Verification. Journal of Automated Reasoning, 2017. [ Info ] [ PDF ]
    Abstract:
    After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different ``schools of thought'' of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.
    [bibtex-entry]

  4. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer (STTT), 2017. [ Info ] [ PDF ]
    Abstract:
    Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.
    [bibtex-entry]

  5. Pavel Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, and Anton Volkov. CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution). In Axel Legay and Tiziana Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 355--359, 2017. Springer-Verlag, Heidelberg. [ Info ] [bibtex-entry]

  6. Dirk Beyer. Software Verification with Validation of Results (Report on SV-COMP 2017). In Axel Legay and Tiziana Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 331-349, 2017. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] [bibtex-entry]

  7. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Exchanging Verification Witnesses between Verifiers. In J. Jürjens and K. Schneider, editors, Tagungsband Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik (21.-24. Februar 2017, Hannover, Deutschland), LNI P-267, pages 93-94, 2017. GI. [bibtex-entry]

  8. Dirk Beyer and Thomas Lemberger. Software Verification: Testing vs. Model Checking. In Proc. HVC, LNCS, 2017. Springer. [ PDF ] [bibtex-entry]

  9. Deyan Ivanov. Interactive Visualization of Verification Results from CPAchecker with D3. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017. [ PDF ] [bibtex-entry]

  10. Stefan Löwe. Effective Approaches to Abstraction Refinement for Automatic Software Verification. PhD Thesis, University of Passau, Software Systems Lab, 2017. [ Info ] [ PDF ] [bibtex-entry]

  11. Nils Steinger. Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. [ Info ] [ PDF ] [bibtex-entry]

  12. Gernot Zoerneck. Implementing PDR in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. [bibtex-entry]

2016

  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 ] [bibtex-entry]

  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. [bibtex-entry]

  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 ] [bibtex-entry]

  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. [bibtex-entry]

  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 ] [bibtex-entry]

  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 ] [bibtex-entry]

  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. [bibtex-entry]

  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 ] [bibtex-entry]

  9. Dirk Beyer and Thomas Lemberger. Symbolic Execution with CEGAR. In Proc. ISoLA (1), LNCS 9952, pages 195-211, 2016. Springer. [ PDF ] [bibtex-entry]

  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. [bibtex-entry]

  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. [bibtex-entry]

  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. [bibtex-entry]

  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. [bibtex-entry]

  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. [bibtex-entry]

  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. [bibtex-entry]

  16. Stephan Lukasczyk. Unbounded Heap Support for CPAchecker's Predicate Analysis Using SMT Arrays. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ Info ] [bibtex-entry]

  17. Magdalena Murr. Towards Understandable CPAchecker Counterexamples. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ] [bibtex-entry]

  18. Sebastian Ott. Implementing a Termination Analysis using Configurable Software Analysis. Master's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ] [bibtex-entry]

  19. Thomas Stieglmaier. Augmenting Predicate Analysis with Auxiliary Invariants. Master's Thesis, University of Passau, Software Systems Lab, 2016. [ Info ] [ PDF ] [bibtex-entry]

  20. Maximilian Syri. Verification of Concurrent Programs by CFA Sequentialization. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [bibtex-entry]

  21. Stefan Weinzierl. Configurable Pointer-Alias Analysis in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2016. [ PDF ] [bibtex-entry]

2015

  1. Dirk Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In C. Baier and C. Tinelli, editors, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2015, London, UK, April 13-17), LNCS 9035, pages 401-416, 2015. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  2. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. Witness Validation and Stepwise Testification across Software Verifiers. In E. Di Nitto, M. Harman, and P. Heymans, editors, Proceedings of the 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2015, Bergamo, Italy, August 31 - September 4, pages 721-733, 2015. ACM, New York. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  3. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Boosting k-Induction with Continuously-Refined Invariants. In D. Kröning and C. S. Pasareanu, editors, Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015, San Francisco, CA, USA, July 18-24)), LNCS 9206, pages 622-640, 2015. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  4. Dirk Beyer and Stefan Löwe. Interpolation for Value Analysis. In U. Assmann, B. Demuth, T. Spitta, G. Püschel, and R. Kaiser, editors, Tagungsband Software Engineering 2015, Fachtagung des GI-Fachbereichs Softwaretechnik (17. März - 20. März 2015, Dresden, Deutschland), LNI 239, pages 73-74, 2015. GI. [bibtex-entry]

  5. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Benchmarking and Resource Measurement. In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 160-178, 2015. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  6. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Refinement Selection. In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 20-38, 2015. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  7. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. In S. Graf and M. Viswanathan, editors, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015, Grenoble, France, June 2-4), LNCS 9039, pages 228-243, 2015. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  8. Johannes Bürdek, Malte Lochau, Stefan Bauregger, Andreas Holzer, Alexander von Rhein, Sven Apel, and Dirk Beyer. Facilitating Reuse in Multi-Goal Test-Suite Generation for Software Product Lines. In A. Egyed and I. Schaefer, editors, Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015, London, UK, April 13-15), LNCS 9033, pages 84-99, 2015. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  9. Matthias Dangl, Stefan Löwe, and Philipp Wendler. CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution). In C. Baier and C. Tinelli, editors, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2015, London, UK, April 13-17), LNCS 9035, pages 423--425, 2015. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking. [bibtex-entry]

  10. Alexander von Rhein, Alexander Grebhahn, Sven Apel, Norbert Siegmund, Dirk Beyer, and Thorsten Berger. Presence-Condition Simplification in Highly Configurable Systems. In A. Bertolino, G. Canfora, and S. Elbaum, editors, Proceedings of the 37th International Conference on Software Engineering (ICSE 2015, Florence, Italy, May 16-24), pages 178-188, 2015. IEEE. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  11. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Combining k-Induction with Continuously-Refined Invariants. Technical report MIP-1503, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Annotation:
    Online: http://arxiv.org/abs/1502.00096
    [bibtex-entry]

  12. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes. Technical report MIP-1501, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015. [ PDF ] Keyword(s): Software Model Checking.
    Annotation:
    Online: http://arxiv.org/abs/1502.00045
    [bibtex-entry]

  13. Karlheinz Friedberger. Block-Abstraction Memoization as an Approach to Verify Recursive Procedures. Master's Thesis, University of Passau, Software Systems Lab, 2015. [ PDF ] [bibtex-entry]

  14. Thomas Lemberger. Efficient Symbolic Execution using CEGAR over Two Abstract Domains. Bachelor's Thesis, University of Passau, Software Systems Lab, 2015. [ PDF ] [bibtex-entry]

2014

  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 ] [bibtex-entry]

  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 ] [bibtex-entry]

  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 ] [bibtex-entry]

  4. 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.
    [bibtex-entry]

  5. 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.
    [bibtex-entry]

  6. 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 ] [bibtex-entry]

  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. [ 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.
    [bibtex-entry]

  8. 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 ] [bibtex-entry]

  9. 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. [bibtex-entry]

  10. 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 ] [bibtex-entry]

  11. Georg Dresler. A Google-App-Engine Implementation for CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ Info ] [bibtex-entry]

  12. Sebastian Ott. VerifierCloud: Implementierung eines Web-Service zur Software-Verifikation. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ PDF ] [bibtex-entry]

  13. Thomas Stieglmaier. Octagon-Based Software Verification with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2014. [ PDF ] [bibtex-entry]

2013

  1. Dirk Beyer and Michele Boreale, editors. Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (33rd FORTE / 15th FMOODS), LNCS 7892, 2013. Springer-Verlag, Heidelberg. [bibtex-entry]

  2. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Abstract-Domain Selection Based on Variable Usage. In V. Bertacco and A. Legay, editors, Proceedings of the 9th Haifa Verification Conference (HVC 2013, Haifa, Israel, November 5-7), LNCS 8244, pages 262–278, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., `int' and `long') to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.
    [bibtex-entry]

  3. Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Grösslinger, and Dirk Beyer. Strategies for Product-Line Verification: Case Studies and Experiments. In D. Notkin, B. H. C. Cheng, and K. Pohl, editors, Proceedings of the 35th International Conference on Software Engineering (ICSE 2013, San Francisco, CA, USA, May 18-26), pages 482-491, 2013. IEEE. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Product-line technology is increasingly used in mission-critical and safety-critical applications. Hence, researchers are developing verification approaches that follow different strategies to cope with the specific properties of product lines. While the research community is discussing the mutual strengths and weaknesses of the different strategies---mostly at a conceptual level---there is a lack of evidence in terms of case studies, tool implementations, and experiments. We have collected and prepared six product lines as subject systems for experimentation. Furthermore, we have developed a model-checking tool chain for C-based and Java-based product lines, called SPLverifier, which we use to compare sample-based and family-based strategies with regard to verification performance and the ability to find defects. Based on the experimental results and an analytical model, we revisit the discussion of the strengths and weaknesses of product-line--verification strategies.
    [bibtex-entry]

  4. Dirk Beyer. Second Competition on Software Verification (Summary of SV-COMP 2013). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 594-609, 2013. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    This report describes the 2nd International Competition on Software Verification (SV-COMP 2013), which is the second edition of this thorough evaluation of fully automatic verifiers for software programs. The reported results represent the 2012 state-of-the-art in automatic software verification, in terms of effectiveness and efficiency. The benchmark set of verification tasks consists of eleven categories containing a total of 2315 programs, written in C, and exposing features of integers, heap-data structures, bit-vector operations, and concurrency; the properties include reachability and memory safety. The competition is again organized as a satellite event of TACAS.
    [bibtex-entry]

  5. Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith. Information Reuse for Multi-goal Reachability Analyses. In M. Felleisen and P. Gardner, editors, Proceedings of the 22nd European Symposium on Programming (ESOP 2013, Rome, Italy, March 19-22), LNCS 7792, pages 472-491, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for computing complex test suites for large sets of test goals, because each test goal requires an expensive run of the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of sub-automata in a series of reachability queries, we achieve considerable performance improvements over the standard approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL.
    [bibtex-entry]

  6. Dirk Beyer and Stefan Löwe. Explicit-State Software Model Checking Based on CEGAR and Interpolation. In V. Cortellessa and D. Varro, editors, Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE 2013, Rome, Italy, March 20-22), LNCS 7793, pages 146-162, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to explicit-value program analysis. We present an approach that integrates abstraction and interpolation-based refinement into an explicit-value analysis, i.e., a program analysis that tracks explicit values for a specified set of variables (the precision). The algorithm uses an abstract reachability graph as central data structure and a path-sensitive dynamic approach for precision adjustment. We evaluate our algorithm on the benchmark set of the Competition on Software Verification 2012 (SV-COMP'12) to show that our new approach is highly competitive. We also show that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP'12 winner.
    [bibtex-entry]

  7. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse for Efficient Regression Verification. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013, St. Petersburg, Russia, August 18-26), pages 389-399, 2013. ACM. [ PDF ] Keyword(s): Software Model Checking.
    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]

  8. Dirk Beyer and Andreas Stahlbauer. BDD-Based Software Model Checking with CPAchecker. In A. Kucera et al., editor, Proceedings of the Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012, Znojmo, Czech Republic, October 26-28), LNCS 7721, pages 1-11, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  9. Dirk Beyer and Philipp Wendler. Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses. In E. Bartocci and C. R. Ramakrishnan, editors, Proceedings of the 2013 International Symposium on Model Checking of Software (SPIN 2013, Stony Brook, NY, USA, July 8-9), LNCS 7976, pages 1-17, 2013. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and ---with less computational effort--- (re-) verify that the witness is valid.
    [bibtex-entry]

  10. S. Löwe. CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 610-612, 2013. Springer. [ Info ] Keyword(s): Software Model Checking. [bibtex-entry]

  11. P. Wendler. CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 613-615, 2013. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking. [bibtex-entry]

  12. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Selecting Abstractions Based on Variable Usage. Technical report MIP-1303, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.
    Annotation:
    Online: http://arxiv.org/abs/1305.6640
    [bibtex-entry]

  13. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Reusing Precisions for Efficient Regression Verification. Technical report MIP-1302, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. [ PDF ] Keyword(s): Software Model Checking.
    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 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, namely, 59 device drivers with 1119 revisions from the Linux kernel.
    Annotation:
    Online: http://arxiv.org/abs/1305.6915
    [bibtex-entry]

  14. Matthias Dangl. Light-Weight Invariant Generation for Software Verification with CPAchecker. Master's Thesis, University of Passau, Software Systems Lab, 2013. [ PDF ] [bibtex-entry]

  15. Matthias Dittrich. Bit-Precise Predicate Analysis with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2013. [bibtex-entry]

2012

  1. Dirk Beyer, Arie van Deursen, and Michael W. Godfrey, editors. Proceedings of the 20th IEEE International Conference on Program Comprehension, 2012. IEEE. [bibtex-entry]

  2. Dirk Beyer. Competition on Software Verification (SV-COMP). In C. Flanagan and B. König, editors, Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2012, Tallinn, Estonia, March 27-30), LNCS 7214, pages 504--524, 2012. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    This report describes the definitions, rules, setup, procedure, and results of the 1st International Competition on Software Verification. The verification community has performed competitions in various areas in the past, and SV-COMP'12 is the first competition of verification tools that take software programs as input and run a fully automatic verification of a given safety property. This year's competition is organized as a satellite event of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
    [bibtex-entry]

  3. Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. Conditional Model Checking: A Technique to Pass Information between Verifiers. In Tevfik Bultan and Martin Robillard, editors, Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2012, Cary, NC, November 10-17), 2012. ACM. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.
    [bibtex-entry]

  4. Dirk Beyer and Alexander K. Petrenko. Linux Driver Verification. In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part II, Heraklion, Crete, October 15-18), LNCS 7610, pages 1-6, 2012. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  5. Dirk Beyer and Philipp Wendler. Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT. In Gianpiero Cabodi and Satnam Singh, editors, Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22-25), pages 106-113, 2012. FMCAD. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).
    [bibtex-entry]

  6. Falk Howar, Malte Isberner, Maik Merten, Bernhard Steffen, and Dirk Beyer. The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part I, Heraklion, Crete, October 15-18), LNCS 7609, pages 608-614, 2012. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking. [bibtex-entry]

  7. S. Löwe and P. Wendler. CPAchecker with Adjustable Predicate Analysis (Competition Contribution). In C. Flanagan and B. König, editors, Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2012, Tallinn, Estonia, March 27-30), LNCS 7214, pages 528--530, 2012. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking. [bibtex-entry]

  8. Dirk Beyer and Stefan Löwe. Explicit-Value Analysis Based on CEGAR and Interpolation. Technical report MIP-1205, Department of Computer Science and Mathematics (FIM), University of Passau (PA), December 2012. [ PDF ] Keyword(s): Software Model Checking.
    Annotation:
    Online: http://arxiv.org/abs/1212.6542
    [bibtex-entry]

  9. Alexander Driemeyer. Software-Verifikation von Java-Programmen in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. [bibtex-entry]

  10. Karlheinz Friedberger. Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. [ PDF ] [bibtex-entry]

  11. Christopher Jahn. Implementation of a CFA and ARG Visualization and Navigation Tool in Java. Master's Thesis, University of Passau, Software Systems Lab, 2012. [bibtex-entry]

2011

  1. Sven Apel and Dirk Beyer. Feature Cohesion in Software Product Lines: An Exploratory Study. In Proceedings of the 33rd International Conference on Software Engineering (ICSE 2011, Honolulu, HI, May 21-28), pages 421-430, 2011. ACM Press, New York (NY). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Software product lines gain momentum in research and industry. Many product-line approaches use features as a central abstraction mechanism. Feature-oriented software development aims at encapsulating features in cohesive units to support program comprehension, variability, and reuse. Surprisingly, not much is known about the characteristics of cohesion in feature-oriented product lines, although proper cohesion is of special interest in product-line engineering due to its focus on variability and reuse. To fill this gap, we conduct an exploratory study on forty software product lines of different sizes and domains. A distinguishing property of our approach is that we use both classic software measures and novel measures that are based on distances in clustering layouts, which can be used also for visual exploration of product-line architectures. This way, we can draw a holistic picture of feature cohesion. In our exploratory study, we found several interesting correlations (e.g., between development process and feature cohesion) and we discuss insights and perspectives of investigating feature cohesion (e.g., regarding feature interfaces and programming style).
    [bibtex-entry]

  2. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Detection of Feature Interactions using Feature-Aware Verification. In Proceedings of the 26th International Conference on Automated Software Engineering (ASE 2011, Lawrence, KS, November 6-10), pages 372-375, 2011. IEEE. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    A software product line is a set of software products that are distinguished in terms of features (i.e., end-user--visible units of behavior). Feature interactions ---situations in which the combination of features leads to emergent and possibly critical behavior--- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line--verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only local knowledge.
    [bibtex-entry]

  3. Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011, Snowbird, UT, July 14-20), LNCS 6806, pages 184-190, 2011. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results --- we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easy-to-extend platform, and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. CPAchecker implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on software-verification benchmarks from the literature, and compare it with other state-of-the-art model checkers. CPAchecker is an open-source toolkit and publicly available.
    [bibtex-entry]

  4. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Feature-Aware Verification. Technical report MIP-1105, Department of Computer Science and Mathematics (FIM), University of Passau (PA), September 2011. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    A software product line is a set of software products that are distinguished in terms of features (i.e., end-user--visible units of behavior). Feature interactions ---situations in which the combination of features leads to emergent and possibly critical behavior--- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only feature-local knowledge, and that variability encoding significantly improves the verification performance when proving the absence of interactions.
    Annotation:
    Online: http://arxiv.org/abs/1110.0021
    [bibtex-entry]

  5. Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. Conditional Model Checking. Technical report MIP-1107, Department of Computer Science and Mathematics (FIM), University of Passau (PA), September 2011. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before space-out, time-out, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, state-space coverage, and performance.
    Annotation:
    Online: http://arxiv.org/abs/1109.6926
    [bibtex-entry]

2010

  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.
    [bibtex-entry]

  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.
    [bibtex-entry]

  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.
    [bibtex-entry]

  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.
    [bibtex-entry]

  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.
    [bibtex-entry]

  6. Philipp Wendler. Software Verification based on Adjustable Large-Block Encoding. Master's Thesis, University of Passau, Software Systems Lab, 2010. [ PDF ] [bibtex-entry]

  7. Alexander von Rhein. Verification Tasks for Software Model Checking. Master's Thesis, University of Passau, Software Systems Lab, 2010. [bibtex-entry]

2009

  1. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009, Austin, TX, November 15-18), pages 25-32, 2009. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Several successful approaches to software verification are based on the construction and analysis of an abstract reachability tree (ART). The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.
    [bibtex-entry]

  2. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. Technical report SFU-CS-2009-09, School of Computing Science (CMPT), Simon Fraser University (SFU), April 2009. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.
    Annotation:
    Online: http://arxiv.org/abs/0904.4709
    [bibtex-entry]

  3. Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Technical report SFU-CS-2009-02, School of Computing Science (CMPT), Simon Fraser University (SFU), January 2009. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, is required to implement the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. The major design goal during the development was to provide a framework for developers that is flexible and easy to extend. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this platform and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. We evaluate the efficiency of our tool on benchmarks from the software model checker BLAST. The first released version of CPAchecker implements CPAs for predicate abstraction, octagon, and explicit-value domains. Binaries and the source code of CPAchecker are publicly available as free software.
    Annotation:
    Online: http://arxiv.org/abs/0902.0019
    [bibtex-entry]

2008

  1. Dirk Beyer. CCVisu: Automatic Visual Software Decomposition. In Proceedings of the 30th ACM/IEEE International Conference on Software Engineering (ICSE 2008, Leipzig, May 10-18), pages 967-968, 2008. ACM Press, New York (NY). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Understanding the structure of large existing (and evolving) software systems is a major challenge for software engineers. In reverse engineering, we aim to compute, for a given software system, a decomposition of the system into its subsystems. CCVisu is a lightweight tool that takes as input a software graph model and computes a visual representation of the system's structure, i.e., it structures the system into separated groups of artifacts that are strongly related, and places them in a 2- or 3-dimensional space. Besides the decomposition into subsystems, it reveals the relatedness between the subsystems via interpretable distances. The tool reads a software graph from a simple text file in RSF format, e.g., call, inheritance, containment, or co-change graphs. The resulting system structure is currently either directly presented on the screen, or written to an output file in SVG, VRML, or plain text format. The tool is designed as a reusable software component, easy to use, and easy to integrate into other tools; it is based on efficient algorithms and supports several formats for data interchange.
    Annotation:
    ICSE 2008, Leipzig, May 10-18,
    © 2008 ACM
    Online: http://dx.doi.org/10.1145/1370175.1370211
    [bibtex-entry]

  2. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Program Analysis with Dynamic Precision Adjustment. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008, L'Aquila, September 15-19), pages 29-38, 2008. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.
    Annotation:
    ASE 2008, L'Aquila, September 15-19.
    © 2008 IEEE
    Online: http://dx.doi.org/10.1109/ASE.2008.13
    [bibtex-entry]

  3. Dirk Beyer, Damien Zufferey, and Rupak Majumdar. CSIsat: Interpolation for LA+EUF. In A. Gupta and S. Malik, editors, Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008, Princeton, NY, July 7-14), LNCS 5123, pages 304-308, 2008. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    We present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason about the boolean structure. We evaluate the efficiency of our tool on benchmarks from software verification. Binaries and the source code of CSIsat are publicly available as free software.
    Annotation:
    CAV 2008, Princeton (NY), July 7-14,
    Aarti Gupta, Sharad Malik, editors.
    © 2008 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-70545-1_29
    [bibtex-entry]

2007

  1. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), 9(5-6):505-525, 2007. Invited to special issue of selected papers from FASE 2004/05. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs.
    Annotation:
    BLAST is available at: http://www.sosy-lab.org/~dbeyer/Blast
    [bibtex-entry]

  2. Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, and Sanjit A. Seshia. An Application of Web-Service Interfaces. In Proceedings of the 2007 IEEE International Conference on Web Services (ICWS 2007, Salt Lake City, UT, July 9-13), pages 831-838, 2007. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    Abstract:
    We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.
    Annotation:
    Online: http://dx.doi.org/10.1109/ICWS.2007.32
    [bibtex-entry]

  3. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Invariant Synthesis for Combined Theories. In Proceedings of the Eighth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2007, Nice, January 14-16), LNCS 4349, pages 378-394, 2007. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.
    Annotation:
    VMCAI 2007, Nice, January 14-16,
    , editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-69738-1_27
    [bibtex-entry]

  4. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path Invariants. In Proceedings of the 2007 ACM Conference on Programming Language Design and Implementation (PLDI 2007, San Diego, CA, June 10-13), pages 300-309, 2007. ACM Press, New York (NY). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm ---the spurious counterexample--- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs ---so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.
    Annotation:
    PLDI 2007, San Diego, CA, June 10-13,
    © 2007 ACM
    Online: http://dx.doi.org/10.1145/1250734.1250769
    [bibtex-entry]

  5. Dirk Beyer, Thomas A. Henzinger, and Vasu Singh. Algorithms for Interface Synthesis. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007, Berlin, July 3-7), LNCS 4590, pages 4-19, 2007. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Interfaces for Component-Based Design, Software Model Checking.
    Abstract:
    A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries.
    Annotation:
    CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_4
    [bibtex-entry]

  6. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007, Berlin, July 3-7), LNCS 4590, pages 504-518, 2007. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.
    Annotation:
    CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_51
    [bibtex-entry]

  7. Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger. An Interface Formalism for Web Services. Technical report MTC-REPORT-2007-002, School of Computer and Communication Sciences (IC), Ecole Polytechnique Fédérale de Lausanne (EPFL), December 2007. [ Info ] [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    Abstract:
    Web application development using distributed components and web services presents new software integration challenges, because solutions often cross vendor, administrative, and other boundaries across which neither binary nor source code can be shared. We present a methodology that addresses this problem through a formalism for specifying and manipulating behavioral interfaces of multi-threaded open software components that communicate with each other through method calls. An interface constrains both the implementation and the user of a web service to fulfill certain assumptions that are specified by the interface. Our methodology consists of three increasingly expressive classes of interfaces. Signature interfaces specify the methods that can be invoked by the user, together with parameters. Consistency interfaces add propositional constraints, enhancing signature interfaces with the ability to specify choice and causality. Protocol interfaces specify, in addition, temporal ordering constraints on method invocations. We provide approaches to check if two or more interfaces are compatible; if a web service can be safely substituted for another one; and if a web service satisfies a specification that represents a desired behavioral property.
    Annotation:
    A preliminary version of this paper was presented at the First International Workshop on Foundations of Interface Technologies (FIT 2005, San Francisco, CA, August 21).
    Online: http://infoscience.epfl.ch/search?recid=114605&ln=en
    [bibtex-entry]

2006

  1. Basil Becker, Dirk Beyer, Holger Giese, Florian Klein, and Daniela Schilling. Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE 2006, Shanghai, May 20-28), pages 72-81, 2006. ACM Press, New York (NY). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The next generation of networked mechatronic systems will be characterized by complex coordination and structural adaptation at run-time. Crucial safety properties have to be guaranteed for all potential structural configurations. Testing cannot provide safety guarantees, while current model checking and theorem proving techniques do not scale for such systems. We present a verification technique for arbitrarily large multi-agent systems from the mechatronic domain, featuring complex coordination and structural adaptation. We overcome the limitations of existing techniques by exploiting the local character of structural safety properties. The system state is modeled as a graph, system transitions are modeled as rule applications in a graph transformation system, and safety properties of the system are encoded as inductive invariants (permitting the verification of infinite state systems). We developed a symbolic verification procedure that allows us to perform the computation on an efficient BDD-based graph manipulation engine, and we report performance results for several examples.
    Annotation:
    ICSE 2006, Shanghai, May 20-28,
    © 2006 ACM
    Online: http://dx.doi.org/10.1145/1134297
    [bibtex-entry]

  2. Dirk Beyer. Co-Change Visualization Applied to PostgreSQL and ArgoUML. In Proceedings of the Third International Workshop on Mining Software Repositories (MSR 2006, Shanghai, May 22-23), pages 165-166, 2006. ACM Press. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Co-change visualization is a method to recover the subsystem structure of a software system from the version history, based on common changes and visual clustering. This paper presents the results of applying the tool CCVisu, which implements co-change visualization, to the two open-source software systems PostgreSQL and ArgoUML. The input of the method is the co-change graph, which can be easily extracted by CCVisu from a CVS version repository. The output is a graph layout that places software artifacts that were often commonly changed at close positions, and artifacts that were rarely co-changed at distant positions. This property of the layout is due to the clustering property of the underlying energy model, which evaluates the quality of a produced layout. The layout can be displayed on the screen, or saved to a file in SVG or VRML format.
    [bibtex-entry]

  3. Dirk Beyer. Relational Programming with CrocoPat. In Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE 2006, Shanghai, May 20-28), pages 807-810, 2006. ACM Press, New York (NY). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Many structural analyses of software systems are naturally formalized as relational queries, for example, the detection of design patterns, patterns of problematic design, code clones, dead code, and differences between the as-built and the as-designed architecture. This paper describes CrocoPat, an application-independent tool for relational programming. Through its efficiency and its expressive language, CrocoPat enables practically important analyses of real-world software systems that are not possible with other graph analysis tools, in particular analyses that involve transitive closures and the detection of patterns in graphs. The language is easy to use, because it is based on the well-known first-order predicate logic. The tool is easy to integrate into other software systems, because it is a small command-line tool that uses a simple text format for input and output of relations.
    Annotation:
    ICSE 2006, Shanghai, May 20-28,
    © 2006 ACM
    CrocoPat is available at: http://www.sosy-lab.org/~dbeyer/CrocoPat/
    [bibtex-entry]

  4. Dirk Beyer and Ahmed E. Hassan. Animated Visualization of Software History using Evolution Storyboards. In Proceedings of the 13th IEEE Working Conference on Reverse Engineering (WCRE 2006, Benevento, October 23-27), pages 199-208, 2006. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    The understanding of the structure of a software system can be improved by analyzing the system's evolution during development. Visualizations of software history that provide only static views do not capture the dynamic nature of software evolution. We present a new visualization technique, the Evolution Storyboard, which provides dynamic views of the evolution of a software's structure. An evolution storyboard consists of a sequence of animated panels, which highlight the structural changes in the system; one panel for each considered time period. Using storyboards, engineers can spot good design, signs of structural decay, or the spread of cross cutting concerns in the code. We implemented our concepts in a tool, which automatically extracts software dependency graphs from version control repositories and computes storyboards based on panels for different time periods. For applying our approach in practice, we provide a step by step guide that others can follow along the storyboard visualizations, in order to study the evolution of large systems. We have applied our method to several large open source software systems. In this paper, we demonstrate that our method provides additional information (compared to static views) on the ArgoUML project, an open source UML modeling tool.
    Annotation:
    Online: http://dx.doi.org/10.1109/WCRE.2006.14
    [bibtex-entry]

  5. Dirk Beyer and Ahmed E. Hassan. Evolution Storyboards: Visualization of Software Structure Dynamics. In Proceedings of the 14th IEEE International Conference on Program Comprehension (ICPC 2006, Athens, June 14-16), pages 248-251, 2006. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Large software systems have a rich development history. Mining certain aspects of this rich history can reveal interesting insights into the system and its structure. Previous approaches to visualize the evolution of software systems provide static views. These static views often do not fully capture the dynamic nature of evolution. We introduce the Evolution Storyboard, a visualization which provides dynamic views of the evolution of a software's structure. Our tool implementation takes as input a series of software graphs, e.g., call graphs or co-change graphs, and automatically generates an evolution storyboard. To illustrate the concept, we present a storyboard for PostgreSQL, as a representative example for large open source systems. Evolution storyboards help to understand a system's structure and to reveal its possible decay over time. The storyboard highlights important changes in the structure during the lifetime of a software system, and how artifacts changed their dependencies over time.
    Annotation:
    Online: http://dx.doi.org/10.1109/ICPC.2006.21
    [bibtex-entry]

  6. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In T. Ball and R.B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006, Seattle, WA, August 17-20), LNCS 4144, pages 532-546, 2006. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.
    Annotation:
    CAV 2006, Seattle, WA, August 17-20,
    Thomas Ball, Robert B. Jones, editors.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/11817963_48
    An extended version of this paper appeared in Proc. Dagstuhl Seminar 06081, IBFI Schloss Dagstuhl, 2006:
    http://drops.dagstuhl.de/portals/06081/
    Supplementary material: http://www.sosy-lab.org/~dbeyer/blast_sa/
    [bibtex-entry]

  7. Alain Wegmann, Lam-Son Le, Lotfi Hussami, and Dirk Beyer. A Tool for Verified Design using Alloy for Specification and CrocoPat for Verification. In D. Jackson and P. Zave, editors, Proceedings of the First Alloy Workshop (ALLOY 2006, Portland, OR, November 6), 2006. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    The context of our work is a project that focuses on methods and tools for modeling enterprise architectures. An enterprise architecture model represents the structure of an enterprise across multiple levels, from the markets in which it operates down to the implementation of the technical systems that support its operation. These models are based on an ontology that defines the model elements and their relations. In this paper, we describe an efficient method to fully automatically verify the design that our modeling tool manages. We specify the ontology in Alloy, and use the efficient interpreter for relational programs CrocoPat to verify that the design fulfills all constraints specified in the ontology. Technically, we transform all constraints from Alloy into a relational program in CrocoPat's programming language. Then, we execute the relational program and feed it with a relational representation of the design as input, in order to check that the design element instances fulfill all constraints of the Alloy representation of the ontology. We also present the current limitations of our approach and how -by overcoming these limitations- we can develop an Alloy-based parameterized modeling tool.
    [bibtex-entry]

  8. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path Invariants. Technical report MTC-REPORT-2006-003, School of Computer and Communication Sciences (IC), Ecole Polytechnique Fédérale de Lausanne (EPFL), December 2006. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In such schemes, the cause of a false positive is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false positive ---the ``spurious counterexample''--- as a full-fledged program, whose control-flow graph may contain loops of the original program and represent unbounded computations. The advantages of using such path programs as counterexamples for abstraction refinement are twofold. First, we can bring the whole machinery of program analysis to bear on path programs: specifically, we use abstract interpretation in the form of constrained-based invariant generation to automatically infer invariants of path programs ---so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but to remove at once all infeasible error computations that are represented by a path program. Unlike predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive invariants.
    Annotation:
    Online: http://infoscience.epfl.ch/search.py?recid=98452&ln=en
    [bibtex-entry]

  9. Dirk Beyer, Thomas A. Henzinger, and Vasu Singh. Three Algorithms for Interface Synthesis: A Comparative Study. Technical report MTC-REPORT-2006-001, School of Computer and Communication Sciences (IC), Ecole Polytechnique Fédérale de Lausanne (EPFL), May 2006. [ Info ] [ PDF ] Keyword(s): Interfaces for Component-Based Design, Software Model Checking.
    Abstract:
    A temporal interface for a system component is a finite automaton that specifies the legal sequences of input events. We evaluate and compare three different algorithms for automatically extracting the temporal interface from the transition graph of a component: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the component to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant state information from the component. Since algorithms (2) and (3) have been published in different software contexts, for comparison purposes, we present the three algorithms in a uniform finite-state setting. We furthermore extend the three algorithms to construct maximally permissive interface automata, which accept all legal input sequences. While the three algorithms have similar worst-case complexities, their actual running times differ greatly depending on the component whose interface is computed. On the theoretical side, we provide families of components that exhibit exponential differences in the performance of the three algorithms. On the practical side, we evaluate the three algorithms experimentally on a variety of real world examples. Not surprisingly, the experimental evaluation confirms the theoretical expectation: learning performs best if the minimal interface automaton is small; CEGAR performs best if only few component variables are needed to prove an interface hypothesis safe and permissive; and the direct (game) algorithm outperforms both approaches if neither is the case.
    Annotation:
    Online: http://infoscience.epfl.ch/search.py?recid=85675&ln=en
    [bibtex-entry]

2005

  1. Dirk Beyer, Andreas Noack, and Claus Lewerentz. Efficient Relational Calculation for Software Analysis. IEEE Transactions on Software Engineering (TSE), 31(2):137-149, 2005. Invited to special issue of selected papers from WCRE 2003. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Calculating with graphs and relations has many applications in the analysis of software systems, for example, the detection of design patterns or patterns of problematic design and the computation of design metrics. These applications require an expressive query language, in particular, for the detection of graph patterns, and an efficient evaluation of the queries even for large graphs. In this paper, we introduce RML, a simple language for querying and manipulating relations based on predicate calculus, and CrocoPat, an interpreter for RML programs. RML is general because it enables the manipulation not only of graphs (i.e., binary relations), but of relations of arbitrary arity. CrocoPat executes RML programs efficiently because it internally represents relations as binary decision diagrams, a data structure that is well-known as a compact representation of large relations in computer-aided verification. We evaluate RML by giving example programs for several software analyses and CrocoPat by comparing its performance with calculators for binary relations, a Prolog system, and a relational database management system.
    Annotation:
    Also available as postprint at the eScholarship Repository, University of California:
    http://repositories.cdlib.org/postprints/687
    Online: http://dx.doi.org/10.1109/TSE.2005.23
    CrocoPat is available at: http://www.sosy-lab.org/~dbeyer/CrocoPat
    [bibtex-entry]

  2. Dirk Beyer. Co-Change Visualization. In Proceedings of the 21st IEEE International Conference on Software Maintenance (ICSM 2005, Budapest, September 25-30), Industrial and Tool volume, Budapest, pages 89-92, 2005. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Clustering layouts of software systems combine two important aspects: they reveal groups of related artifacts of the software system, and they produce a visualization of the results that is easy to understand. Co-change visualization is a lightweight method for computing clustering layouts of software systems for which the change history is available. This paper describes CCVisu, a tool that implements co-change visualization. It extracts the co-change graph from a version repository, and computes a layout, which positions the artifacts of the software system in a two- or three-dimensional space. Two artifacts are positioned closed together in the layout if they were often changed together. The tool is designed as a framework, easy to use, and easy to integrate into reengineering environments; several formats for data interchange are already implemented. The graph layout is currently provided in VRML format, in a standard text format, or directly drawn on the screen.
    Annotation:
    ICSM 2005, Budapest, September 25-30
    Tool Paper
    CCVisu is available at: http://www.sosy-lab.org/~dbeyer/CCVisu
    [bibtex-entry]

  3. Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger. An Interface Formalism for Web Services. In Proceedings of the First International Workshop on Foundations of Interface Technologies (FIT 2005, San Francisco, CA, August 21), 2005. [ Info ] [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    Abstract:
    Web application development using distributed components and web services presents new software integration challenges, because solutions often cross vendor, administrative, and other boundaries across which neither binary nor source code can be shared. We present a methodology that addresses this problem through a formalism for specifying and manipulating behavioral interfaces of multi-threaded open software components that communicate with each other through method calls. An interface constrains both the implementation and the user of a web service to fulfill certain assumptions that are specified by the interface. Our methodology consists of three increasingly expressive classes of interfaces. Signature interfaces specify the methods that can be invoked by the user, together with parameters. Consistency interfaces add propositional constraints, enhancing signature interfaces with the ability to specify choice and causality. Protocol interfaces specify, in addition, temporal ordering constraints on method invocations. We provide approaches to check if two or more interfaces are compatible; if a web service can be safely substituted for another one; and if a web service satisfies a specification that represents a desired behavioral property.
    Annotation:
    FIT 2005, San Francisco, CA, August 21
    [bibtex-entry]

  4. Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger. Web Service Interfaces. In Proceedings of the 14th ACM International World Wide Web Conference (WWW 2005, Chiba, May 10-14), pages 148-159, 2005. ACM Press, New York (NY). [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    Abstract:
    We present a language for specifying web service interfaces. A web service interface puts three kinds of constraints on the users of the service. First, the interface specifies the methods that can be called by a client, together with types of input and output parameters; these are called signature constraints. Second, the interface may specify propositional constraints on method calls and output values that may occur in a web service conversation; these are called consistency constraints. Third, the interface may specify temporal constraints on the ordering of method calls; these are called protocol constraints. The interfaces can be used to check, first, if two or more web services are compatible, and second, if a web service A can be safely substituted for a web service B. The algorithm for compatibility checking verifies that two or more interfaces fulfill each others' constraints. The algorithm for substitutivity checking verifies that service A demands fewer and fulfills more constraints than service B.
    Annotation:
    WWW 2005, Chiba, Japan, May 10-14,
    © 2006 ACM
    Online: http://dx.doi.org/10.1145/1060745.1060770
    [bibtex-entry]

  5. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Checking Memory Safety with Blast. In M. Cerioli, editor, Proceedings of the Eighth International Conference on Fundamental Approaches to Software Engineering (FASE 2005, Edinburgh, April 2-10), LNCS 3442, pages 2-18, 2005. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use CCured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by CCured and provide useful information to the programmer about many of the remaining checks.
    Annotation:
    FASE 2005, Edinburgh, April 2-10,
    Maura Cerioli, editor.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/b107062
    [bibtex-entry]

  6. Dirk Beyer and Andreas Noack. Clustering Software Artifacts Based on Frequent Common Changes. In Proceedings of the 13th IEEE International Workshop on Program Comprehension (IWPC 2005, St. Louis, MO, May 15-16), pages 259-268, 2005. IEEE Computer Society Press, Los Alamitos (CA). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Changes of software systems are less expensive and less error-prone if they affect only one subsystem. Thus, clusters of artifacts that are frequently changed together are subsystem candidates. We introduce a two-step method for identifying such clusters. First, a model of common changes of software artifacts, called co-change graph, is extracted from the version control repository of the software system. Second, a layout of the co-change graph is computed that reveals clusters of frequently co-changed artifacts. We derive requirements for such layouts, and introduce an energy model for producing layouts that fulfill these requirements. We evaluate the method by applying it to three example systems, and comparing the resulting layouts to authoritative decompositions.
    Annotation:
    IWPC 2005, St. Louis, MO, May 15-16
    Online: http://dx.doi.org/10.1109/WPC.2005.12
    Supplementary material: http://www.sosy-lab.org/~dbeyer/co-change/
    [bibtex-entry]

  7. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. Technical report MTC-REPORT-2005-006, School of Computer and Communication Sciences (IC), Ecole Polytechnique Fédérale de Lausanne (EPFL), December 2005. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Many software model checkers are based on predicate abstraction. Values of variables in branching conditions are represented abstractly using predicates. The strength of this approach is its path-sensitive nature. However, if the control flow depends heavily on the values of memory cells on the heap, the approach does not work well, because it is difficult to find `good' predicate abstractions to represent the heap. In contrast, shape analysis can lead to a very compact representation of data structures stored on the heap. In this paper, we combine shape analysis with predicate abstraction, and integrate it into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that shapes are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to shapes. This approach does not only increase the precision of model checking and shape analysis taken individually, but also increases the efficiency of shape analysis (we do not compute shapes where not necessary). We implemented the technique by extending BLAST with calls to TVLA, and evaluated it on several C programs manipulating data structures, with the result that the combined tool can now automatically verify programs that are not verifiable using either shape analysis or predicate abstraction on its own.
    Annotation:
    Online: http://infoscience.epfl.ch/search.py?recid=63789&ln=en
    [bibtex-entry]

  8. Dirk Beyer and Andreas Noack. Mining Co-Change Clusters from Version Repositories. Technical report IC/2005/003, School of Computer and Communication Sciences (IC), Ecole Polytechnique Fédérale de Lausanne (EPFL), January 2005. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Clusters of software artifacts that are frequently changed together are subsystem candidates, because one of the main goals of software design is to make changes local. The contribution of this paper is a visualization-based method that supports the identification of such clusters. First, we define the co-change graph as a simple but powerful model of common changes of software artifacts, and describe how to extract the graph from version control repositories. Second, we introduce an energy model for computing force-directed layouts of co-change graphs. The resulting layouts have a well-defined interpretation in terms of the structure of the visualized graph, and clearly reveal groups of frequently co-changed artifacts. We evaluate our method by comparing the layouts for three example projects with authoritative subsystem decompositions.
    Annotation:
    Online: http://infoscience.epfl.ch/record/52706
    [bibtex-entry]

2004

  1. Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Generating Tests from Counterexamples. In Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE 2004, Edinburgh, May 26-28), pages 326-335, 2004. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).
    Annotation:
    Online: http://dx.doi.org/10.1109/ICSE.2004.1317455
    [bibtex-entry]

  2. Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Blast Query Language for Software Verification. In R. Giacobazzi, editor, Proceedings of the 11th International Static Analysis Symposium (SAS 2004, Verona, August 26-28), LNCS 3148, pages 2-18, 2004. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    BLAST is an automatic verification tool for checking temporal safety properties of C programs. BLAST is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the BLAST specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications.
    Annotation:
    SAS 2004, Verona, August 26-28,
    Roberto Giacobazzi, editor.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/b99688
    [bibtex-entry]

  3. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. An Eclipse Plug-in for Model Checking. In Proceedings of the 12th IEEE International Workshop on Program Comprehension (IWPC 2004, Bari, June 24-26), pages 251-255, 2004. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems --assertion checking, reachability analysis, dead code analysis, and test generation-- directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code.
    Annotation:
    IWPC 2004, Bari, June 24-26
    Online: http://dx.doi.org/10.1109/WPC.2004.1311069
    [bibtex-entry]

  4. Dirk Beyer and Andreas Noack. CrocoPat 2.1 Introduction and Reference Manual. Technical report UCB//CSD-04-1338, Computer Science Division (EECS), University of California, Berkeley, July 2004.
    Also: The Computing Research Repository (CoRR), cs.PL/0409009, September 2004. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    CrocoPat is an efficient, powerful and easy-to-use tool for manipulating relations of arbitrary arity, including directed graphs. This manual provides an introduction to and a reference for CrocoPat and its programming language RML. It includes several application examples, in particular from the analysis of structural models of software systems.
    Annotation:
    Online: http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338
    ArXiv archive: http://arxiv.org/abs/cs/0409009
    A tutorial and user's guide for CrocoPat, defines and explains the syntax and semantics of the extended language.
    CrocoPat is available at: http://www.sosy-lab.org/~dbeyer/CrocoPat/
    [bibtex-entry]

2003

  1. Dirk Beyer and Claus Lewerentz. CrocoPat: Efficient Pattern Analysis in Object-Oriented Programs. In Proceedings of the 11th IEEE International Workshop on Program Comprehension (IWPC 2003, Portland, OR, May 10-11), pages 294-295, 2003. IEEE Computer Society Press, Los Alamitos (CA). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Automatic pattern-based recognition of design weakness is a research topic since almost 10 years. Reports about experiments with existing approaches reveal two major problems: A notation for easy and flexible specification of the pattern is missing; only a restricted set of patterns is applicable because of the limitations of the specification language. Performance improvement is needed, because the computation time of existing tools is to high to be acceptable for large real-world systems.
    The tool CrocoPat satisfies the following three requirements: (1) The analysis is done automatically by the tool, i.e. without user interaction. (2) The properties of a system are specified in an easy and flexible way because the patterns are described by relational expressions. On demand the user is able to define new patterns he is interested in, or to change existing patterns to solve specific problems. (3) The tool is able to analyze large object-oriented programs (1'000 to 10'000~classes) in acceptable time.
    Annotation:
    IWPC 2003, Portland, OR, May 10-11
    Introduction of a BDD-based tool for pattern analysis and a short overview of the main features of CrocoPat.
    [bibtex-entry]

  2. Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In W. A. Hunt and F. Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003, Boulder, CO, July 8-12), LNCS 2725, pages 122-125, 2003. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    This paper gives a short overview of a model checking tool for real-time systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data structure BDD. Good variable orderings for the BDDs are computed from the modular structure of the model and an estimate of the BDD size. This leads to a significant performance improvement compared to the tool RED and the BDD-based version of Kronos.
    Annotation:
    CAV 2003, Boulder, CO, July 8-12,
    Warren A. Hunt Jr., Fabio Somenzi, editors.
    © 2006 Springer-Verlag
    Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122
    A description of the BDD-based tool's main features.
    [bibtex-entry]

  3. Dirk Beyer and Andreas Noack. Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?. In H. König, M. Heiner, and A. Wolisz, editors, Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003, Berlin, September 29 - October 2), LNCS 2767, pages 193-208, 2003. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present analytical and empirical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. This is the first evidence that CDDs can grow only polynomially for models with non-trivial state space explosion. Secondly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-size CDDs if they use better variable orders, as the BDD-based tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values.
    Annotation:
    FORTE 2003, Berlin, September 29 - October 2
    Hartmut König, Monika Heiner, Adam Wolisz, editors.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/11965
    Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols.
    [bibtex-entry]

  4. Dirk Beyer, Andreas Noack, and Claus Lewerentz. Simple and Efficient Relational Querying of Software Structures. In Proceedings of the Tenth IEEE Working Conference on Reverse Engineering (WCRE 2003, Victoria, BC, November 13-16), pages 216-225, 2003. IEEE Computer Society Press, Los Alamitos (CA). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Many analyses of software systems can be formalized as relational queries, for example the detection of design patterns, of patterns of problematic design, of code clones, of dead code, and of differences between the as-built and the as-designed architecture. This paper describes the concepts of CrocoPat, a tool for querying and manipulating relations. CrocoPat is easy to use, because of its simple query and manipulation language based on predicate calculus, and its simple file format for relations. CrocoPat is efficient, because it internally represents relations as binary decision diagrams, a data structure that is well-known as a compact representation of large relations in computer-aided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but n-ary relations.
    Annotation:
    WCRE 2003, Victoria, BC, November 13-16
    CrocoPat's concepts, an introduction to the BDD-based implementation, software analysis applications, and performance measurements.
    Online: http://dx.doi.org/10.1109/WCRE.2003.1287252
    [bibtex-entry]

  5. Dirk Beyer and Claus Lewerentz. CrocoPat: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs. Technical report I-04/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Annotation:
    See WCRE03 [27] for proceedings version.
    [bibtex-entry]

  6. Dirk Beyer and Andreas Noack. A Comparative Study of Decision Diagrams for Real-Time Verification. Technical report I-03/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See FORTE03 [26] for proceedings version.
    [bibtex-entry]

2002

  1. Dirk Beyer. Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata. Mensch & Buch Verlag, Berlin, 2002.
    Also: Dissertation, Brandenburgische Technische Universität Cottbus, 2002. [ Info ] [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    The construction of embedded systems which have to fulfill hard real-time requirements is becoming more and more important in various application areas, e. g. in medicine, in transport technology, or in production automation. Formal methods support the development of faultless systems because they use a precise mathematical basis. The author developed a suitable modelling formalism and efficient verification methods to enable the application of a formal method. Due to the module concept introduced in the thesis, the modelling of large systems is supported systematically. For the verification efficient BDD-based algorithms are used, and the problem of finding good BDD variable orderings is solved. Reachability analysis as well as refinement checking are provided. The practicability of the approaches for modelling and verification is demonstrated by presenting various case studies from the application areas of reactive systems and protocol engineering.
    Annotation:
    ISBN: 3-89820-450-2
    BTU version: Dissertation
    Also as abstract: Softwaretechnik-Trends, Gesellschaft für Informatik, Berlin, 23(2):4, May 2003. (ISSN 0720-8928)
    Dissertation, describes all important concepts and details of the Rabbit project in German.
    [bibtex-entry]

2001

  1. Dirk Beyer. Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs. In T. Margaria and T. F. Melham, editors, Proceedings of the 11th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2001, Livingston, September 4-7), LNCS 2144, pages 86-91, 2001. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    For the formal specification and verification of real-time systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrix-based algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDD-based version of Rabbit, which supports also refinement checking, is now available.
    Annotation:
    CHARME 2001, Livingston, September 4-7,
    Tiziana Margaria, Tom Melham, editors.
    © 2006 Springer-Verlag
    Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
    Decribes how the tool checks refinement via simulation relation.
    [bibtex-entry]

  2. Dirk Beyer. Improvements in BDD-Based Reachability Analysis of Timed Automata. In J. N. Oliveira and P. Zave, editors, Proceedings of the Tenth International Symposium of Formal Methods Europe (FME 2001, Berlin, March 12-16): Formal Methods for Increasing Software Productivity, LNCS 2021, pages 318-343, 2001. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    To develop efficient algorithms for the reachability analysis of timed automata, a promising approach is to use binary decision diagrams (BDDs) as data structure for the representation of the explored state space. The size of a BDD is very sensitive to the ordering of the variables. We use the communication structure to deduce an estimation for the BDD size. In our experiments, this guides the choice of good variable orderings, which leads to an efficient reachability analysis. We develop a discrete semantics for closed timed automata to get a finite state space required by the BDD-based representation and we prove the equivalence to the continuous semantics regarding the set of reachable locations. An upper bound for the size of the BDD representing the transition relation and an estimation for the set of reachable configurations based on the communication structure is given. We implemented these concepts in the verification tool Rabbit [BR00]. Different case studies justify our conjecture: Polynomial reachability analysis seems to be possible for some classes of real-time models, which have a good-natured communication structure.
    Annotation:
    FME 2001, Berlin, March 12-16,
    Jose Nuno Oliveira, Pamela Zave, editors.
    © 2006 Springer-Verlag
    Online: http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm
    Discretization of Timed Automata, BDD-based representation, proof of an upper bound for the BDD of the transition relation, BDD variable ordering, heuristics for efficient verification, contains the proof of the equivalence of our integer semantics to the continuous semantics regarding reachable locations.
    [bibtex-entry]

  3. Dirk Beyer. Rabbit: Verification of Real-Time Systems. In P. Pettersson and S. Yovine, editors, Proceedings of the Workshop on Real-Time Tools (RT-TOOLS 2001, Aalborg, August 20), Uppsala, pages 13-21, 2001. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    This paper gives a short overview of a model checking tool for Cottbus Timed Automata, which is a modular modeling language based on timed and hybrid automata. For timed automata, the current version of the tool provides BDD-based verification using an integer semantics. Reachability analysis as well as refinement checking is possible. To find good variable orderings it uses the component structure of the model and an upper bound for the BDD size. For hybrid automata, reachability analysis based on the double description method is implemented.
    Annotation:
    RT-TOOLS 2001, Aalborg, August 20
    Paul Pettersson, Sergio Yovine, editors
    [bibtex-entry]

  4. Dirk Beyer and Andy Heinig. Different Strategies for BDD-Based Reachability Analysis of Timed Automata. In C. Rattray, M. Sveda, and J. Rozenblit, editors, Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 89-98, 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    FSCBS 2001, Washington, D.C., April 20
    Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors
    [bibtex-entry]

  5. Dirk Beyer, Claus Lewerentz, and Frank Simon. Impact of Inheritance on Metrics for Size, Coupling, and Cohesion in Object Oriented Systems. In R. Dumke and A. Abran, editors, Proceedings of the Tenth International Workshop on Software Measurement (IWSM 2000, Berlin, October 4-6): New Approaches in Software Measurement, LNCS 2006, pages 1-17, 2001. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    In today's engineering of object oriented systems many different metrics are used to get feedback about design quality and to automatically identify design weaknesses. While the concept of inheritance is covered by special inheritance metrics its impact on other classical metrics (like size, coupling or cohesion metrics) is not considered; this can yield misleading measurement values and false interpretations. In this paper we present an approach to work the concept of inheritance into classical metrics (and with it the related concepts of overriding, overloading and polymorphism). This is done by some language dependent flattening functions that modify the data on which the measurement will be done. These functions are implemented within our metrics tool Crocodile and are applied for a case study: the comparison of the measurement values of the original data with the measurement values of the flattened data yields interesting results and improves the power of classical measurements for interpretation.
    Annotation:
    Online: http://link.springer.de/link/service/series/0558/bibs/2006/20060001.htm
    [bibtex-entry]

  6. Dirk Beyer and Andreas Noack. Efficient Verification of Timed Automata using BDDs. In S. Gnesi and U. Ultes-Nitsche, editors, Proceedings of the Sixth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2001, Paris, July 16-17), pages 95-113, 2001. INRIA, Paris. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    This paper investigates the efficient reachability analysis of timed automata. It describes a discretization of time which preserves the reachability properties. The discretization allows to represent sets of configurations of timed automata as binary decision diagrams (BDDs). Further techniques, like computing good variable orderings, are applied to use the full potential of BDDs as compact and canonical representation of large sets. We implemented these concepts within the tool Rabbit. The highly improved performance is shown for some example models. For additional speedup we used an on-the-fly algorithm and refinement checking for large models.
    Annotation:
    FMICS 2001, Paris, July 16-17
    Stefania Gnesi, Ulrich Ultes-Nitsche, editors
    [bibtex-entry]

  7. Dirk Beyer and Heinrich Rust. Cottbus Timed Automata: Formal Definition and Semantics. In C. Rattray, M. Sveda, and J. Rozenblit, editors, Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 75-87, 2001. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    We present a formalism for modular modelling of hybrid systems, the Cottbus Timed Automata. For the theoretical basis, we build on work about timed and hybrid automata. We use concepts from concurrency theory to model communication of separately defined modules, but we extend these concepts to be able to express explicitly read- and write-access to signals and variables.
    Annotation:
    FSCBS 2001, Washington, D.C., April 20
    Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors
    The pdf is a revised version of the original paper.
    The full formal definition and semantics of CTA.
    [bibtex-entry]

  8. Dirk Beyer. Rabbit: Verification of Real-Time Systems. Technical report I-05/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, March 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See CAV03 [25] for proceedings version.
    [bibtex-entry]

  9. Dirk Beyer. Reachability Analysis and Refinement Checking for BDD-Based Model Checking of Timed Automata. Technical report I-04/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, February 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See CHARME01 [20] for proceedings version.
    [bibtex-entry]

2000

  1. Dirk Beyer, Claus Lewerentz, and Heinrich Rust. Modelling and Analysing a Railroad Crossing in a Modular Way. In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of the Fifth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000, Berlin, April 3-4), Berlin, pages 287-303, 2000. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    One problem of modelling hybrid systems with existing notations of hybrid automata is that there is no modular structure in the model. We introduce an extended modelling notation which allows the modelling of a system as a hierarchical structure of modules. The modules are capable of communicating through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes a model of the railroad crossing example and how to verify it. The current version of a tool for reachability analysis using the double description method to represent symbolically the sets of reachable configurations is presented.
    Annotation:
    FMICS 2000, Berlin, April 3-4
    Stefania Gnesi, Ina Schieferdecker, Axel Rennoch, editors
    Describes a case study for modeling and analysis using the DDM-based representation.
    [bibtex-entry]

  2. Dirk Beyer and Andreas Noack. BDD-basierte Verifikation von Realzeit-Systemen. In J. Grabowski and S. Heymer, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 2000, Lübeck, June 22-23), pages 79-89, 2000. Shaker Verlag, Aachen. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    Diese Arbeit behandelt die effiziente Erreichbarkeitsanalyse von Timed Automata. Wir beschreiben eine Erreichbarkeitseigenschaften erhaltende Diskretisierung der Zeit. Diese ermöglicht es, Konfigurationsmengen von Timed Automata als Binary Decision Diagrams (BDDs) darzustellen. Die kompakte BDD-Repräsentation großer Mengen erfordert geeignete Variablenordnungen. Zur deren Bestimmung nutzen wir Strukturinformationen aus der Modellierungsnotation Cottbus Timed Automaton. Wir belegen die erzielten Effizienzverbesserungen durch Meßwerte.
    Annotation:
    FBT 2000, Lübeck, June 22-23
    Jens Grabowski, Stefan Heymer, editors
    [bibtex-entry]

  3. Dirk Beyer and Heinrich Rust. A Tool for Modular Modelling and Verification of Hybrid Systems. In A. Crespo and J. Vila, editors, Proceedings of the 25th IFAC/IFIP Workshop on Real-Time Programming (WRTP 2000, Palma, May 17-19), pages 169-174, 2000. Elsevier Science, Oxford. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    WRTP 2000, Palma, May 17-19
    Alfons Crespo, Joan Vila, editors
    annote = { }, Also as preprint: Proc. WRTP'00, pages 181-186, Valencia, 2000.
    The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.
    [bibtex-entry]

  4. Dirk Beyer and Heinrich Rust. Modular Modelling and Verification with Cottbus Timed Automata. In C. Rattray and M. Sveda, editors, Proceedings of the IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2000, Edinburgh, April 6-7), Stirling, pages 17-24, 2000. Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    A new modelling notation and a verification tool for hybrid systems is introduced: The Cottbus Timed Automaton (CTA). In contrast to existing modelling concepts, the new formalism has the advantage to be capable of modelling hybrid systems as a modular structure of components which communicate through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes how to model a system and how to verify it. The current version of the tool using the double description method to represent the regions is presented.
    Annotation:
    FSCBS 2000, Edinburgh, April 6-7
    Charles Rattray, Miroslav Sveda, editors
    [bibtex-entry]

  5. Dirk Beyer, Claus Lewerentz, and Frank Simon. Flattening Inheritance Structures -- OR -- Getting the Right Picture of Large OO-Systems. Technical report I-12/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, November 2000. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    More and more software systems are developed using the object oriented paradigm. Thus, large systems contain inheritance structures to provide a flexible and re-usable design and to allow for polymorphic method calls. This paper gives a detailed overview about the impact of using inheritance on measuring, understanding and using subclasses in such class systems. Usually, considering classes within an inheritance relation is reduced to the consideration of locally defined members of a class. This view might be incomplete or even misleading in some use cases. To provide an additional view on a given system we define a tool-supported flattening process which transforms an inheritance structure to a representation in which all the inherited members are explicit in each subclass. This representation provides additional insights for measuring, understanding, and developing large software systems.
    [bibtex-entry]

  6. Dirk Beyer and Andreas Noack. Efficient Verification of Real-Time Systems using BDDs. Technical report I-13/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, December 2000. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See FMICS01 [18] for proceedings version.
    [bibtex-entry]

  7. Frank Simon and Dirk Beyer. Considering Inheritance, Overriding, Overloading and Polymorphism for Measuring C++ Sources. Technical report I-04/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, May 2000. Keyword(s): Structural Analysis and Comprehension.
    Annotation:
    See IWSM00 [12] for proceedings version.
    [bibtex-entry]

1999

  1. Dirk Beyer and Heinrich Rust. Concepts of Cottbus Timed Automata. In K. Spies and B. Schätz, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 1999, München, June 17-18), pages 27-34, 1999. Herbert Utz Verlag, München. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    Today, many industrial production cells are controlled by software. Many such systems have to deal with requirements which the developer has to guarantee. Because of the complexity of the implementation one of the main problems for developing the software for reactive systems is to be sure that such properties are fulfilled. One way to handle the problems is to use formal methods: This means to develop a formal model which is used to prove the properties of the specification with tool support.
    There are many different methods to model such reactive systems. Some of these abstract from real-time aspects of the system. We chose a problem area where we have real-time requirements, for example the throughput of the modelled production cell. So we have to use formal methods which support models of real-time systems.
    Annotation:
    FBT 1999, München, June 17-18
    Katharina Spies and Bernhard Schätz, editors
    [bibtex-entry]

  2. Dirk Beyer and Heinrich Rust. A Formalism for Modular Modelling of Hybrid Systems. Technical report I-10/1999, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, October 1999. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See FSCBS01 [16] for proceedings version.
    [bibtex-entry]

  3. Dirk Beyer and Heinrich Rust. A Modular Hybrid Modelling Notation. Technical report I-03/1999, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, February 1999. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See TR10-BTU99 [04] for revised version.
    [bibtex-entry]

1998

  1. Dirk Beyer and Heinrich Rust. Modeling a Production Cell as a Distributed Real-Time System with Cottbus Timed Automata. In H. König and P. Langendörfer, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 1998, Cottbus, June 4-5), pages 148-159, 1998. Shaker Verlag, Aachen. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    We build on work in designing modeling languages for hybrid systems in the development of CTA, the Cottbus Timed Automata. Our design features a facility to specify a hybrid system modulary and hierarchically, communication through CSP-like synchronizations but with special support to specify explicitly different roles which the interface signals and variables of a module play, and to instantiate recurring elements serveral times from a template. Continuous system components are modeled with analogue variables having piecewise constant derivatives. Discrete system aspects like control modes are modeled with the discrete variables and the states of a finite automaton. Our approach to specifying distributed hybrid systems is illustrated with the specification of a component of a production cell, a transport belt.
    Annotation:
    FBT 1998, Cottbus, June 4-5
    Hartmut König, Peter Langendörfer, editors
    The first published paper where we introduce the concepts of Cottbus Timed Automata, i.e. modules, interfaces and a modeling example.
    [bibtex-entry]




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: Sun Nov 19 01:08:08 2017


This document was translated from BibTEX by bibtex2html