Incremental bounded model checking for embedded software

DOI10.1007/s00165-017-0419-1zbMath1375.68081arXiv1409.5872OpenAlexW2588551419WikidataQ59528027 ScholiaQ59528027MaRDI QIDQ1682291

Daniel Kroening, Ruben Martins, Martin Brain, Peter Schrammel, Tom Bienmüller, Tino Teige

Publication date: 29 November 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

embedded systemsbounded model checking\(k\)-inductionincremental SAT solving

Mathematics Subject Classification ID

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

Related Items (1)

Incremental design-space model checking via reusable reachable state approximations

Uses Software

• Boolector
• MiniSat
• SATIRE
• KLEE
• PicoSAT
• SystemC
• StarExec
• CBMC
• NModel

Cites Work

• Under-approximating loops in C programs for fast counterexample detection
• Linear Completeness Thresholds for Bounded Model Checking
• Query-Driven Program Testing
• Solving the incremental satisfiability problem
• Random time evolution and direct integrals: Constants of the motion and the mass operator
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• Deciding Bit-Vector Arithmetic with Abstraction
• Bounded model checking using satisfiability solving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Incremental bounded model checking for embedded software