---
_id: '10906'
abstract:
- lang: eng
  text: HSF(C) is a tool that automates verification of safety and liveness properties
    for C programs. This paper describes the verification approach taken by HSF(C)
    and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
  full_name: Grebenshchikov, Sergey
  last_name: Grebenshchikov
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Nuno P.
  full_name: Lopes, Nuno P.
  last_name: Lopes
- first_name: Corneliu
  full_name: Popeea, Corneliu
  last_name: Popeea
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
citation:
  ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
    verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg:
    Springer; 2012:549-551. doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>'
  apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko,
    A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38;
    B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of
    Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>'
  chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
    and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
    <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited
    by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
    2012. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>.'
  ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
    “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol.
    7214, pp. 549–551.'
  ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
    A software verifier based on Horn clauses. Tools and Algorithms for the Construction
    and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
    Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
  mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
    Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>,
    edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
    doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>.'
  short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
    C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
    of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
  end_date: 2012-04-01
  location: Tallinn, Estonia
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2012-03-24
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2023-09-05T14:09:54Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
  full_name: Flanagan, Cormac
  last_name: Flanagan
- first_name: Barbara
  full_name: König, Barbara
  last_name: König
intvolume: '      7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
  eisbn:
  - '9783642287565'
  eissn:
  - 1611-3349
  isbn:
  - '9783642287558'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7214
year: '2012'
...