Assertion-based Analysis via Slicing with ABETS (System Description)

TL;DR

ABETS is a dynamic analysis tool for Maude programs that uses assertion-based slicing and runtime checks to diagnose bugs, automatically generate fixes, and improve debugging efficiency.

Contribution

The paper introduces ABETS, a novel assertion-based analysis system that combines slicing, runtime assertion checking, and automated repair for Maude programs.

Findings

Effective bug diagnosis through assertion-based slicing

Automated generation of program fixes when invariants are violated

Experimental results demonstrate system performance and effectiveness

Abstract

We present ABETS, an assertion-based, dynamic analyzer that helps diagnose errors in Maude programs. ABETS uses slicing to automatically create reduced versions of both a run's execution trace and executed program, reduced versions in which any information that is not relevant to the bug currently being diagnosed is removed. In addition, ABETS employs runtime assertion checking to automate the identification of bugs so that whenever an assertion is violated, the system automatically infers accurate slicing criteria from the failure. We summarize the main services provided by ABETS, which also include a novel assertion-based facility for program repair that generates suitable program fixes when a state invariant is violated. Finally, we provide an experimental evaluation that shows the performance and effectiveness of the system. This paper is under consideration for publication in TPLP.