{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:51Z","timestamp":1750220091185,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE1565478"],"award-info":[{"award-number":["DGE1565478"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,18]]},"DOI":"10.1145\/3524482.3527655","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"102-112","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Computing program functions"],"prefix":"10.1145","author":[{"given":"Hessamaldin","family":"Mohammadi","sequence":"first","affiliation":[{"name":"New Jersey Institute of Technology"}]},{"given":"Wided","family":"Ghardallou","sequence":"additional","affiliation":[{"name":"University of Sousse"}]},{"given":"Richard C","family":"Linger","sequence":"additional","affiliation":[{"name":"Assurance Labs"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6578-5510","authenticated-orcid":false,"given":"Ali","family":"Mili","sequence":"additional","affiliation":[{"name":"New Jersey Institute of Technology"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings, FASE","author":"Aguirre Nazareno","year":"2009","unstructured":"Nazareno Aguirre , Marcelo F. Frias , Mariano M. Moscato , T.S.E. Maibaum , and Alan Wassyng . 2009 . Describing and Analyzing Behaviors over Tabular Specifications Unsing DynAlloy . In Proceedings, FASE 2009. 155--170. Nazareno Aguirre, Marcelo F. Frias, Mariano M. Moscato, T.S.E. Maibaum, and Alan Wassyng. 2009. Describing and Analyzing Behaviors over Tabular Specifications Unsing DynAlloy. In Proceedings, FASE 2009. 155--170."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1016\/j.entcs.2010.09.002"},{"volume-title":"Relational Methods in Computer Science","author":"Brink Chris","unstructured":"Chris Brink , Wolfram Kahl , and Gunther Schmidt . 1997. Relational Methods in Computer Science . Springer Verlag , Berlin, Germany . Chris Brink, Wolfram Kahl, and Gunther Schmidt. 1997. Relational Methods in Computer Science. Springer Verlag, Berlin, Germany.","key":"e_1_3_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings, International Conference on Theoretical Aspects of Computing","volume":"3407","author":"Rodriguez Carbonnell E.","year":"2004","unstructured":"E. Rodriguez Carbonnell and Deepak Kapur . 2004 . Program Verification Using Automatic Generation of Invariants . In Proceedings, International Conference on Theoretical Aspects of Computing 2004, Vol. 3407 . Lecture Notes in Computer Science, Springer Verlag, 325--340. E. Rodriguez Carbonnell and Deepak Kapur. 2004. Program Verification Using Automatic Generation of Invariants. In Proceedings, International Conference on Theoretical Aspects of Computing 2004, Vol. 3407. Lecture Notes in Computer Science, Springer Verlag, 325--340."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings, CAV","volume":"2725","author":"Colon M.","year":"2003","unstructured":"M. Colon , S. Sankaranarayanan , and H. Sipma . 2003. Linear Invariant Generation Using Non-Linear Constraint Solving . In Proceedings, CAV 2003 , Vol. 2725 . M. Colon, S. Sankaranarayanan, and H. Sipma. 2003. Linear Invariant Generation Using Non-Linear Constraint Solving. In Proceedings, CAV 2003, Vol. 2725."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings, Computer Aided Verification, CAV 2003 (Lecture Notes in Computer Science)","volume":"2725","author":"Colon M. A.","unstructured":"M. A. Colon , S. Sankaranarayana , and H. B. Sipma . 2003. Linear Invariant Generation Using Non Linear Constraint Solving . In Proceedings, Computer Aided Verification, CAV 2003 (Lecture Notes in Computer Science) , Vol. 2725 . Springer Verlag, 420--432. M. A. Colon, S. Sankaranarayana, and H. B. Sipma. 2003. Linear Invariant Generation Using Non Linear Constraint Solving. In Proceedings, Computer Aided Verification, CAV 2003 (Lecture Notes in Computer Science), Vol. 2725. Springer Verlag, 420--432."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/800228.806926"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1016\/j.jlamp.2018.02.001"},{"key":"e_1_3_2_1_10_1","volume-title":"Blary and M. Chechik (Eds.)","volume":"9971","author":"Dockins R","unstructured":"R Dockins , A. Foltzer , J. Hendrix , B. Huffman , D. McNamee , and A. Tomb . 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In VSTTE: Verified Software Theories, Tools and Experiments, S . Blary and M. Chechik (Eds.) , Vol. 9971 . Springer Verlag LNCS. R Dockins, A. Foltzer, J. Hendrix, B. Huffman, D. McNamee, and A. Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In VSTTE: Verified Software Theories, Tools and Experiments, S. Blary and M. Chechik (Eds.), Vol. 9971. Springer Verlag LNCS."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1016\/j.scico.2007.01.015"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1109\/32.908957"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1007\/978-3-030-45190-5_12"},{"key":"e_1_3_2_1_14_1","volume-title":"Automated Discovery of Loop Invariants for High Assurance Programs Synthesized Using AI Planning Techniques. In HASE 2008: 11th High Assurance Systems Engineering Symposium (December 3--5)","author":"Fu JiCheng","year":"2008","unstructured":"JiCheng Fu , Farokh B. Bastani , and I- Ling Yen . 2008 . Automated Discovery of Loop Invariants for High Assurance Programs Synthesized Using AI Planning Techniques. In HASE 2008: 11th High Assurance Systems Engineering Symposium (December 3--5) . Nanjing, China, 333--342. JiCheng Fu, Farokh B. Bastani, and I-Ling Yen. 2008. Automated Discovery of Loop Invariants for High Assurance Programs Synthesized Using AI Planning Techniques. In HASE 2008: 11th High Assurance Systems Engineering Symposium (December 3--5). Nanjing, China, 333--342."},{"key":"e_1_3_2_1_15_1","volume-title":"Furia and Bertrand Meyer","author":"Carlo","year":"2010","unstructured":"Carlo A. Furia and Bertrand Meyer . 2010 . Inferring Loop Invariants using Post-conditions. In Festschrift in honor of Yuri Gurevich's 70th birthday (Lecture Notes in Computer Science), Nachum Dershowitz (Ed.). Springer-Verlag . Carlo A. Furia and Bertrand Meyer. 2010. Inferring Loop Invariants using Post-conditions. In Festschrift in honor of Yuri Gurevich's 70th birthday (Lecture Notes in Computer Science), Nachum Dershowitz (Ed.). Springer-Verlag."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1016\/j.jlap.2012.04.001"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings, Workshop on Invariant Generation: WING","author":"Gulwani Sumit","year":"2010","unstructured":"Sumit Gulwani . 2010 . Invited Talk: Methods for Loop Invariant Generation . In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK. Sumit Gulwani. 2010. Invited Talk: Methods for Loop Invariant Generation. In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings, FMCAD.","author":"Hassan Zyad","year":"2013","unstructured":"Zyad Hassan , Aaron R. Bradley , and Fabio Somenzi . 2013 . Better Generaliation in IC3 . In Proceedings, FMCAD. Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi. 2013. Better Generaliation in IC3. In Proceedings, FMCAD."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1007\/978-3-540-89439-1_24"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings, Workshop on Invariant Generation: WING","author":"Iosif Radu","year":"2010","unstructured":"Radu Iosif , Marius Bozga , Filip Konecny , and Tomas Vojnar . 2010 . Tool Demonstration for the FLATA Counter Automata Toolset . In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK. Radu Iosif, Marius Bozga, Filip Konecny, and Tomas Vojnar. 2010. Tool Demonstration for the FLATA Counter Automata Toolset. In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK."},{"key":"e_1_3_2_1_23_1","first-page":"184","article-title":"Tabular representations in relational documents. In Relational Methods in Computer Science, Ch. Brink, W. Kahl, and G. Schmidt (Eds.). Springer Verlag","volume":"12","author":"Janicki R.","year":"1997","unstructured":"R. Janicki , D. L. Parnas , and J. Zucker . 1997 . Tabular representations in relational documents. In Relational Methods in Computer Science, Ch. Brink, W. Kahl, and G. Schmidt (Eds.). Springer Verlag , Chapter 12 , 184 -- 196 . R. Janicki, D. L. Parnas, and J. Zucker. 1997. Tabular representations in relational documents. In Relational Methods in Computer Science, Ch. Brink, W. Kahl, and G. Schmidt (Eds.). Springer Verlag, Chapter 12, 184--196.","journal-title":"Chapter"},{"volume-title":"Tabular Representations in Relational Documents","author":"Janicki Ryszard","unstructured":"Ryszard Janicki , David L Parnas , and Jeffrey Zucker . 2001. Tabular Representations in Relational Documents . In Software Fundamentals, Daniel M. Hoffman and David M. Weiss (Eds.). Addison Wesley , Chapter 4. Ryszard Janicki, David L Parnas, and Jeffrey Zucker. 2001. Tabular Representations in Relational Documents. In Software Fundamentals, Daniel M. Hoffman and David M. Weiss (Eds.). Addison Wesley, Chapter 4.","key":"e_1_3_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1007\/s11334-012-0189-0"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1016\/j.jsc.2012.04.001"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1109\/SYNASC.2009.66"},{"volume-title":"Proceedings, CAV 2010: 22nd International Conference on Computer Aided Verification","author":"Kroening Daniel","unstructured":"Daniel Kroening , Natasha Sharyngina , Aliaksei Tsitovitch , and Christoph M. Wintersteiger . 2010. Termination Analysis with Compositional Transition Invariants . In Proceedings, CAV 2010: 22nd International Conference on Computer Aided Verification . Edinburg, UK. Daniel Kroening, Natasha Sharyngina, Aliaksei Tsitovitch, and Christoph M. Wintersteiger. 2010. Termination Analysis with Compositional Transition Invariants. In Proceedings, CAV 2010: 22nd International Conference on Computer Aided Verification. Edinburg, UK.","key":"e_1_3_2_1_29_1"},{"volume-title":"Proceedings, VMCAI. 267--281","author":"Lahiri S.K.","unstructured":"S.K. Lahiri and R.E. Bryant . 2004. Constructing Quantified Invariants via Predicate Abstraction . In Proceedings, VMCAI. 267--281 . S.K. Lahiri and R.E. Bryant. 2004. Constructing Quantified Invariants via Predicate Abstraction. In Proceedings, VMCAI. 267--281.","key":"e_1_3_2_1_30_1"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings, Workshop on Invariant Generation: WING","author":"Maclean Ewen","year":"2010","unstructured":"Ewen Maclean , Andrew Ireland , and Gudmund Grov . 2010 . Synthesizing Functional Invariants in Separation Logic . In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK. Ewen Maclean, Andrew Ireland, and Gudmund Grov. 2010. Synthesizing Functional Invariants in Separation Logic. In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"e_1_3_2_1_33_1","volume-title":"Reflexive Transitive Loop Invariants: A Basis for Computing Loop Functions. In First International Workshop on Invariant Generation","author":"Mili A.","year":"2007","unstructured":"A. Mili . 2007 . Reflexive Transitive Loop Invariants: A Basis for Computing Loop Functions. In First International Workshop on Invariant Generation . Hagenberg, Austria. A. Mili. 2007. Reflexive Transitive Loop Invariants: A Basis for Computing Loop Functions. In First International Workshop on Invariant Generation. Hagenberg, Austria."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1016\/j.scico.2012.05.006"},{"doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In LICS. 32--41.  Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In LICS. 32--41.","key":"e_1_3_2_1_36_1","DOI":"10.1109\/LICS.2004.1319598"},{"doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2011. Transition Invariants and Transition Predicate Abstraction for Program Termination. In TACAS. 3--10.  Andreas Podelski and Andrey Rybalchenko. 2011. Transition Invariants and Transition Predicate Abstraction for Program Termination. In TACAS. 3--10.","key":"e_1_3_2_1_37_1","DOI":"10.1007\/978-3-642-19835-9_2"},{"key":"e_1_3_2_1_38_1","first-page":"381","article-title":"Non Linear Loop Invariant Generation Using Groebner Bases. In Proceedings, ACM SIGPLAN Principles of Programming Languages","volume":"2004","author":"Sankaranarayanan S.","year":"2004","unstructured":"S. Sankaranarayanan , H. B. Sipma , and Z. Manna . 2004 . Non Linear Loop Invariant Generation Using Groebner Bases. In Proceedings, ACM SIGPLAN Principles of Programming Languages , POPL 2004. 381 -- 329 . S. Sankaranarayanan, H. B. Sipma, and Z. Manna. 2004. Non Linear Loop Invariant Generation Using Groebner Bases. In Proceedings, ACM SIGPLAN Principles of Programming Languages, POPL 2004. 381--329.","journal-title":"POPL"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1145\/3385412.3386014"},{"volume-title":"Proceedings, 8th International Workshop on Logic Based Program Synthesis and Transformation","author":"Stark J.","unstructured":"J. Stark and A. Ireland . 1998. Invariant Discovery via failed Proof Attempts . In Proceedings, 8th International Workshop on Logic Based Program Synthesis and Transformation . Manchester, UK. J. Stark and A. Ireland. 1998. Invariant Discovery via failed Proof Attempts. In Proceedings, 8th International Workshop on Logic Based Program Synthesis and Transformation. Manchester, UK.","key":"e_1_3_2_1_40_1"},{"volume-title":"Proceedings, PLDI.","author":"Torlak E.","unstructured":"E. Torlak and R. Bodik . 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages . In Proceedings, PLDI. E. Torlak and R. Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Proceedings, PLDI.","key":"e_1_3_2_1_41_1"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings, Workshop on Invariant Generation: WING","author":"Zuleger Florian","year":"2010","unstructured":"Florian Zuleger and Moritz Sinn . 2010 . LOOPUS: A Tool for Computing Loop Bounds for C Programs . In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK. Florian Zuleger and Moritz Sinn. 2010. LOOPUS: A Tool for Computing Loop Bounds for C Programs. In Proceedings, Workshop on Invariant Generation: WING 2010. Edimburg, UK."}],"event":{"sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"acronym":"FormaliSE '22","name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","location":"Pittsburgh Pennsylvania"},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527655","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527655","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527655","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:51Z","timestamp":1750183791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":39,"alternative-id":["10.1145\/3524482.3527655","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527655","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}