Under-approximating loops in C programs for fast counterexample detection

DOI10.1007/s10703-015-0228-1zbMath1322.68054OpenAlexW1977456312WikidataQ38366581 ScholiaQ38366581MaRDI QIDQ746774

D. Kharzeev

Publication date: 20 October 2015

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

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

zbMATH Keywords

model checkingcounterexamplesunderapproximationloop acceleration

Mathematics Subject Classification ID

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

Related Items

A Calculus for Modular Loop Acceleration, Incremental bounded model checking for embedded software, On the complexity of the quantified bit-vector arithmetic with binary encoding, Proving Safety with Trace Automata and Bounded Model Checking, Lower Runtime Bounds for Integer Programs, Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)

Uses Software

• CBMC

Cites Work

• Unnamed Item
• Verification and falsification of programs with loops using predicate abstraction
• Loop Summarization Using Abstract Transformers
• Accelerating Interpolants
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Precise reasoning for programs using containers
• Lazy Abstraction with Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems