DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs

Williame Rocha, Herbert Rocha, Hussama Ismail, Lucas Cordeiro, Bernd Fischer

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

117 Downloads (Pure)


DepthK is a software verification tool that employs a proof by induction algorithm that combines k-induction with invariant inference. In order to efficiently and effectively verify and falsify safety properties in C programs, DepthK infers program invariants using polyhedral constraints. Experimental results show that our approach can handle a wide variety of safety properties in several intricate verification tasks.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, PT II
Number of pages4
Publication statusPublished - 2017

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs'. Together they form a unique fingerprint.

Cite this