Under-approximating loops in C programs for fast counterexample detection
DOI10.1007/S10703-015-0228-1zbMATH Open1322.68054OpenAlexW1977456312WikidataQ38366581 ScholiaQ38366581MaRDI QIDQ746774FDOQ746774
Authors: 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Lazy Abstraction with Interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
- Accelerating interpolants
- Lazy abstraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Precise reasoning for programs using containers
- Loop Summarization Using Abstract Transformers
- Verification and falsification of programs with loops using predicate abstraction
Cited In (9)
- Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
- On the complexity of the quantified bit-vector arithmetic with binary encoding
- Lower runtime bounds for integer programs
- A calculus for modular loop acceleration
- Proving safety with trace automata and bounded model checking
- Incremental bounded model checking for embedded software
- Transition power abstractions for deep counterexample detection
- From under-approximations to over-approximations and back
- Underapproximation for Model-Checking Based on Random Cryptographic Constructions
Uses Software
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)
