On Extensibility of Software Systems

This report contains the progress report written as part of the author's PhD qualifying exam. It describes initial work carried out in analyzing and improving the extensibility of software systems, including a detailed case study analyzing the extensibility of the Proof Obligation Generator (POG) of the Overture tool. Additional extension work includes improving the output format of the POG and support for additional logic systems. Future work for the remaining half of the PhD is also discussed, including ways to combine formal modelling and extensibility analysis and also techniques for multi-paradigm extensibility.