--- _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. Tools and Algorithms for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46' apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46' chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-28756-5_46.' ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms for the Construction and Analysis of Systems, 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.” Tools and Algorithms for the Construction and Analysis of Systems, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:10.1007/978-3-642-28756-5_46.' 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' ...