Proving safety with trace automata and bounded model checking

DOI10.1007/978-3-319-19249-9_21zbMATH Open1427.68047arXiv1410.5764OpenAlexW2963707299WikidataQ62040429 ScholiaQ62040429MaRDI QIDQ5206955FDOQ5206955

Authors:

Publication date: 19 December 2019

Published in: FM 2015: Formal Methods (Search for Journal in Brave)

Abstract: Loop under-approximation is a technique that enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up the detection of bugs significantly, it introduces redundant execution traces which may complicate the verification of the program. This holds particularly true for verification tools based on Bounded Model Checking, which incorporate simplistic heuristics to determine whether all feasible iterations of a loop have been considered. We present a technique that uses emph{trace automata} to eliminate redundant executions after performing loop acceleration. The method reduces the diameter of the program under analysis, which is in certain cases sufficient to allow a safety proof using Bounded Model Checking. Our transformation is precise---it does not introduce false positives, nor does it mask any errors. We have implemented the analysis as a source-to-source transformation, and present experimental results showing the applicability of the technique.

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

Recommendations

• Under-approximating loops in C programs for fast counterexample detection
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Computing over-approximations with bounded model checking
• Programming Languages and Systems
• Scaling bounded model checking by transforming programs with arrays

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Fluid updates: beyond strong vs. weak updates
• Title not available (Why is that?)
• Lazy Abstraction with Interpolants
• Accelerating interpolants
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Fast acceleration of ultimately periodic relations
• Title not available (Why is that?)
• Refinement of Trace Abstraction
• Under-approximating loops in C programs for fast counterexample detection
• Verification and falsification of programs with loops using predicate abstraction
• Proving safety with trace automata and bounded model checking

Cited In (6)

• Application of the trace assertion method to the specification, design, and verification of automaton programs
• Finite Models vs Tree Automata in Safety Verification
• Proving nondeterministically specified safety properties using progress measures
• Proving safety with trace automata and bounded model checking
• Under-approximating loops in C programs for fast counterexample detection
• Proving Safety Properties of Rewrite Theories

This page was built for publication: Proving safety with trace automata and bounded model checking

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