Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection

DOI10.1007/978-3-319-15075-8_7MaRDI QIDQ2797866zbMATH OpenOpenAlexFDO

Authors Grigory Fedyukovich, Natasha Sharygina

Publication date 1 April 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-15075-8_7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• On the magnitude of completeness thresholds in bounded model checking
• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
• scientific article; zbMATH DE number 1796143
• scientific article; zbMATH DE number 2080052
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• scientific article; zbMATH DE number 1692938
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Bounded model checking of recursive programs with pointers in K

Cited in

(1)

• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

Describes a project that uses

Uses Software

• ESBMC
• eVolCheck
• LLBMC
• PeRIPLO
• FunFrog
• PVS

This page was built for publication: Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection

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