DepthK: A k-induction verifier based on invariant inference for C programs
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. Experiment...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer, Berlin, Heidelberg
2017
|
| _version_ | 1797071539378585600 |
|---|---|
| author | Rocha, W Rocha, H Ismail, H Cordeiro, L Fischer, B |
| author_facet | Rocha, W Rocha, H Ismail, H Cordeiro, L Fischer, B |
| author_sort | Rocha, W |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T22:54:45Z |
| format | Conference item |
| id | oxford-uuid:5ffb466b-4645-49a4-954c-5edb64e88a85 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:54:45Z |
| publishDate | 2017 |
| publisher | Springer, Berlin, Heidelberg |
| record_format | dspace |
| spelling | oxford-uuid:5ffb466b-4645-49a4-954c-5edb64e88a852022-03-26T17:50:31ZDepthK: A k-induction verifier based on invariant inference for C programsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:5ffb466b-4645-49a4-954c-5edb64e88a85Symplectic Elements at OxfordSpringer, Berlin, Heidelberg2017Rocha, WRocha, HIsmail, HCordeiro, LFischer, BDepthK 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. |
| spellingShingle | Rocha, W Rocha, H Ismail, H Cordeiro, L Fischer, B DepthK: A k-induction verifier based on invariant inference for C programs |
| title | DepthK: A k-induction verifier based on invariant inference for C programs |
| title_full | DepthK: A k-induction verifier based on invariant inference for C programs |
| title_fullStr | DepthK: A k-induction verifier based on invariant inference for C programs |
| title_full_unstemmed | DepthK: A k-induction verifier based on invariant inference for C programs |
| title_short | DepthK: A k-induction verifier based on invariant inference for C programs |
| title_sort | depthk a k induction verifier based on invariant inference for c programs |
| work_keys_str_mv | AT rochaw depthkakinductionverifierbasedoninvariantinferenceforcprograms AT rochah depthkakinductionverifierbasedoninvariantinferenceforcprograms AT ismailh depthkakinductionverifierbasedoninvariantinferenceforcprograms AT cordeirol depthkakinductionverifierbasedoninvariantinferenceforcprograms AT fischerb depthkakinductionverifierbasedoninvariantinferenceforcprograms |