{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:09Z","timestamp":1740109089424,"version":"3.37.3"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Grantov\u00e1 Agentura \u010cesk\u00e9 Republiky (CZ)","award":["14-11384S"],"award-info":[{"award-number":["14-11384S"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>During explicit software model checking, the tools spend a lot of time in state matching. This is implied not only by processing a huge number of states, but also by the fact that state representation is usually not small either. In this article, we present two dead variable analyses; applying them during the code-model-checking process results in size reduction of both state representation and explored state space itself. We implemented the analyses inside Java PathFinder and evaluate their impact in terms of memory and time reduction using several non-trivial benchmarks.<\/jats:p>","DOI":"10.1007\/s00165-016-0413-z","type":"journal-article","created":{"date-parts":[[2017,1,23]],"date-time":"2017-01-23T07:17:16Z","timestamp":1485155836000},"page":"777-803","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On partial state matching"],"prefix":"10.1145","volume":"29","author":[{"given":"Pavel","family":"Jan\u010d\u00edk","sequence":"first","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University, Malostranske namesti 25, 118 00, Praha 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-4812","authenticated-orcid":false,"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Physics, Charles University, Malostranske namesti 25, 118 00, Praha 1, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Ad\u00e1mek J et al (2006) Component reliability extensions for fractal component model. http:\/\/d3s.mff.cuni.cz\/software\/ft\/"},{"key":"e_1_2_1_2_2_2","unstructured":"Bruneton E et\u00a0al (2004) An open component model and its support in java. In: Crnkovic I Stafford JA Schmidt HW Wallnau KC (eds) CBSE LNCS vol 3054. Springer Berlin pp 7\u201322"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bozga M Fernandez J-C Ghirvu L (1999) State space reduction based on live variables analysis. In: Cortesi A Fil\u00e9 G (eds) Static analysis 6th international symposium SAS \u201999 Venice Italy September 22\u201324 1999 Proceedings. Lecture Notes in Computer Science vol 1694. Springer pp 164\u2013178","DOI":"10.1007\/3-540-48294-6_11"},{"volume-title":"Principles of model checking","year":"2008","author":"Christel B","key":"e_1_2_1_2_4_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Corbett JC et\u00a0al (2000) Bandera: extracting finite-state models from java source code. In: Ghezzi C Jazayeri M Wolf AL (eds) Proceedings of the 22nd International Conference on on Software Engineering ICSE 2000 Limerick Ireland June 4\u201311 2000. ACM pp 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_2_6_2","unstructured":"Concurrency tool comparison repository. https:\/\/facwiki.cs.byu.edu\/vv-lab\/index.php\/Concurrency_Tool_Comparison"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s12243-008-0067-9"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Doron P (1993) All from one one for all: on model checking using representatives. In: Proceedings of the 5th International Conference on Computer Aided Verification CAV \u201993. Springer-Verlag London pp 409\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00133-8"},{"volume-title":"The SPIN Model Checker\u2014primer and reference manual","year":"2004","author":"Holzmann GJ","key":"e_1_2_1_2_10_2"},{"issue":"40","key":"e_1_2_1_2_11_2","first-page":"1098","article-title":"A method for the construction of minimum-redundancy codes","volume":"9","author":"Huffman David A","year":"1952","journal-title":"Proc Inst Radio Eng"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Jan\u010d\u00edk P Kofro\u0148 J (2016) Dead variable analysis for multi-threaded heap manipulating programs. In: Proceedings of 31st ACM Symposium on Applied Computing. ACM","DOI":"10.1145\/2851613.2851826"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Lewis M Jones M (2006) A dead variable analysis for explicit model checking. In: Hatcliff J Tip F (eds) Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation Charleston South Carolina USA January 9\u201310 2006. ACM pp 48\u201357","DOI":"10.1145\/1111542.1111551"},{"key":"e_1_2_1_2_14_2","first-page":"357","article-title":"CoCoME in fractal","volume":"5153","author":"Lubom\u00edr B","year":"2007","journal-title":"LNCS"},{"key":"e_1_2_1_2_15_2","unstructured":"MURPHI Model Checker. http:\/\/formalverification.cs.utah.edu\/Murphi\/"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Nguyen VY Ruys TC (2009) Memoised garbage collection for software model checking. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin pp 201\u2013214","DOI":"10.1007\/978-3-642-00768-2_20"},{"key":"e_1_2_1_2_17_2","unstructured":"Parallel Java Benchmarks. https:\/\/bitbucket.org\/pag-lab\/pjbench"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Par\u00edzek P Lhot\u00e1k O (2011) Identifying future field accesses in exhaustive state space traversal. In: Alexander P Pasareanu CS Hosking JG (eds) 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011) Lawrence KS USA November 6\u201310 2011. IEEE Computer Society pp 93\u2013102","DOI":"10.1109\/ASE.2011.6100154"},{"issue":"4","key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1016\/j.scico.2014.10.008","article-title":"Model checking of concurrent programs with static analysis of field accesses","volume":"98","author":"Par\u00edzek P","year":"2015","journal-title":"Sci Comput Program"},{"key":"e_1_2_1_2_20_2","unstructured":"Pavel J Pavel P Jan K (2012) BeJC: checking compliance between java implementation and behavior specification. In: Proceedings of the 17th international doctoral symposium on components and architecture WCOP \u201912. ACM New York pp 31\u201336"},{"key":"e_1_2_1_2_21_2","unstructured":"Run-length encoding. https:\/\/en.wikipedia.org\/wiki\/Run-length_encoding"},{"key":"e_1_2_1_2_22_2","unstructured":"Self JP Mercer EG (2007) On-the-fly dynamic dead variable analysis. In: Bosnacki D Edelkamp S (eds) Model Checking Software 14th International SPIN Workshop Berlin Germany July 1\u20133 2007 Proceedings. Lecture Notes in Computer Science vol 4595. Springer pp 113\u2013130"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000033963.55470.9e"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0413-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0413-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0413-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0413-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:33Z","timestamp":1641538473000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0413-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-016-0413-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0413-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}