{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T05:53:51Z","timestamp":1729662831383,"version":"3.28.0"},"reference-count":40,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1109\/ipdps.2006.1639581","type":"proceedings-article","created":{"date-parts":[[2006,7,10]],"date-time":"2006-07-10T19:59:56Z","timestamp":1152561596000},"page":"8 pp.","source":"Crossref","is-referenced-by-count":0,"title":["Verification of software via integration of design and implementation"],"prefix":"10.1109","author":[{"given":"A.S.","family":"Miner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Basu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X_13","article-title":"Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation","author":"glusman","year":"2003","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"35","first-page":"6","article-title":"Efficient reachability set generation and storage using decision diagrams","volume":"1639","author":"miner","year":"1999","journal-title":"LNCS"},{"key":"17","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","article-title":"A BDD-based model checker for recursive programs","author":"esparza","year":"2001","journal-title":"Computer-Aided Verification (CAV)"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/32.83912"},{"key":"33","doi-asserted-by":"crossref","DOI":"10.1007\/s100090050040","article-title":"Control and data abstraction:the cornerstones of pratical formal verification","author":"kesten","year":"2000","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"15","article-title":"Model checking in CLP","author":"delzanno","year":"1999","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348042"},{"key":"16","article-title":"Slicing software for model construction","author":"dwyer","year":"1999","journal-title":"Proc Workshop Partial Evaluation and Semantics-Based Program Manipulation"},{"key":"39","first-page":"230","article-title":"On computable numbers, with an application to the Entscheidungsproblem","volume":"3","author":"turing","year":"1936","journal-title":"Proc Lond Math Soc Ser"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstract refinement","author":"clarke","year":"2000","journal-title":"Computer Aided Verification (CAV)"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"14"},{"key":"37","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent systems in CESAR","author":"queille","year":"1982","journal-title":"International Symposium on Programming"},{"key":"11","first-page":"328","article-title":"Saturation: An efficient iteration strategy for symbolic state space generation","volume":"2031","author":"ciardo","year":"2001","journal-title":"LNCS"},{"key":"38","first-page":"374","article-title":"Verification of asynchronous circuits by BDD-based model checking of Petri nets","volume":"935","author":"roig","year":"1995","journal-title":"LNCS"},{"key":"12","first-page":"256","article-title":"Using edge-valued decision diagrams for symbolic generation of shortest paths","volume":"2517","author":"ciardo","year":"2002","journal-title":"LNCS"},{"key":"21","first-page":"207","article-title":"Analysing the WAP class 2 wireless transaction protocol using coloured Petri nets","volume":"1825","author":"gordon","year":"2000","journal-title":"LNCS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"40","doi-asserted-by":"publisher","DOI":"10.1145\/358557.358577"},{"key":"22","first-page":"39","article-title":"Using the Bandera, Tool Set to model-check properties of concurrent Java software","volume":"2154","author":"hatcliff","year":"2001","journal-title":"LNCS"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"journal-title":"BLAST","year":"0","author":"henzinger","key":"24"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00066-8"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459838"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.1992.753516"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/53990.53994"},{"key":"29","article-title":"Better verification through symmetry reduction","author":"ip","year":"1996","journal-title":"Formal Methods Syst Design (FMSD)"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39979-7_6"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_17"},{"year":"0","key":"1"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"7","first-page":"49","article-title":"Symbolic model checking with partitioned transition relations","author":"burch","year":"1991","journal-title":"Proc Int Conf Very Large Scale Integration"},{"journal-title":"Coloured Petri Nets Basic Concepts Analysis Methods and Practical Use Volume 1 Analysis Methods","year":"1992","author":"jensen","key":"30"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01257083"},{"key":"32","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1007\/978-3-540-31980-1_39","article-title":"Focuscheck: A tool for model checking and debugging sequential c programs","volume":"3440","author":"keller","year":"2005","journal-title":"Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS"},{"key":"4","article-title":"Counter-example analysis for Cimple debugging","author":"basu","year":"2004","journal-title":"Proc Formal Techniques Networked and Distributed Systems (FORTE)"},{"key":"31","first-page":"9","article-title":"Multi-valued decision diagrams: Theory and applications","volume":"4","author":"kam","year":"1998","journal-title":"Multiple-Valued Logic"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"}],"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\/01639581.pdf?arnumber=1639581","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T07:23:01Z","timestamp":1497684181000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1639581\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"references-count":40,"URL":"https:\/\/doi.org\/10.1109\/ipdps.2006.1639581","relation":{},"subject":[],"published":{"date-parts":[[2006]]}}}