{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T16:17:49Z","timestamp":1729613869749,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987595","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"51-58","source":"Crossref","is-referenced-by-count":2,"title":["Efficient verification of periodic programs using sequential consistency and snapshots"],"prefix":"10.1109","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"Context-bounded translations for concurrent software: An empirical evaluation","author":"ghafari","year":"2010","journal-title":"Proc of SPIN"},{"key":"17","article-title":"Time-bounded analysis of real-time systems","author":"chaki","year":"2011","journal-title":"Proc of FMCAD"},{"key":"18","article-title":"Reducing context-bounded concurrent reachability to sequential reachability","author":"torre","year":"2009","journal-title":"Proc of CAV"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.020"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"larsen","year":"1997","journal-title":"STTT"},{"key":"14","article-title":"Verification of real-time designs: Combining scheduling theory with automatic formal verification","author":"braberman","year":"1999","journal-title":"Proc of FSE"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_31"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679402"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"22","article-title":"One stack to run them all-reducing concurrent analysis to sequential analysis under priority scheduling","author":"kidd","year":"2010","journal-title":"Proc of SPIN"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_11"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987595"},{"key":"26","article-title":"Ufo: A framework for abstraction-And interpolation-based software verification","author":"albarghouthi","year":"2012","journal-title":"Proc of CAV"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"29","article-title":"A tool for checking ansi-c programs","author":"clarke","year":"2004","journal-title":"Proc of TACAS"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"2","article-title":"Bounded model checking of concurrent programs","author":"rabinovitz","year":"2005","journal-title":"Proc of CAV"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926433"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2012-2607"},{"key":"30","article-title":"Reducing concurrent analysis under a context bound to sequential analysis","author":"lal","year":"2008","journal-title":"Proc of CAV"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"6","article-title":"Partial orders for efficient bounded model checking of concurrent software","author":"alglave","year":"2013","journal-title":"Proc of CAV"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882301"},{"key":"4","article-title":"Symbolic predictive analysis for concurrent programs","author":"wang","year":"2009","journal-title":"Proc of FM"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2014,10,21]]},"location":"Lausanne, Switzerland","end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987595.pdf?arnumber=6987595","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T02:54:05Z","timestamp":1498186445000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987595\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987595","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}