Assertion-based analysis via slicing withABETS(system description)

DOI10.1017/S1471068416000375MaRDI QIDQ4593040zbMATH OpenOpenAlexWikidataFDO

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)

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

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)

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.

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

Cites work

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

Cited in

(7)

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

Describes a project that uses

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)