[{"date_created":"2022-03-21T08:03:30Z","corr_author":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems","oa_version":"Published Version","status":"public","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2012-03-24","location":"Tallinn, Estonia","end_date":"2012-04-01"},"type":"conference","alternative_title":["LNCS"],"day":"01","intvolume":"      7214","publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642287558"],"eisbn":["9783642287565"],"issn":["0302-9743"]},"_id":"10906","scopus_import":"1","ddc":["000"],"editor":[{"last_name":"Flanagan","first_name":"Cormac","full_name":"Flanagan, Cormac"},{"first_name":"Barbara","last_name":"König","full_name":"König, Barbara"}],"doi":"10.1007/978-3-642-28756-5_46","citation":{"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.","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>","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.","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.","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>","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>."},"volume":7214,"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","place":"Berlin, Heidelberg","department":[{"_id":"ToHe"}],"article_processing_charge":"No","title":"HSF(C): A software verifier based on Horn clauses","date_updated":"2026-06-18T10:45:24Z","series_title":"LNCS","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"author":[{"full_name":"Grebenshchikov, Sergey","last_name":"Grebenshchikov","first_name":"Sergey"},{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"first_name":"Nuno P.","last_name":"Lopes","full_name":"Lopes, Nuno P."},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"}],"date_published":"2012-04-01T00:00:00Z","abstract":[{"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.","lang":"eng"}],"publisher":"Springer","year":"2012","month":"04","page":"549-551","language":[{"iso":"eng"}],"oa":1}]