Establishing a holistic landscape of theories and tools for reliable Software Reengineering processes is the long-term goal of Dominic Steinhöfel, computer science researcher, formal methods enthusiast and tool developer. Dominic develops techniques for expressing and proving that program transformations do what they're supposed to do: Retaining original functionality, improving non-functional properties like resource consumption, or fix a bug, but nothing more.
Here, advances in the field of Software Reengineering will be presented, with a focus on, but no limited to, Dominic's original work.
This page is currently under construction. Stay tuned!
Abstract Execution: Automatically Proving Infinitely Many ProgramsTheory & Tooling for correctness proofs of program transformations(2020).PhD Thesis, Darmstadt University of Technology, GermanyWith Abstract Execution, an implemented specification and verification framework for schematic programs, in particular program transformations, and Model Trace Logic, a specification framework that can be used to express interesting properties of, e.g., program evolution, this thesis provides theoretic and practical building blocks for safe Software Reengineering. The thesis presents REFINITY, a workbench for encoding and proving Java program transformations on statement level. REFINITY is used to prove conditional correctness of well-known code refactoring rules, for which so far undocumented safety preconditions are extracted.
Abstract ExecutionAutomatic correctness proofs of program transformations(2019).Proc. Third World Congress on Formal Methods - The Next 30 Years, (FM)Abstract Execution (AE) is an extension of Symbolic Execution for the analysis of schematic programs containing placeholder symbols representing unknown statements or expressions. By an encoding of program transformation rules (on statement level) as pairs of schematic programs, AE can reason about the conditional correctness of program transformation techniques. For example, one can prove that code refactoring techniques preserve behavior, given that certain preconditions are met. AE proofs are highly automated: In many cases, proofs run through fully automatically.
Perspectives on Legacy System ReengineeringEarly paper on the nature of Software ReengineeringScott R. Tilley and Dennis Smith(1995).White Paper, Carnegie Mellon University, Software Engineering InstituteThis report regards the field of Software Reengineering from six different viewpoints: From an engineering perspective, a system perspective, a software perspective, a managerial perspective, an evolutionary perspective, and a maintanance perspective. It provides a usable definition of Software Reengineering: "Reengineering is the systematic transformation of an existing system into a new form to realize quality improvements in operation, system capability, functionality, performance, or evolvability at a lower cost, schedule, or risk to the customer."