Proving safety with trace automata and bounded model checking

DOI10.1007/978-3-319-19249-9_21MaRDI QIDQ5206955zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 19 December 2019

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

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

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)

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.

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

Cites work

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

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)