Formal Foundations of Consistency in Model-Driven Development
Pascual, R.; Beckert, B.; Ulbrich, M.; Kirsten, M.; Pfeifer, W.
2025. Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification : 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part III. Ed.: T. Margaria, 178–200, Springer Nature Switzerland. doi:10.1007/978-3-031-75380-0_11
Pascual, R.; Beckert, B.; Ulbrich, M.; Kirsten, M.; Pfeifer, W.
2025. Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification : 12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part III. Ed.: T. Margaria, 178–200, Springer Nature Switzerland. doi:10.1007/978-3-031-75380-0_11
The VerifyThis Collaborative Long-Term Challenge Series
Ahrendt, W.; Ernst, G.; Herber, P.; Huisman, M.; Monti, R. E.; Ulbrich, M.; Weigl, A.
2025. TOOLympics Challenge 2023 – Updates, Results, Successes of the Formal-Methods Competitions. Ed.: D. Beyer, 160–170, Springer Nature Switzerland. doi:10.1007/978-3-031-67695-6_6
Ahrendt, W.; Ernst, G.; Herber, P.; Huisman, M.; Monti, R. E.; Ulbrich, M.; Weigl, A.
2025. TOOLympics Challenge 2023 – Updates, Results, Successes of the Formal-Methods Competitions. Ed.: D. Beyer, 160–170, Springer Nature Switzerland. doi:10.1007/978-3-031-67695-6_6
The Java Verification Tool KeY: A Tutorial
Beckert, B.; Bubel, R.; Drodt, D.; Hähnle, R.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.; Weigl, A.
2025. Formal Methods : 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part II, 597 – 623, Springer Nature Switzerland. doi:10.1007/978-3-031-71177-0_32
Beckert, B.; Bubel, R.; Drodt, D.; Hähnle, R.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.; Weigl, A.
2025. Formal Methods : 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part II, 597 – 623, Springer Nature Switzerland. doi:10.1007/978-3-031-71177-0_32
Formally Verifying an Efficient Sorter
Beckert, B.; Sanders, P.; Ulbrich, M.; Witt, S.; Wiesler, J.
2024. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000167846
Beckert, B.; Sanders, P.; Ulbrich, M.; Witt, S.; Wiesler, J.
2024. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000167846
Formally Verifying an Efficient Sorter
Beckert, B.; Sanders, P.; Ulbrich, M.; Wiesler, J.; Witt, S.
2024. Tools and Algorithms for the Construction and Analysis of Systems – 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. Ed.: B. Finkbeiner, 268–287, Springer Nature Switzerland. doi:10.1007/978-3-031-57246-3_15
Beckert, B.; Sanders, P.; Ulbrich, M.; Wiesler, J.; Witt, S.
2024. Tools and Algorithms for the Construction and Analysis of Systems – 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I. Ed.: B. Finkbeiner, 268–287, Springer Nature Switzerland. doi:10.1007/978-3-031-57246-3_15
The Java Verification Tool KeY: A Tutorial
Beckert, B.; Bubel, R.; Drodt, D.; Hähnle, R.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.; Weigl, A.
2024. doi:10.5281/zenodo.11669182
Beckert, B.; Bubel, R.; Drodt, D.; Hähnle, R.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.; Weigl, A.
2024. doi:10.5281/zenodo.11669182
Contract Automata: A Specification Language for Mode-Based Systems
Weigl, A.; Bachmeier, J.; Ulbrich, M.; Beckert, B.
2024. FormaliSE ’24: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), 1–11, Association for Computing Machinery (ACM). doi:10.1145/3644033.3644381
Weigl, A.; Bachmeier, J.; Ulbrich, M.; Beckert, B.
2024. FormaliSE ’24: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), 1–11, Association for Computing Machinery (ACM). doi:10.1145/3644033.3644381
Scalable and Precise Refinement Types for Imperative Languages
Lanzinger, F.; Bachmeier, J.; Ulbrich, M.; Dietl, W.
2024. iFM 2023 – 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Ed.: P. Herber, 377–383, Springer Nature Switzerland. doi:10.1007/978-3-031-47705-8_20
Lanzinger, F.; Bachmeier, J.; Ulbrich, M.; Dietl, W.
2024. iFM 2023 – 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Ed.: P. Herber, 377–383, Springer Nature Switzerland. doi:10.1007/978-3-031-47705-8_20
Formally Verifying an Efficient Sorter - Verification and Benchmarking Artifact
Beckert, B.; Sanders, P.; Ulbrich, M.; Wiesler, J.; Witt, S.
2023, Dezember 30. doi:10.5281/zenodo.8436535
Beckert, B.; Sanders, P.; Ulbrich, M.; Wiesler, J.; Witt, S.
2023, Dezember 30. doi:10.5281/zenodo.8436535
Formal Specification and Verification of JDK’s Identity Hash Map Implementation
De Boer, M.; De Gouw, S.; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2023. Formal Aspects of Computing, 35 (3), 1–26. doi:10.1145/3594729
De Boer, M.; De Gouw, S.; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2023. Formal Aspects of Computing, 35 (3), 1–26. doi:10.1145/3594729
The ’Choc-Machine’ - an Introduction to Algorithmic Thinking using Finite State Machines
Vielsack, A.; Klein, M.; Niesenhaus, T.; Ulbrich, M.
2023. WiPSCE ’23: Proceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research, Ed.: S. Sentance, Art.-Nr.: 25, Association for Computing Machinery (ACM). doi:10.1145/3605468.3609772
Vielsack, A.; Klein, M.; Niesenhaus, T.; Ulbrich, M.
2023. WiPSCE ’23: Proceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research, Ed.: S. Sentance, Art.-Nr.: 25, Association for Computing Machinery (ACM). doi:10.1145/3605468.3609772
Verification of Red-Black Trees in KeY - A Case Study in Deductive Java Verification. Bachelorarbeit
Stuber, J.
2023, September 11. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000162878
Stuber, J.
2023, September 11. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000162878
Neue Einblicke in den Berufswahlprozess von Informatiklehrkräften
Hildebrandt, C.; Pampel, B.; Standl, B.; Hauck, F. J.; Ulbrich, M.; Paech Barbara
2023. INFOS 2023 - Informatikunterricht zwischen Aktualität und Zeitlosigkeit. Hrsg.: L., Hellmig; M., Hennecke;, 83 – 92, Gesellschaft für Informatik (GI). doi:10.18420/infos2023-006
Hildebrandt, C.; Pampel, B.; Standl, B.; Hauck, F. J.; Ulbrich, M.; Paech Barbara
2023. INFOS 2023 - Informatikunterricht zwischen Aktualität und Zeitlosigkeit. Hrsg.: L., Hellmig; M., Hennecke;, 83 – 92, Gesellschaft für Informatik (GI). doi:10.18420/infos2023-006
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY
Abbasi, R.; Schiffl, J.; Darulova, E.; Ulbrich, M.; Ahrendt, W.
2023. International Journal on Software Tools for Technology Transfer, 25 (2), 185–204. doi:10.1007/s10009-022-00691-x
Abbasi, R.; Schiffl, J.; Darulova, E.; Ulbrich, M.; Ahrendt, W.
2023. International Journal on Software Tools for Technology Transfer, 25 (2), 185–204. doi:10.1007/s10009-022-00691-x
Contract Automata: A Specification Language for Mode-Based Systems
Weigl, A.; Bachmeier, J.; Beckert, B.; Ulbrich, M.
2023. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000164563
Weigl, A.; Bachmeier, J.; Beckert, B.; Ulbrich, M.
2023. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000164563
Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Boer, M. de; Gouw, S. de; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2022. doi:10.5445/IR/1000145727
Boer, M. de; Gouw, S. de; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2022. doi:10.5445/IR/1000145727
Towards a Usable and Sustainable Deductive Verification Tool
Beckert, B.; Bubel, R.; Hähnle, R.; Ulbrich, M.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II. Ed.: T. Margaria, 281–300, Springer Nature Switzerland. doi:10.1007/978-3-031-19756-7_16
Beckert, B.; Bubel, R.; Hähnle, R.; Ulbrich, M.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II. Ed.: T. Margaria, 281–300, Springer Nature Switzerland. doi:10.1007/978-3-031-19756-7_16
SpecifyThis – Bridging Gaps Between Program Specification Paradigms
Ahrendt, W.; Herber, P.; Huisman, M.; Ulbrich, M.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. Ed.: T. Margaria, 3–6, Springer International Publishing. doi:10.1007/978-3-031-19849-6_1
Ahrendt, W.; Herber, P.; Huisman, M.; Ulbrich, M.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. Ed.: T. Margaria, 3–6, Springer International Publishing. doi:10.1007/978-3-031-19849-6_1
Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems
Beckert, B.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2022. Theoretical Aspects of Computing – ICTAC 2022 – 19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022, Proceedings. Ed.: H. Seidl, 7–13, Springer International Publishing. doi:10.1007/978-3-031-17715-6_2
Beckert, B.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2022. Theoretical Aspects of Computing – ICTAC 2022 – 19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022, Proceedings. Ed.: H. Seidl, 7–13, Springer International Publishing. doi:10.1007/978-3-031-17715-6_2
A Refactoring for Data Minimisation Using Formal Verification
Lanzinger, F.; Ulbrich, M.; Weigl, A.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II. Ed.: T. Margaria, 345–364, Springer Nature Switzerland. doi:10.1007/978-3-031-19756-7_19
Lanzinger, F.; Ulbrich, M.; Weigl, A.
2022. Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering – 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II. Ed.: T. Margaria, 345–364, Springer Nature Switzerland. doi:10.1007/978-3-031-19756-7_19
The Karlsruhe Java Verification Suite
Klamroth, J.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.
2022. The Logic of Software. A Tasting Menu of Formal Methods – Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday. Ed.: W. Ahrendt, 290–312, Springer International Publishing. doi:10.1007/978-3-031-08166-8_14
Klamroth, J.; Lanzinger, F.; Pfeifer, W.; Ulbrich, M.
2022. The Logic of Software. A Tasting Menu of Formal Methods – Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday. Ed.: W. Ahrendt, 290–312, Springer International Publishing. doi:10.1007/978-3-031-08166-8_14
Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Boer, M. de; Gouw, S. de; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2022. Integrated Formal Methods – 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings. Ed.: M. ter Beek, 45–62, Springer International Publishing. doi:10.1007/978-3-031-07727-2_4
Boer, M. de; Gouw, S. de; Klamroth, J.; Jung, C.; Ulbrich, M.; Weigl, A.
2022. Integrated Formal Methods – 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings. Ed.: M. ter Beek, 45–62, Springer International Publishing. doi:10.1007/978-3-031-07727-2_4
Inferring Interval-Valued Floating-Point Preconditions
Krämer, J.; Blatter, L.; Darulova, E.; Ulbrich, M.
2022. Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I. Ed.: D. Fisman, 303–321, Springer International Publishing. doi:10.1007/978-3-030-99524-9_16
Krämer, J.; Blatter, L.; Darulova, E.; Ulbrich, M.
2022. Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I. Ed.: D. Fisman, 303–321, Springer International Publishing. doi:10.1007/978-3-030-99524-9_16
Table-based formal specification approaches for control engineers—empirical studies of usability
Cha, S.; Vogel-Heuser, B.; Weigl, A.; Ulbrich, M.; Beckert, B.
2021. IET Cyber-Physical Systems: Theory and Applications, 64, 193–207. doi:10.1049/cps2.12017
Cha, S.; Vogel-Heuser, B.; Weigl, A.; Ulbrich, M.; Beckert, B.
2021. IET Cyber-Physical Systems: Theory and Applications, 64, 193–207. doi:10.1049/cps2.12017
Beratung und Berufsorientierung im Lehr-Lern-Labor Informatik in Karlsruhe
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Ritter, F.; Wagner, I.
2021. 16. Lernort-Labor(LeLa)-Jahrestagung "Interessieeren, fördern, beraten: Wie berufs- und studienorientierend sind Schülerlabore? (2021), Online, 8. März 2021
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Ritter, F.; Wagner, I.
2021. 16. Lernort-Labor(LeLa)-Jahrestagung "Interessieeren, fördern, beraten: Wie berufs- und studienorientierend sind Schülerlabore? (2021), Online, 8. März 2021
Beratung und Supervision im Lehr- Lern-Labor Informatik in Karlsruhe
Standl, B.; Bentz, A.; Vielsack, A.; Wagner, I.; Ulbrich, M.
2021. Beratung und Supervision in der Bildung von Lehrer*innen : Online Tagung an der Universität Bielefeld (2021), Bielefeld, Deutschland, 18.–19. Juni 2021
Standl, B.; Bentz, A.; Vielsack, A.; Wagner, I.; Ulbrich, M.
2021. Beratung und Supervision in der Bildung von Lehrer*innen : Online Tagung an der Universität Bielefeld (2021), Bielefeld, Deutschland, 18.–19. Juni 2021
Deductive Verification of Floating-Point Java Programs in KeY
Abbasi, R.; Schiffl, J.; Darulova, E.; Ulbrich, M.; Ahrendt, W.
2021. Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II. Ed.: J. F. Groote, 242–261, Springer International Publishing. doi:10.1007/978-3-030-72013-1_13
Abbasi, R.; Schiffl, J.; Darulova, E.; Ulbrich, M.; Ahrendt, W.
2021. Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II. Ed.: J. F. Groote, 242–261, Springer International Publishing. doi:10.1007/978-3-030-72013-1_13
Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
Lanzinger, F.; Weigl, A.; Ulbrich, M.; Dietl, W.
2021. Proceedings of the ACM on programming languages, 5 (OOPSLA), Article no: 143. doi:10.1145/3485520
Lanzinger, F.; Weigl, A.; Ulbrich, M.; Dietl, W.
2021. Proceedings of the ACM on programming languages, 5 (OOPSLA), Article no: 143. doi:10.1145/3485520
Reconstructing z3 proofs in KeY: There and back again
Pfeifer, W.; Schiffl, J.; Ulbrich, M.
2021. Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null, 24–31, Association for Computing Machinery (ACM). doi:10.1145/3464971.3468421
Pfeifer, W.; Schiffl, J.; Ulbrich, M.
2021. Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null, 24–31, Association for Computing Machinery (ACM). doi:10.1145/3464971.3468421
Runtime Verification of Generalized Test Tables
Weigl, A.; Ulbrich, M.; Tyszberowicz, S.; Klamroth, J.
2021. NASA Formal Methods: 13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings. Ed.: A. Dutle, 358–374, Springer-Verlag. doi:10.1007/978-3-030-76384-8_22
Weigl, A.; Ulbrich, M.; Tyszberowicz, S.; Klamroth, J.
2021. NASA Formal Methods: 13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings. Ed.: A. Dutle, 358–374, Springer-Verlag. doi:10.1007/978-3-030-76384-8_22
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher Education
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020, November 17. 13th International Conference on Informatics in Schools: Situation, Evaluation, Problems (ISSEP 2020), Online, 16.–18. November 2020
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020, November 17. 13th International Conference on Informatics in Schools: Situation, Evaluation, Problems (ISSEP 2020), Online, 16.–18. November 2020
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher Education
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020, November 17. 13th International Conference on Informatics in Schools: Situation, Evaluation, Problems (ISSEP 2020), Online, 16.–18. November 2020
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020, November 17. 13th International Conference on Informatics in Schools: Situation, Evaluation, Problems (ISSEP 2020), Online, 16.–18. November 2020
Relational Test Tables – A Practical Specification Language for Evolution and Security
Weigl, A.; Ulbrich, M.; Cha, S.; Beckert, B.; Vogel-Heuser, B.
2020. FormaliSE ’20: 8th International Conference on Formal Methods in Software Engineering, Seoul Republic of Korea, October, 2020, 77–86, Association for Computing Machinery (ACM). doi:10.1145/3372020.3391566
Weigl, A.; Ulbrich, M.; Cha, S.; Beckert, B.; Vogel-Heuser, B.
2020. FormaliSE ’20: 8th International Conference on Formal Methods in Software Engineering, Seoul Republic of Korea, October, 2020, 77–86, Association for Computing Machinery (ACM). doi:10.1145/3372020.3391566
Smart Contracts: Application Scenarios for Deductive Program Verification
Beckert, B.; Schiffl, J.; Ulbrich, M.
2020. Formal Methods. FM 2019 International Workshops : Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I. Ed.: Emil Sekerinski, 293–298, Springer. doi:10.1007/978-3-030-54994-7_21
Beckert, B.; Schiffl, J.; Ulbrich, M.
2020. Formal Methods. FM 2019 International Workshops : Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I. Ed.: Emil Sekerinski, 293–298, Springer. doi:10.1007/978-3-030-54994-7_21
VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event
Huismann, M.; Monti, R. E.; Ulbrich, M.; Weigl, A. (Hrsg.)
2020
Huismann, M.; Monti, R. E.; Ulbrich, M.; Weigl, A. (Hrsg.)
2020
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher Education
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020. Informatics in Schools. Engaging Learners in Computational Thinking – 13th International Conference, ISSEP 2020, Tallinn, Estonia, November 16–18, 2020, Proceedings. Ed.: K. Kori, 133–145, Springer International Publishing. doi:10.1007/978-3-030-63212-0_11
Standl, B.; Bentz, A.; Ulbrich, M.; Vielsack, A.; Wagner, I.
2020. Informatics in Schools. Engaging Learners in Computational Thinking – 13th International Conference, ISSEP 2020, Tallinn, Estonia, November 16–18, 2020, Proceedings. Ed.: K. Kori, 133–145, Springer International Publishing. doi:10.1007/978-3-030-63212-0_11
Modular Regression Verification for Reactive Systems
Weigl, A.; Ulbrich, M.; Lentzsch, D.
2020. Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles ; 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II. Ed.: T. Margaria, 25–43, Springer-Verlag. doi:10.1007/978-3-030-61470-6_3
Weigl, A.; Ulbrich, M.; Lentzsch, D.
2020. Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles ; 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II. Ed.: T. Margaria, 25–43, Springer-Verlag. doi:10.1007/978-3-030-61470-6_3
Modular Verification of JML Contracts Using Bounded Model Checking
Beckert, B.; Kirsten, M.; Klamroth, J.; Ulbrich, M.
2020. ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium (ISoLA 2020), 60–80, Springer. doi:10.1007/978-3-030-61362-4_4
Beckert, B.; Kirsten, M.; Klamroth, J.; Ulbrich, M.
2020. ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium (ISoLA 2020), 60–80, Springer. doi:10.1007/978-3-030-61362-4_4
Seamless interactive program verification
Grebing, S.; Klamroth, J.; Ulbrich, M.
2020. Verified Software. Theories, Tools, and Experiments : 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019. Revised Selected Papers. Ed.: S. Chakraborty, 68–86, Springer. doi:10.1007/978-3-030-41600-3_6
Grebing, S.; Klamroth, J.; Ulbrich, M.
2020. Verified Software. Theories, Tools, and Experiments : 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019. Revised Selected Papers. Ed.: S. Chakraborty, 68–86, Springer. doi:10.1007/978-3-030-41600-3_6
On the preservation of the trust by regression verification of plc software for cyber-physical systems of systems
Cha, S.; Ulbrich, M.; Weigl, A.; Beckert, B.; Land, K.; Vogel-Heuser, B.
2020. IEEE International Conference on Industrial Informatics (INDIN), Helsinki/Espoo, Finland, July 22-25, July 22-25, 2019, 413–418, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN41052.2019.8972210
Cha, S.; Ulbrich, M.; Weigl, A.; Beckert, B.; Land, K.; Vogel-Heuser, B.
2020. IEEE International Conference on Industrial Informatics (INDIN), Helsinki/Espoo, Finland, July 22-25, July 22-25, 2019, 413–418, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN41052.2019.8972210
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Angelis, E. D.; Fedyukovich, G.; Tzevelekos, N.; Ulbrich, M.
2019. Electronic proceedings in theoretical computer science, 296, 1–48. doi:10.4204/EPTCS.296
Angelis, E. D.; Fedyukovich, G.; Tzevelekos, N.; Ulbrich, M.
2019. Electronic proceedings in theoretical computer science, 296, 1–48. doi:10.4204/EPTCS.296
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Angelis, E. D.; Fedyukovich, G.; Tzevelekos, N.; Ulbrich, M.
2019
Angelis, E. D.; Fedyukovich, G.; Tzevelekos, N.; Ulbrich, M.
2019
Addressed Challenges
Jung, R.; Märtin, L.; Johanssen, J. O.; Paech, B.; Lochau, M.; Thüm, T.; Schneider, K.; Tichy, M.; Ulbrich, M.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 21–36, Springer. doi:10.1007/978-3-030-13499-0_3
Jung, R.; Märtin, L.; Johanssen, J. O.; Paech, B.; Lochau, M.; Thüm, T.; Schneider, K.; Tichy, M.; Ulbrich, M.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 21–36, Springer. doi:10.1007/978-3-030-13499-0_3
Learning from Evolution for Evolution
Kögel, S.; Tichy, M.; Chakraborty, A.; Fay, A.; Vogel-Heuser, B.; Haubeck, C.; Taentzer, G.; Kehrer, T.; Ladiges, J.; Grunske, L.; Ulbrich, M.; Bougouffa, S.; Getir, S.; Cha, S.; Kelter, U.; Lamersdorf, W.; Busch, K.; Heinrich, R.; Koch, S.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 255–308, Springer. doi:10.1007/978-3-030-13499-0_10
Kögel, S.; Tichy, M.; Chakraborty, A.; Fay, A.; Vogel-Heuser, B.; Haubeck, C.; Taentzer, G.; Kehrer, T.; Ladiges, J.; Grunske, L.; Ulbrich, M.; Bougouffa, S.; Getir, S.; Cha, S.; Kelter, U.; Lamersdorf, W.; Busch, K.; Heinrich, R.; Koch, S.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 255–308, Springer. doi:10.1007/978-3-030-13499-0_10
Formal Verification of Evolutionary Changes
Beckert, B.; Mund, J.; Ulbrich, M.; Weigl, A.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 309–332, Springer. doi:10.1007/978-3-030-13499-0_11
Beckert, B.; Mund, J.; Ulbrich, M.; Weigl, A.
2019. Managed Software Evolution. Hrsg.: Ralf H. Reussner, Michael Goedicke, Wilhelm Hasselbring, Birgit Vogel-Heuser, Jan Keim, Lukas Märtin, 309–332, Springer. doi:10.1007/978-3-030-13499-0_11
Using Relational Verification for Program Slicing
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2019. Software Engineering and Formal Methods – 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. Ed.: P. Ölveczky, 353–372, Springer. doi:10.1007/978-3-030-30446-1_19
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2019. Software Engineering and Formal Methods – 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. Ed.: P. Ölveczky, 353–372, Springer. doi:10.1007/978-3-030-30446-1_19
VerifyThis – Verification Competition with a Human Factor
Ernst, G.; Huisman, M.; Mostowski, W.; Ulbrich, M.
2019. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019; Prague; Czech Republic; 6 April 2019 through 11 April 2019. Ed.: B. Steffen, 176–195, Springer. doi:10.1007/978-3-030-17502-3_12
Ernst, G.; Huisman, M.; Mostowski, W.; Ulbrich, M.
2019. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019; Prague; Czech Republic; 6 April 2019 through 11 April 2019. Ed.: B. Steffen, 176–195, Springer. doi:10.1007/978-3-030-17502-3_12
Using Relational Verification for Program Slicing
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2019. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000093895
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2019. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000093895
Achieving delta description of the control software for an automated production system evolution
Cha, S.; Weigl, A.; Ulbrich, M.; Beckert, B.; Vogel-Heuser, B.
2018. 14th IEEE International Conference on Automation Science and Engineering, CASE 2018; Technical University MunichMunich; Germany; 20 August 2018 through 24 August 2018, 1170–1176, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/COASE.2018.8560588
Cha, S.; Weigl, A.; Ulbrich, M.; Beckert, B.; Vogel-Heuser, B.
2018. 14th IEEE International Conference on Automation Science and Engineering, CASE 2018; Technical University MunichMunich; Germany; 20 August 2018 through 24 August 2018, 1170–1176, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/COASE.2018.8560588
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Beckert, B.; Bingmann, T.; Kiefer, M.; Sanders, P.; Ulbrich, M.; Weigl, A.
2018. Verified Software: Theories, Tools, and Experiments; 10th International Conference, VSTTE 2018; Oxford, UK, July 18–19, 2018; Revised Selected Papers. Ed.: R. Piskac, 248–266, Springer Nature. doi:10.1007/978-3-030-03592-1_14
Beckert, B.; Bingmann, T.; Kiefer, M.; Sanders, P.; Ulbrich, M.; Weigl, A.
2018. Verified Software: Theories, Tools, and Experiments; 10th International Conference, VSTTE 2018; Oxford, UK, July 18–19, 2018; Revised Selected Papers. Ed.: R. Piskac, 248–266, Springer Nature. doi:10.1007/978-3-030-03592-1_14
Towards a notion of coverage for incomplete program-correctness proofs
Beckert, B.; Herda, M.; Kobischke, S.; Ulbrich, M.
2018. 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018; Limassol; Cyprus; 5 November 2018 through 9 November 2018. Ed.: T. Margaria, 53–63, Springer. doi:10.1007/978-3-030-03421-4_4
Beckert, B.; Herda, M.; Kobischke, S.; Ulbrich, M.
2018. 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018; Limassol; Cyprus; 5 November 2018 through 9 November 2018. Ed.: T. Margaria, 53–63, Springer. doi:10.1007/978-3-030-03421-4_4
Applicability of generalized test tables: a case study using the manufacturing system demonstrator xPPU
Cha, S.; Weigl, A.; Ulbrich, M.; Beckert, B.; Vogel-Heuser, B.
2018. Automatisierungstechnik, 66 (10), 834–848. doi:10.1515/auto-2018-0028
Cha, S.; Weigl, A.; Ulbrich, M.; Beckert, B.; Vogel-Heuser, B.
2018. Automatisierungstechnik, 66 (10), 834–848. doi:10.1515/auto-2018-0028
Proving equivalence between imperative and MapReduce implementations using program transformations
Beckert, B.; Bingmann, T.; Kiefer, M.; Sanders, P.; Ulbrich, M.; Weigl, A.
2018. 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018; Thessaloniki; Greece; 20 April 2018. Ed.: R. van Glabbeek, 185–199, Open Publishing Association. doi:10.4204/EPTCS.268.7
Beckert, B.; Bingmann, T.; Kiefer, M.; Sanders, P.; Ulbrich, M.; Weigl, A.
2018. 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018; Thessaloniki; Greece; 20 April 2018. Ed.: R. van Glabbeek, 185–199, Open Publishing Association. doi:10.4204/EPTCS.268.7
Generation of monitoring functions in production automation using test specifications
Cha, S.; Ulewicz, S.; Vogel-Heuser, B.; Weigl, A.; Ulbrich, M.; Beckert, B.
2017. 2017 IEEE 15th International Conference on Industrial Informatics (INDIN), Emden, Germany, 24-26 July 2017 : proceedings, 339–344, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN.2017.8104795
Cha, S.; Ulewicz, S.; Vogel-Heuser, B.; Weigl, A.; Ulbrich, M.; Beckert, B.
2017. 2017 IEEE 15th International Conference on Industrial Informatics (INDIN), Emden, Germany, 24-26 July 2017 : proceedings, 339–344, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN.2017.8104795
Proving JDK’s Dual Pivot Quicksort Correct
Beckert, B.; Schiffl, J.; Schmitt, P. H.; Ulbrich, M.
2017. Verified Software : Theories, Tools, and Experiments, Proceedings of the 9th International Conference, VSTTE 2017, Revised Selected Papers, Heidelberg, Germany, 22nd - 23th July 2017. Ed.: A. Paskevich, 35–48, Springer. doi:10.1007/978-3-319-72308-2_3
Beckert, B.; Schiffl, J.; Schmitt, P. H.; Ulbrich, M.
2017. Verified Software : Theories, Tools, and Experiments, Proceedings of the 9th International Conference, VSTTE 2017, Revised Selected Papers, Heidelberg, Germany, 22nd - 23th July 2017. Ed.: A. Paskevich, 35–48, Springer. doi:10.1007/978-3-319-72308-2_3
An interaction concept for program verification systems with explicit proof object
Beckert, B.; Grebing, S.; Ulbrich, M.
2017. Hardware and Software : Verification and Testing, 13th International Haifa Verification Conference, Haifa, Israel, 13th - 15th November 2017. Ed.: O. Strichman, 163–178, Springer. doi:10.1007/978-3-319-70389-3_11
Beckert, B.; Grebing, S.; Ulbrich, M.
2017. Hardware and Software : Verification and Testing, 13th International Haifa Verification Conference, Haifa, Israel, 13th - 15th November 2017. Ed.: O. Strichman, 163–178, Springer. doi:10.1007/978-3-319-70389-3_11
VerifyThis 2017 : A Program Verification Competition
Huisman, M.; Monahan, R.; Müller, P.; Mostowski, W.; Ulbrich, M.
2017. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000077160
Huisman, M.; Monahan, R.; Müller, P.; Mostowski, W.; Ulbrich, M.
2017. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000077160
Generalised Test Tables : A Practical Specification Language for Reactive Systems
Beckert, B.; Cha, S.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2017. Integrated Formal Methods : 13th International Conference, IFM 2017, Proceedings, Turin, Italy, 20th - 22nd September 2017. Ed.: N. Polikarpova, 129–144, Springer. doi:10.1007/978-3-319-66845-1_9
Beckert, B.; Cha, S.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2017. Integrated Formal Methods : 13th International Conference, IFM 2017, Proceedings, Turin, Italy, 20th - 22nd September 2017. Ed.: N. Polikarpova, 129–144, Springer. doi:10.1007/978-3-319-66845-1_9
SemSlice : Exploiting Relational Verification for Automatic Program Slicing
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2017. Integrated Formal Methods : 13th International Conference, IFM 2017, Proceedings, Turin, Italy, 20th - 22nd September 2017. Ed.: N. Polikarpova, 312–319, Springer. doi:10.1007/978-3-319-66845-1_20
Beckert, B.; Bormer, T.; Gocht, S.; Herda, M.; Lentzsch, D.; Ulbrich, M.
2017. Integrated Formal Methods : 13th International Conference, IFM 2017, Proceedings, Turin, Italy, 20th - 22nd September 2017. Ed.: N. Polikarpova, 312–319, Springer. doi:10.1007/978-3-319-66845-1_20
Relational Program Reasoning Using Compiler IR : Combining Static Verification and Dynamic Analysis
Kiefer, M.; Klebanov, V.; Ulbrich, M.
2017. Journal of automated reasoning, 1–27. doi:10.1007/s10817-017-9433-5
Kiefer, M.; Klebanov, V.; Ulbrich, M.
2017. Journal of automated reasoning, 1–27. doi:10.1007/s10817-017-9433-5
Automating regression verification of pointer programs by predicate abstraction
Klebanov, V.; Rümmer, P.; Ulbrich, M.
2017. Formal methods in system design, 1–31. doi:10.1007/s10703-017-0293-8
Klebanov, V.; Rümmer, P.; Ulbrich, M.
2017. Formal methods in system design, 1–31. doi:10.1007/s10703-017-0293-8
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems
Weigl, A.; Wiebe, F.; Ulbrich, M.; Ulewicz, S.; Cha, S.; Kirsten, M.; Beckert, B.; Birgit Vogel-Heuser
2017. 15th IEEE International Conference on Industrial Informatics (INDIN 2017), Emden, July 24-26 2017, Institute of Electrical and Electronics Engineers (IEEE)
Weigl, A.; Wiebe, F.; Ulbrich, M.; Ulewicz, S.; Cha, S.; Kirsten, M.; Beckert, B.; Birgit Vogel-Heuser
2017. 15th IEEE International Conference on Industrial Informatics (INDIN 2017), Emden, July 24-26 2017, Institute of Electrical and Electronics Engineers (IEEE)
Automated Verification for Functional and Relational Properties of Voting Rules
Beckert, B.; Bormer, T.; Kirsten, M.; Neuber, T.; Ulbrich, M.
2016. Sixth International Workshop on Computational Social Choice, COMSOC-2016, Toulouse, France, 22–24 June 2016, 16 S
Beckert, B.; Bormer, T.; Kirsten, M.; Neuber, T.; Ulbrich, M.
2016. Sixth International Workshop on Computational Social Choice, COMSOC-2016, Toulouse, France, 22–24 June 2016, 16 S
Modular specification and verification
Grahl, D.; Bubel, R.; Mostowski, W.; Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 289–351, Springer International Publishing. doi:10.1007/978-3-319-49812-6_9
Grahl, D.; Bubel, R.; Mostowski, W.; Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 289–351, Springer International Publishing. doi:10.1007/978-3-319-49812-6_9
Proof search with taclets
Rümmer, P.; Ulbrich, M.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 107–147, Springer International Publishing. doi:10.1007/978-3-319-49812-6_4
Rümmer, P.; Ulbrich, M.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 107–147, Springer International Publishing. doi:10.1007/978-3-319-49812-6_4
From specification to proof obligations
Grahl, D.; Ulbrich, M.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 243–287, Springer International Publishing. doi:10.1007/978-3-319-49812-6_8
Grahl, D.; Ulbrich, M.
2016. Deductive Software Verification – The KeY Book. From Theory to Practice. Ed. : W. Ahrendt, 243–287, Springer International Publishing. doi:10.1007/978-3-319-49812-6_8
A verification-supported evolution approach to assist software application engineers in industrial factory automation
Ulewicz, S.; Ulbrich, M.; Weigl, A.; Kirsten, M.; Wiebe, F.; Beckert, B.; Vogel-Heuser, B.
2016. 2016 IEEE International Symposium on Assembly and Manufacturing, ISAM 2016, Fort Worth, United States, 21 - 22 August, 2016, 19–25, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ISAM.2016.7750714
Ulewicz, S.; Ulbrich, M.; Weigl, A.; Kirsten, M.; Wiebe, F.; Beckert, B.; Vogel-Heuser, B.
2016. 2016 IEEE International Symposium on Assembly and Manufacturing, ISAM 2016, Fort Worth, United States, 21 - 22 August, 2016, 19–25, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ISAM.2016.7750714
Relational program reasoning using compiler IR
Kiefer, M.; Klebanov, V.; Ulbrich, M.
2016. Verified Software. Theories, Tools, and Experiments : 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17–18, 2016, Revised Selected Papers. Ed.: S. Blazy, 149–165, Springer. doi:10.1007/978-3-319-48869-1_12
Kiefer, M.; Klebanov, V.; Ulbrich, M.
2016. Verified Software. Theories, Tools, and Experiments : 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17–18, 2016, Revised Selected Papers. Ed.: S. Blazy, 149–165, Springer. doi:10.1007/978-3-319-48869-1_12
Dynamic Dispatch for Method Contracts Through Abstract Predicates
Mostowski, W.; Ulbrich, M.
2016. Transactions on Modularity and Composition I, 238–267, Springer-Verlag. doi:10.1007/978-3-319-46969-0_7
Mostowski, W.; Ulbrich, M.
2016. Transactions on Modularity and Composition I, 238–267, Springer-Verlag. doi:10.1007/978-3-319-46969-0_7
Axiomatization of Typed First-Order Logic
Schmitt, P. H.; Ulbrich, M.
2015. 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway, June 24-26, 2015, Proceedings. Ed.: N. Bjørner, 470–486, Springer. doi:10.1007/978-3-319-19249-9_29
Schmitt, P. H.; Ulbrich, M.
2015. 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway, June 24-26, 2015, Proceedings. Ed.: N. Bjørner, 470–486, Springer. doi:10.1007/978-3-319-19249-9_29
Dynamic Dispatch for Method Contracts through Abstract Predicates
Mostowski, W.; Ulbrich, M.
2015. 15th International Conference on MODULARITY (MODULARITY15), proceedings : March 16-19, 2015, Fort Collins, CO, USA. Ed.: R. France, 109–116, Association for Computing Machinery (ACM). doi:10.1145/2724525.2724574
Mostowski, W.; Ulbrich, M.
2015. 15th International Conference on MODULARITY (MODULARITY15), proceedings : March 16-19, 2015, Fort Collins, CO, USA. Ed.: R. France, 109–116, Association for Computing Machinery (ACM). doi:10.1145/2724525.2724574
Regression Verification for Java Using a Secure Information Flow Calculus
Beckert, B.; Klebanov, V.; Ulbrich, M.
2015. Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP ’15) , Prague, Czech Republic, July 7th, 2015, Art.Nr.: a6, Association for Computing Machinery (ACM). doi:10.1145/2786536.2786544
Beckert, B.; Klebanov, V.; Ulbrich, M.
2015. Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP ’15) , Prague, Czech Republic, July 7th, 2015, Art.Nr.: a6, Association for Computing Machinery (ACM). doi:10.1145/2786536.2786544
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant Diversity
Ulewicz, S.; Ulbrich, M.; Weigl, A.; Beckert, B.; Vogel-Heuser, B.
2015. 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA 2015) : Luxembourg, 8 - 11 September 2015, Art.Nr.: 7301603, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ETFA.2015.7301603
Ulewicz, S.; Ulbrich, M.; Weigl, A.; Beckert, B.; Vogel-Heuser, B.
2015. 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA 2015) : Luxembourg, 8 - 11 September 2015, Art.Nr.: 7301603, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/ETFA.2015.7301603
Selected Challenges of Software Evolution for Automated Production Systems
Vogel-Heuser, B.; Feldmann, S.; Folmer, J.; Kowal, M.; Schaefer, I.; Ladiges, J.; Fay, A.; Haubeck, C.; Lamersdorf, W.; Lity, S.; Kehrer, T.; Tichy, M.; Getir, S.; Ulbrich, M.; Klebanov, V.; Beckert, B.
2015. 2015 IEEE 13th International Conference on Industrial Informatics (INDIN 2015) : Cambridge, United Kingdom, 22 - 24 July 2015, 314–321, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN.2015.7281753
Vogel-Heuser, B.; Feldmann, S.; Folmer, J.; Kowal, M.; Schaefer, I.; Ladiges, J.; Fay, A.; Haubeck, C.; Lamersdorf, W.; Lity, S.; Kehrer, T.; Tichy, M.; Getir, S.; Ulbrich, M.; Klebanov, V.; Beckert, B.
2015. 2015 IEEE 13th International Conference on Industrial Informatics (INDIN 2015) : Cambridge, United Kingdom, 22 - 24 July 2015, 314–321, Institute of Electrical and Electronics Engineers (IEEE). doi:10.1109/INDIN.2015.7281753
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided Surgery
Ulbrich, M.; Schreiter, L.; Grebing, S.; Raczkowsky, J.; Wörn, H.; Beckert, B.
2015. FTSCS 2015 Fourth International Workshop on Formal Techniques for Safety-Critical Systems, November 6 and 7, 2015 Paris, France
Ulbrich, M.; Schreiter, L.; Grebing, S.; Raczkowsky, J.; Wörn, H.; Beckert, B.
2015. FTSCS 2015 Fourth International Workshop on Formal Techniques for Safety-Critical Systems, November 6 and 7, 2015 Paris, France
Implementation-level Verification of Algorithms with KeY
Bruns, D.; Mostowski, W.; Ulbrich, M.
2015. International journal on software tools for technology transfer, 17 (6), 729–744. doi:10.1007/s10009-013-0293-y
Bruns, D.; Mostowski, W.; Ulbrich, M.
2015. International journal on software tools for technology transfer, 17 (6), 729–744. doi:10.1007/s10009-013-0293-y
Regression Verification for Programmable Logic Controller Software
Beckert, B.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2015. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000047251
Beckert, B.; Ulbrich, M.; Vogel-Heuser, B.; Weigl, A.
2015. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000047251
Automating Regression Verification
Felsing, D.; Grebing, S.; Klebanov, V.; Rümmer, P.; Ulbrich, M.
2014. ASE ’14 : proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering : September 15-19, 2014, Västerås, Sweden, 349–359, Association for Computing Machinery (ACM). doi:10.1145/2642937.2642987
Felsing, D.; Grebing, S.; Klebanov, V.; Rümmer, P.; Ulbrich, M.
2014. ASE ’14 : proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering : September 15-19, 2014, Västerås, Sweden, 349–359, Association for Computing Machinery (ACM). doi:10.1145/2642937.2642987
JKelloy: A Proof Assistant for Relational Specifications of Java Programs
El Ghazi, A. A.; Ulbrich, M.; Gladisch, C.; Tyszberowicz, S.; Taghdiri, M.
2014. NASA Formal Methods - 6th International Symposium (NFM’14), Houston, Texas/USA, April 29 - May 1, 2014. Ed.: J. M. Badger, 173–187, Springer US. doi:10.1007/978-3-319-06200-6_13
El Ghazi, A. A.; Ulbrich, M.; Gladisch, C.; Tyszberowicz, S.; Taghdiri, M.
2014. NASA Formal Methods - 6th International Symposium (NFM’14), Houston, Texas/USA, April 29 - May 1, 2014. Ed.: J. M. Badger, 173–187, Springer US. doi:10.1007/978-3-319-06200-6_13
The KeY Platform for Verification and Analysis of Java Programs
Ahrendt, W.; Beckert, B.; Bruns, D.; Bubel, R.; Gladisch, C.; Grebing, S.; Hähnle, R.; Hentschel, M.; Herda, M.; Klebanov, V.; Mostowski, W.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2014. Verified Software: Theories, Tools and Experiments - 6th International Conference (VSTTE’14), Wien, Österreich, July 17-18, 2014. Ed.: D. Giannakopoulou, 55–71, Springer US. doi:10.1007/978-3-319-12154-3_4
Ahrendt, W.; Beckert, B.; Bruns, D.; Bubel, R.; Gladisch, C.; Grebing, S.; Hähnle, R.; Hentschel, M.; Herda, M.; Klebanov, V.; Mostowski, W.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2014. Verified Software: Theories, Tools and Experiments - 6th International Conference (VSTTE’14), Wien, Österreich, July 17-18, 2014. Ed.: D. Giannakopoulou, 55–71, Springer US. doi:10.1007/978-3-319-12154-3_4
On Verifying Relational Specifications of Java Programs with JKelloy
El Ghazi, A. A.; Ulbrich, M.; Gladisch, C.; Tyszberowicz, S.; Taghdiri, M.
2014. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000039153
El Ghazi, A. A.; Ulbrich, M.; Gladisch, C.; Tyszberowicz, S.; Taghdiri, M.
2014. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000039153
Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement. Dissertation
Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000041169
Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000041169
Reducing the Complexity of Quantified Formulas via Variable Elimination
El Ghazi, A. A.; Ulbrich, M.; Taghdiri, M.; Herda, M.
2013. 11th International Workshop on Satisfiability Modulo Theories (SMT’13), Helsinki, Finland, July 8-9, 2013
El Ghazi, A. A.; Ulbrich, M.; Taghdiri, M.; Herda, M.
2013. 11th International Workshop on Satisfiability Modulo Theories (SMT’13), Helsinki, Finland, July 8-9, 2013
Information Flow in Object-Oriented Software - Extended Version -
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000037606
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000037606
Information Flow in Object-Oriented Software
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Logic-Based Program Synthesis and Transformation, LOPSTR 2013, Madrid, Spain, September 16-18, 2013 [Konferenz]. Ed.: G. Gupta, 15–32, Universidad
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Logic-Based Program Synthesis and Transformation, LOPSTR 2013, Madrid, Spain, September 16-18, 2013 [Konferenz]. Ed.: G. Gupta, 15–32, Universidad
Secure Information Flow for Java. A Dynamic Logic Approach. Extended Version
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000036786
Beckert, B.; Bruns, D.; Klebanov, V.; Scheben, C.; Schmitt, P. H.; Ulbrich, M.
2013. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000036786
A Proof Assistant for Alloy Specifications
Ulbrich, M.; Geilmann, U.; El Ghazi, A. A.; Taghdiri, M.
2012. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Ed.: C. Flanagan, 422–436, Springer-Verlag
Ulbrich, M.; Geilmann, U.; El Ghazi, A. A.; Taghdiri, M.
2012. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Ed.: C. Flanagan, 422–436, Springer-Verlag
A Dual-Engine for Early Analysis of Critical Systems
El Ghazi, A. A.; Geilmann, U.; Ulbrich, M.; Taghdiri, M.
2011. Workshop on Dependable Software for Critical Infrastructures (DSCI), 4.-7. Okt. 2011, Berlin, 1–15
El Ghazi, A. A.; Geilmann, U.; Ulbrich, M.; Taghdiri, M.
2011. Workshop on Dependable Software for Critical Infrastructures (DSCI), 4.-7. Okt. 2011, Berlin, 1–15
On Proving Alloy Specifications Using KeY
Ulbrich, M.; Geilmann, U.; El Ghazi, A. A.; Taghdiri, M.
2011. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000025523
Ulbrich, M.; Geilmann, U.; El Ghazi, A. A.; Taghdiri, M.
2011. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000025523
A Dynamic Logic for Unstructured Programs with Embedded Assertions
Ulbrich, M.
2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Ed.: B. Beckert, 128–142, Karlsruher Institut für Technologie (KIT)
Ulbrich, M.
2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Ed.: B. Beckert, 128–142, Karlsruher Institut für Technologie (KIT)
Dynamic Frames in Java Dynamic Logic
Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Ed.: B. Beckert, 113–127, Karlsruher Institut für Technologie (KIT)
Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. Ed.: B. Beckert, 113–127, Karlsruher Institut für Technologie (KIT)
Dynamic Frames in Java Dynamic Logic. Formalisation and Proofs
Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2010. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000018332
Schmitt, P. H.; Ulbrich, M.; Weiß, B.
2010. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000018332
Deductive Verification of a Byzantine Agreement Protocol
Krenický, R.; Ulbrich, M.
2010. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000017275
Krenický, R.; Ulbrich, M.
2010. Karlsruher Institut für Technologie (KIT). doi:10.5445/IR/1000017275