SAGE: Profiling and Optimization in Formal Methods

Abstract

The quality and the correctness of software are often the greatest concern in electronic systems. Formal methods techniques and tools provide a guarantee that a design of software system is free of specific flaws. This paper discusses an open source mathematical software system SAGE, which combines and extends program analysis, testing, verification, model checking, and automated theorem proving techniques. Then we concentrate on profiling and optimization techniques in analysis and design phase of software systems in SAGE. In today's programming world optimization plays a vital role. It is an on-going, non-functional requirement that affects all stages in the development of a system, from analysis and design through development and implementation. Profiling refers to analysis of the relative execution time spent in different parts of the program. Finally, we describe various optimization techniques.