{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T04:24:50Z","timestamp":1729657490486,"version":"3.28.0"},"reference-count":87,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1109\/ipdps.2006.1639580","type":"proceedings-article","created":{"date-parts":[[2006,7,10]],"date-time":"2006-07-10T15:59:56Z","timestamp":1152547196000},"page":"8 pp.","source":"Crossref","is-referenced-by-count":9,"title":["An overview of the Jahob analysis system: project goals and current status"],"prefix":"10.1109","author":[{"given":"V.","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"M.","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"Symbolic shape analysis","year":"2004","author":"wies","key":"79"},{"key":"78","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881918"},{"key":"77","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873645"},{"key":"35","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"journal-title":"Systematic Software Development Using VDM","year":"1986","author":"cliff","key":"36"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"34","article-title":"A micromodularity mechanism","author":"jackson","year":"2001","journal-title":"Proc ACM SIGSOFT Conf Foundations of Software Engineering \/ European Software Engineering Conference (FSE\/ESEC '01)"},{"journal-title":"A program verifier","year":"1970","author":"cornelius king","key":"39"},{"journal-title":"Program Flow Analysis Theory and Applications chapter Chapter 4 Flow Analysis and Optimization of LISP-like Structures","year":"1981","author":"jones","key":"37"},{"year":"0","key":"38"},{"key":"43","doi-asserted-by":"crossref","DOI":"10.1007\/11532231_20","article-title":"An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic","author":"kuncak","year":"2005","journal-title":"CADE Proceedings of 10th International Conference on Automated Deduction"},{"key":"42","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"40","article-title":"MONA implementation secrets","author":"klarlund","year":"2000","journal-title":"LNCS"},{"key":"82","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349313"},{"key":"83","doi-asserted-by":"crossref","DOI":"10.1007\/11690634_7","article-title":"A logic of reachable patterns in linked data-structures","author":"yorsh","year":"2006","journal-title":"Proc Foundations of Software Science and Computation Structures (FOSSACS 2006)"},{"key":"80","article-title":"Field constraint analysis","author":"wies","year":"2006","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"journal-title":"Using Z","year":"1996","author":"woodcock","key":"81"},{"key":"86","article-title":"Automatic assume\/guarantee reasoning for heap-manupilating programs","author":"yorsh","year":"2005","journal-title":"1st AIOOL Workshop"},{"key":"87","article-title":"Combining theorem proving with static analysis for data structure consistency","author":"zee","year":"2004","journal-title":"International Workshop on Software Verification and Validation (SVV 2004)"},{"key":"84","article-title":"Symbolically computing most-precise abstract operations for shape analysis","author":"yorsh","year":"2004","journal-title":"10th TACAS"},{"key":"85","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182618"},{"year":"0","key":"67"},{"key":"66","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"69","article-title":"Finite differencing of logical formulas for static analysis","author":"reps","year":"2003","journal-title":"Proc 12th ESOP"},{"journal-title":"A decidable logic for pointer programs manipulating linked lists","year":"2005","author":"ranise","key":"68"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45136-6_18"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263706"},{"key":"26","article-title":"Is it a tree, a DAG, or a cyclic graph?","author":"ghiya","year":"1996","journal-title":"Proc 10th ACM POPL"},{"key":"27","article-title":"Connection analysis: A practical interprocedural heap analysis for C","author":"ghiya","year":"1995","journal-title":"Proc 5th Workshop Languages and Compilers for Parallel Computing"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567757"},{"key":"29","article-title":"Decision procedures for guarded logics","volume":"1632","author":"gra?del","year":"1999","journal-title":"LNCS"},{"key":"3","article-title":"The KeY approach: Integrating object oriented design and formal verification","author":"ahrendt","year":"2000","journal-title":"Proceedings 8th European Workshop on Logics in AI (JELIA) Malaga Spain"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020001"},{"journal-title":"The b-toolkit","year":"2006","key":"1"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_14"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"journal-title":"CASSIS 2004 International Workshop on Construction and Analysis of Safe Secure and Interoperable Smart devices","year":"2004","author":"barnett","key":"6"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"32","article-title":"Region-based shape analysis with tracked locations","author":"hackett","year":"2005","journal-title":"Proc 25th ACM SIGPLAN Symp Principles of Programming Languages (POPL)"},{"key":"4","article-title":"Shape analysis by predicate abstraction","author":"balaban","year":"2005","journal-title":"VMCAl'05"},{"key":"31","article-title":"Automata-based verification of programs with tree updates","author":"habermehl","year":"2006","journal-title":"TACAS'06"},{"key":"70","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349325"},{"key":"71","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"9","article-title":"Quantitative verification of programs with lists","author":"bozga","year":"2005","journal-title":"Proc of the NATO Advanced Research Workshop on Verification of Infinite-State Systems with Applications to Security (VISSAS 2005)"},{"key":"72","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"8","first-page":"415","article-title":"STeP: Deductive-algorithmic verification of reactive and real-time systems","volume":"1102","author":"bj\ufffdrner","year":"1996","journal-title":"8th CAV"},{"key":"73","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"journal-title":"Automatic Verification of Programs with Complex Data Structure","year":"1976","author":"suzuki","key":"74"},{"key":"75","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512963"},{"year":"0","key":"76"},{"key":"59","article-title":"A mechanized program verifier","author":"strother moore","year":"2005","journal-title":"IFIP Working Conference on the Program Verifier Challenge"},{"key":"58","article-title":"The Pointer Assertion Logic Engine","author":"m\ufffdller","year":"2001","journal-title":"Programming Language Design and Implementation"},{"key":"57","first-page":"476","article-title":"Data structure specifications via local equality axioms","author":"mcpeak","year":"2005","journal-title":"CAV"},{"journal-title":"Automatic testing of software with structurally complex inputs","year":"2005","author":"marinov","key":"56"},{"key":"19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-45099-3_7","article-title":"Checking cleanness in linked lists","author":"dor","year":"2000","journal-title":"Proceedings of the 8th Static Analysis Symposium"},{"key":"55","article-title":"The Krakatoa tool for certification of JAVA\/JAVACARD programs annotated in JML","author":"marche?","year":"2003","journal-title":"Journal of Logic and Algebraic Programming"},{"journal-title":"An Interactive Program Verifier","year":"1973","author":"deutsch","key":"17"},{"key":"18","article-title":"A local shape analysis based on separation logic","author":"distefano","year":"2006","journal-title":"TACAS'06"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"article-title":"Extended static checking","year":"1998","author":"detlefs","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/125083.123049"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"year":"0","key":"11"},{"key":"12","article-title":"Esc\/java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an internet voting tally system","author":"cok","year":"2004","journal-title":"Construction and Analysis of Safe Secure and Interoperable Smart Devices"},{"year":"0","key":"21"},{"key":"20","article-title":"Static analysis versus software model checking for bug finding","author":"engler","year":"2004","journal-title":"VMCAI"},{"year":"0","key":"64"},{"key":"65","article-title":"Boolean heaps","author":"podelski","year":"2005","journal-title":"Proc Int l Static Analysis Symp"},{"key":"62","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"63","article-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","volume":"2283","author":"nipkow","year":"2002","journal-title":"LNCS"},{"article-title":"Nelson. Techniques for program verification","year":"1981","author":"greg","key":"60"},{"key":"61","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"49","article-title":"Automatic verification of pointer programs using grammar-based shape analysis","author":"lee","year":"2005","journal-title":"ESOP"},{"key":"48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"44","article-title":"Indexed predicate discovery for unbounded system verification","author":"lahiri","year":"2004","journal-title":"CAV'04"},{"key":"47","doi-asserted-by":"crossref","DOI":"10.1145\/1052898.1052913","article-title":"Cross-cutting techniques in program specification and analysis","author":"lam","year":"2005","journal-title":"Proc of the 4th International Conference on Aspect-Oriented Software Development (AOSD)"},{"key":"46","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.125"},{"key":"10","first-page":"84","article-title":"Reasoning in expressive description logics with fixpoints based on automata on infinite trees","author":"calvanese","year":"1999","journal-title":"Proc of the 16th Int Joint Conf on Artificial Intelligence (IJCAJ'99)"},{"key":"51","article-title":"Using data groups to specify and check side effects","author":"rustan","year":"2002","journal-title":"Proc ACM PLDI"},{"key":"52","volume":"cade 20","author":"lev-ami","year":"2005","journal-title":"Simulating reachability using first-order logic with applications to verification of linked data structures"},{"key":"53","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"50","article-title":"Loop invariants on demand","volume":"3780","author":"rustan","year":"2005","journal-title":"LNCS"}],"event":{"name":"Proceedings 20th IEEE International Parallel & Distributed Processing Symposium","start":{"date-parts":[[2006,4,25]]},"location":"Rhodes Island, Greece","end":{"date-parts":[[2006,4,29]]}},"container-title":["Proceedings 20th IEEE International Parallel & Distributed Processing Symposium"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/10917\/34366\/01639580.pdf?arnumber=1639580","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T19:22:43Z","timestamp":1555701763000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1639580\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"references-count":87,"URL":"https:\/\/doi.org\/10.1109\/ipdps.2006.1639580","relation":{},"subject":[],"published":{"date-parts":[[2006]]}}}