Loop Verification with Invariants and Contracts.

Publications by year

2020

  1. Dirk Beyer and Damien Zufferey, editors. Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS 11990, 2020. Springer. doi:10.1007/978-3-030-39322-9 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{VMCAI20, title = {Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)}, editor = {Dirk Beyer and Damien Zufferey}, year = {2020}, series = {LNCS~11990}, publisher = {Springer}, isbn = {978-3-030-39321-2}, doi = {10.1007/978-3-030-39322-9}, sha256 = {}, url = {https://popl20.sigplan.org/home/VMCAI-2020}, pdf = {https://doi.org/10.1007/978-3-030-39322-9}, }

2019

  1. Dirk Beyer and Chantal Keller, editors. Proceedings of the 13th International Conference on Tests and Proofs (TAP). LNCS 11823, 2019. Springer. doi:10.1007/978-3-030-31157-5 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TAP19, title = {Proceedings of the 13th International Conference on Tests and Proofs (TAP)}, editor = {Dirk Beyer and Chantal Keller}, year = {2019}, series = {LNCS~11823}, publisher = {Springer}, isbn = {978-3-030-31156-8}, doi = {10.1007/978-3-030-31157-5}, sha256 = {}, url = {https://tap.sosy-lab.org/2019/}, pdf = {https://doi.org/10.1007/978-3-030-31157-5}, }
  2. Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors. Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 3. LNCS 11429, 2019. Springer. doi:10.1007/978-3-030-17502-3 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TOOLympics19, title = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 3}, editor = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, isbn = {978-3-030-17501-6}, doi = {10.1007/978-3-030-17502-3}, sha256 = {}, url = {https://tacas.info/toolympics.php}, pdf = {https://doi.org/10.1007/978-3-030-17502-3}, }

2018

  1. Dirk Beyer and Marieke Huisman, editors. Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 2. LNCS 10806, 2018. Springer. doi:10.1007/978-3-319-89963-3 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TACAS18b, title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 2}, editor = {Dirk Beyer and Marieke Huisman}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, isbn = {978-3-319-89962-6}, doi = {10.1007/978-3-319-89963-3}, sha256 = {}, url = {https://www.etaps.org/index.php/2018/tacas}, pdf = {https://doi.org/10.1007/978-3-319-89963-3}, }
  2. Dirk Beyer and Marieke Huisman, editors. Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 1. LNCS 10805, 2018. Springer. doi:10.1007/978-3-319-89960-2 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{TACAS18a, title = {Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part 1}, editor = {Dirk Beyer and Marieke Huisman}, year = {2018}, series = {LNCS~10805}, publisher = {Springer}, isbn = {978-3-319-89959-6}, doi = {10.1007/978-3-319-89960-2}, sha256 = {}, url = {https://www.etaps.org/index.php/2018/tacas}, pdf = {https://doi.org/10.1007/978-3-319-89960-2}, }

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. doi:10.1007/978-3-642-38592-6 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{FORTE13, title = {Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (33rd FORTE / 15th FMOODS)}, editor = {Dirk Beyer and Michele Boreale}, year = {2013}, series = {LNCS~7892}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-38591-9}, doi = {10.1007/978-3-642-38592-6}, sha256 = {}, url = {https://forte13.sosy-lab.org/}, pdf = {https://doi.org/10.1007/978-3-642-38592-6}, }

2012

  1. Dirk Beyer, Arie van Deursen, and Michael W. Godfrey, editors. Proceedings of the 20th IEEE International Conference on Program Comprehension. 2012. IEEE. doi:10.1109/ICPC19659.2012 Link to this entry Publisher's Version PDF Supplement
    BibTeX Entry
    @proceedings{ICPC12, title = {Proceedings of the 20th IEEE International Conference on Program Comprehension}, editor = {Dirk Beyer and Arie van Deursen and Michael W. Godfrey}, year = {2012}, publisher = {IEEE}, isbn = {978-1-4673-1216-5}, doi = {10.1109/ICPC19659.2012}, url = {https://icpc12.sosy-lab.org/}, pdf = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6230782}, }

2002

  1. Dirk Beyer. Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata. 2002. Mensch & Buch Verlag, Berlin. Link to this entry Also: Dissertation, Brandenburgische Technische Universität Cottbus, 2002 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF Supplement
    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.
    BibTeX Entry
    @book{Diss02, author = {Dirk Beyer}, title = {Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata}, year = {2002}, publisher = {Mensch~\&~Buch Verlag, Berlin}, isbn = {3-89820-450-2}, url = {http://books.google.com/books?id=psEhN74boe4C&printsec=frontcover&dq=isbn:3898204502&source=gbs_summary_r&cad=0}, pdf = {https://www.sosy-lab.org/research/pub/2002-Dissertation.Formale_Verifikation_von_Realzeit-Systemen_mittels_Cottbus_Timed_Automata.pdf}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {BTU version: Dissertation
    Summary appeared as: 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.}, doinone = {DOI not available}, note = {Also: Dissertation, Brandenburgische Technische Universit{\"a}t Cottbus, 2002}, urn = {urn:nbn:de:kobv:co1-000000258}, }
    Additional Infos
    BTU version: Dissertation
    Summary appeared as: 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.

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: Tue Dec 07 02:51:54 2021