Under-approximating loops in C programs for fast counterexample detection

DOI10.1007/S10703-015-0228-1MaRDI QIDQ746774zbMATH OpenOpenAlexWikidataFDO

Authors D. Kharzeev

Publication date 20 October 2015

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10703-015-0228-1

zbMATH Keywords

model checkingcounterexamplesunderapproximationloop acceleration

Mathematics Subject Classification ID

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

Recommendations

• Loop Invariants from Counterexamples
• Proving safety with trace automata and bounded model checking
• Making the most of BMC counterexamples
• From under-approximations to over-approximations and back
• Leaping Loops in the Presence of Abstraction

Cites work

• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• Accelerating interpolants
• Lazy Abstraction with Interpolants
• Lazy abstraction
• Loop Summarization Using Abstract Transformers
• Precise reasoning for programs using containers
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification and falsification of programs with loops using predicate abstraction

Cited in

(9)

• Proving safety with trace automata and bounded model checking
• Underapproximation for Model-Checking Based on Random Cryptographic Constructions
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Incremental bounded model checking for embedded software
• Transition power abstractions for deep counterexample detection
• On the complexity of the quantified bit-vector arithmetic with binary encoding
• A calculus for modular loop acceleration
• Lower runtime bounds for integer programs
• From under-approximations to over-approximations and back

Describes a project that uses

Uses Software

• CBMC

This page was built for publication: Under-approximating loops in C programs for fast counterexample detection

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