M.N.: Integration of a software model checker into Isabelle

Abstract. The paper presents a combination of interactive and auto-matic tools in the area of software verification. We have integrated a newly developed software model checker into an interactive verification environment for imperative programming languages. Although the prob-lems in software verification are mostly too hard for full automation, we could increase the level of automated assistance by discharging less in-teresting side conditions. That allows the verification engineer to focus on the abstract algorithm, safely assuming unbounded arithmetic and unlimited buffers.