Ever Change a Running System: Structured Software Reengineering Using Automatically Proven-Correct Transformation Rules

Autor: Dominic Steinhöfel

Publikováno v: Ernst Denert Award for Software Engineering 2020 ISBN: 9783030831271

Legacy systems are business-critical software systems whose failure can have a significant impact on the business. Yet, their maintenance and adaption to changed requirements consume a considerable amount of the total software development costs. Freq

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::dadf68a47ff4f679ec8c724651aa0b32
https://doi.org/10.1007/978-3-030-83128-8_10

Certified Abstract Cost Analysis

Autor: Dominic Steinhöfel, Elvira Albert, Reiner Hähnle, Alicia Merayo

Publikováno v: Fundamental Approaches to Software Engineering ISBN: 9783030714994
FASE

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation, optimization, or paral

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::d53aa7fc17ed7ff63a28de816d11a34a
https://doi.org/10.1007/978-3-030-71500-7_2

The Trace Modality

Autor: Reiner Hähnle, Dominic Steinhöfel

Publikováno v: Lecture Notes in Computer Science ISBN: 9783030388072
DaLí

We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its usefulness, we formalize several program verification problems in it: Functional Verification, Information Flow Analysis,

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a86af292b632b5f35552609881dd7b01
https://doi.org/10.1007/978-3-030-38808-9_8

Verifying OpenJDK’s Sort Method for Generic Collections

Autor: Reiner Hähnle, Richard Bubel, Stijn de Gouw, Dominic Steinhöfel, Frank S. de Boer, Jurriaan Rot

Publikováno v: Journal of Automated Reasoning, 62, 1, pp. 93-126
Journal of Automated Reasoning, 62(1), 93-126. Springer Netherlands
Journal of Automated Reasoning
Gouw, S D, Boer, F S D, Bubel, R, Hähnle, R, Rot, J & Steinhöfel, D 2019, ' Verifying OpenJDK's Sort Method for Generic Collections ', Journal of Automated Reasoning, vol. 62, no. 1, pp. 93-126 . https://doi.org/10.1007/s10817-017-9426-4
Journal of Automated Reasoning, 62, 93-126

TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9fa6d2c180bec44115d99b239730afce
https://doi.org/10.1007/s10817-017-9426-4

Modular, Correct Compilation with Automatic Soundness Proofs

Autor: Dominic Steinhöfel, Reiner Hähnle

Publikováno v: Leveraging Applications of Formal Methods, Verification and Validation. Modeling ISBN: 9783030034177
ISoLA (1)

Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9b9d5fcd6003d86e1219eb0ade4fbdf2
https://doi.org/10.1007/978-3-030-03418-4_25