{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:01Z","timestamp":1751660521556},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290061"},{"type":"electronic","value":"9783030290078"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29007-8_5","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T23:10:06Z","timestamp":1566429006000},"page":"77-93","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Ilinva: Using Abduction to Generate Loop Invariants"],"prefix":"10.1007","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]},{"given":"Yanis","family":"Sellami","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"5_CR1","unstructured":"http:\/\/toccata.lri.fr\/gallery\/"},{"key":"5_CR2","unstructured":"http:\/\/pauillac.inria.fr\/~levy\/\/why3\/sorting\/"},{"key":"5_CR3","unstructured":"https:\/\/www.lri.fr\/~sboldo\/research.html"},{"key":"5_CR4","unstructured":"Invgen tool. \n                      http:\/\/pub.ist.ac.at\/agupta\/invgen\/"},{"key":"5_CR5","unstructured":"Neclabs NECLA verification benchmarks. \n                      http:\/\/www.nec-labs.com\/research\/system\/systemsSAV-website\/benchmarks.php"},{"key":"5_CR6","unstructured":"SATCONV benchmarks"},{"key":"5_CR7","unstructured":"Abdulot framework\/GPiD-Ilinva tool suite. \n                      https:\/\/github.com\/sellamiy\/GPiD-Framework"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, Nice (2007)","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4\u20134. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31424-7_4"},{"issue":"4\u20135","key":"5_CR10","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4\u20135), 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"5_CR12","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1997","unstructured":"Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1997)","edition":"1"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan,: Inductive invariant generation via abductive inference. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) Proceedings of OOPSLA 2013, Indianapolis, pp. 443\u2013456. ACM (2013)","DOI":"10.1145\/2544173.2509511"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-94205-6_19","volume-title":"Automated Reasoning","author":"M Echenim","year":"2018","unstructured":"Echenim, M., Peltier, N., Sellami, Y.: A generic framework for implicate generation modulo theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 279\u2013294. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94205-6_19"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 213\u2013224. ACM, New York (1999)","DOI":"10.1145\/302405.302467"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45251-6_29\n                      \n                    . Kindly provide volume number for Ref. [18]"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Logical Methods Comput. Sci. 6(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235\u2013239. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-44829-2_17"},{"issue":"10","key":"5_CR20","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11424-006-0307-x","volume":"19","author":"D Kapur","year":"2006","unstructured":"Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. J. Syst. Sci. Complex. 19, 307\u2013330 (2006)","journal-title":"J. Syst. Sci. Complex."},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/3022187","volume":"64","author":"A Karbyshev","year":"2017","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 71\u2013733 (2017)","journal-title":"J. ACM"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, 22\u201329 March 2009, pp. 470\u2013485 (2009)","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199\u2013213. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02959-2_17"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19, 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 217\u2013231 (2016)","DOI":"10.1145\/2837614.2837640"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Suzuki, N., Ishihata, K.: Implementation of an array bound checker (1977)","DOI":"10.21236\/ADA038191"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29007-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T23:12:40Z","timestamp":1566429160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29007-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290061","9783030290078"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29007-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.frocos2019.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}