{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T09:51:34Z","timestamp":1730281894503,"version":"3.28.0"},"reference-count":15,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1109\/memcod.2016.7797745","type":"proceedings-article","created":{"date-parts":[[2016,12,29]],"date-time":"2016-12-29T21:54:22Z","timestamp":1483048462000},"page":"54-58","source":"Crossref","is-referenced-by-count":0,"title":["Combining type-checking with model-checking for system verification"],"prefix":"10.1109","author":[{"given":"Zhiqiang","family":"Ren","sequence":"first","affiliation":[]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.995426"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2242"},{"journal-title":"SAGE Unified hybrid checking for first-class types general refinement types and dynamic","year":"2006","author":"knowles","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"ref14","article-title":"Maude: Specification and programming in rewriting logic","author":"clavel","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"ref15","article-title":"The Maude LTL model checker","volume":"71","author":"eker","year":"2002","journal-title":"Fourth Workshop on Rewriting Logic and Its Applications WRLA '02 Ser Electronic Notes in Theoretical Computer Science"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_21"},{"journal-title":"The ATS Programming Language System","year":"2016","author":"xi","key":"ref6"},{"key":"ref5","article-title":"A Linear Type System for Multicore Programming","author":"shi","year":"2009","journal-title":"Proceedings of Simposio Brasileiro de Linguagens de Programacao"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14458-5_1"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"journal-title":"The SPIN Model Checker Primer and Reference Manual","year":"2003","author":"holzmann","key":"ref2"},{"key":"ref1","article-title":"A Dialogue with Professor Joseph Sifakis about Concurrent Systems Specification and Verification","author":"sifakis","year":"2011","journal-title":"Interview by Christian Calude"},{"journal-title":"Effective ATS Session-typed Channels A Brief Introduction","year":"2016","author":"xi","key":"ref9"}],"event":{"name":"2016 ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)","start":{"date-parts":[[2016,11,18]]},"location":"Kanpur, India","end":{"date-parts":[[2016,11,20]]}},"container-title":["2016 ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7786794\/7797738\/07797745.pdf?arnumber=7797745","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,1,21]],"date-time":"2017-01-21T04:47:47Z","timestamp":1484974067000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7797745\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":15,"URL":"https:\/\/doi.org\/10.1109\/memcod.2016.7797745","relation":{},"subject":[],"published":{"date-parts":[[2016,11]]}}}