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)

Abstract

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
Pages360-364
Number of pages4
Volume10206
DOIs
Publication statusPublished - 2017

Publication series

NameLecture Notes in Computer Science

Fingerprint

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