Assertion-based analysis via slicing withABETS(system description)

DOI10.1017/S1471068416000375zbMATH Open1379.68088arXiv1608.01433OpenAlexW2963227324WikidataQ57978108 ScholiaQ57978108MaRDI QIDQ4593040FDOQ4593040

Authors: María Alpuente, Francisco Frechina, Julia Sapiña, D. Ballis 

Publication date: 9 November 2017

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1608.01433

Recommendations

• Abstract program slicing: an abstract interpretation-based approach to program slicing
• Trace Abstraction-Based Verification for Uninterpreted Programs
• An automatic abstraction technique for verifying featured, parameterised systems
• Assertion-based slicing and slice graphs
• Cut branches before looking for bugs: certifiably sound verification on relaxed slices

zbMATH Keywords

rewriting logicMaudeprogram diagnosis and debuggingdynamic program and trace slicingruntime assertion checking

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20) Grammars and rewriting systems (68Q42)

Cites Work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Conditional rewriting logic as a unified model of concurrency
• Exploring conditional rewriting logic computations
• Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday
• A modular order-sorted equational generalization algorithm
• Debugging Maude programs via runtime assertion checking and trace slicing
• Specification, algebra, and software. Essays dedicated to Kokichi Futatsugi
• Built-in variant generation and unification, and their applications in Maude 2.7

Cited In (7)

• Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system
• Optimizing Maude programs via program specialization
• Debugging Maude programs via runtime assertion checking and trace slicing
• Inferring safe Maude programs with ÁTAME
• Symbolic analysis of Maude theories with Narval
• ABETS
• Combining runtime checking and slicing to improve Maude error diagnosis

Uses Software

• Maude

This page was built for publication: Assertion-based analysis via slicing withABETS(system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593040)