Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME System

Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided program specialization methodology for efficiently imposing safety properties on software systems. The program specializer takes as input a set A of logical assertions that specifies the expected system behavior plus a software system that is modeled as a Maude program R that may violate some of the assertions in A. The outcome is a safe refinement R▹ of R in which every system computation is a good run of R, i.e., it satisfies the assertions in A. The specialization technique has been fully automated in the ÁTAME system and ensures that no good run of R is removed from R▹, while the number of bad runs is reduced to zero. The efficiency and scalability of our technique is empirically demonstrated by means of a thorough experimental evaluation of the ÁTAME system, which shows fast specialization times and good performance of the computed specializations, even for large assertion sets.