{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:34:20Z","timestamp":1781238860321,"version":"3.54.1"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603011","type":"proceedings-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T01:33:52Z","timestamp":1546997632000},"page":"1-9","source":"Crossref","is-referenced-by-count":37,"title":["Solving Constrained Horn Clauses Using Syntax and Data"],"prefix":"10.23919","author":[{"given":"Grigory","family":"Fedyukovich","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sumanth","family":"Prabhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kumar","family":"Madhukar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref12","first-page":"574","article-title":"A data driven approach for algebraic loop invariants","author":"sharma","year":"2013","journal-title":"ESOP Volume 7792 of LNCS"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039704"},{"key":"ref14","first-page":"500","article-title":"Houdini: an Annotation Assistant for ESC\/Java","author":"flanagan","year":"2001","journal-title":"FME vol 2021 of LNCS"},{"key":"ref15","first-page":"300","article-title":"Incremental verification of compiler optimizations","author":"fedyukovich","year":"2014","journal-title":"NFM vol 8430 of LNCS"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_11"},{"key":"ref17","first-page":"606","article-title":"Automated discovery of simulation between programs","author":"fedyukovich","year":"2015","journal-title":"LPAR vol 9450 of LNCS"},{"key":"ref18","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"TACAS Volume 4963 of LNCS"},{"key":"ref19","doi-asserted-by":"crossref","DOI":"10.21105\/joss.00026","article-title":"Armadillo: a template-based c++ library for linear algebra","author":"sanderson","year":"2016","journal-title":"Open Source Software"},{"key":"ref4","first-page":"17","article-title":"SMT-Based Model Checking for Recursive Programs","author":"komuravelli","year":"2014","journal-title":"CAV vol 8559 of LNCS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"ref6","first-page":"261","article-title":"Rahft: A tool for verifying Horn clauses using abstract interpretation and finite tree automata","author":"kafle","year":"2016","journal-title":"CAV Part I vol 9779 of LNCS"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_10"},{"key":"ref8","first-page":"251","article-title":"Accelerating Syntax-Guided Invariant Synthesis","author":"fedyukovich","year":"2018","journal-title":"TACAS Part I vol 10805 of LNCS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"ref2","first-page":"247","article-title":"A verification toolkit for numerical transition systems - tool paper","author":"hojjat","year":"2012","journal-title":"FM volume 7436 of LNCS"},{"key":"ref1","first-page":"157","article-title":"Generalized property directed reachability","author":"hoder","year":"2012","journal-title":"SAT vol 7317 of LNCS"},{"key":"ref9","article-title":"Efficiently learning safety proofs from appearance as well as behaviours","author":"prabhu","year":"2018","journal-title":"SAS LNCS"},{"key":"ref20","first-page":"443","article-title":"Inductive invariant generation via abductive inference","author":"dillig","year":"2013","journal-title":"OOPSLA"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"ref24","first-page":"88","article-title":"From invariant checking to invariant inference using randomized search","author":"sharma","year":"2014","journal-title":"CAV vol 8559 of LNCS"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1145\/2837614.2837664","article-title":"Learning invariants using decision trees and implication counterexamples","author":"garg","year":"2016","journal-title":"POPL"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603011.pdf?arnumber=8603011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,25]],"date-time":"2022-01-25T23:55:08Z","timestamp":1643154908000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603011\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":24,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603011","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}