{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T17:09:42Z","timestamp":1742404182862},"reference-count":36,"publisher":"Oxford University Press (OUP)","license":[{"start":{"date-parts":[[2018,11,27]],"date-time":"2018-11-27T00:00:00Z","timestamp":1543276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"CAS-INRIA project VIP","award":["GJHZ1844"],"award-info":[{"award-number":["GJHZ1844"]}]},{"name":"NSFC-ANR project LOCALI","award":["NSFC 61161130530","ANR-11-IS02-00201"],"award-info":[{"award-number":["NSFC 61161130530","ANR-11-IS02-00201"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1093\/comjnl\/bxy112","type":"journal-article","created":{"date-parts":[[2018,10,12]],"date-time":"2018-10-12T19:12:57Z","timestamp":1539371577000},"source":"Crossref","is-referenced-by-count":0,"title":["Towards Combining Model Checking and Proof Checking"],"prefix":"10.1093","author":[{"given":"Ying","family":"Jiang","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Liu","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Dowek","sequence":"additional","affiliation":[{"name":"Inria and ENS de Cachan, 61, avenue du Pr\u00e9sident Wilson, Cachan cedex, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kailiang","family":"Ji","sequence":"additional","affiliation":[{"name":"University Paris Diderot, 8 Place Aur\u00e9lie Nemours, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2018,11,27]]},"reference":[{"key":"key\n\t\t\t\t2019012510015667400_bxy112C1","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"Clarke","year":"2001"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C2","author":"Bouajjani","year":"2000"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C3","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996","edition":"2nd edn"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C5","volume-title":"Automated Theorem Proving: A Logical Basis (Fundamental Studies in Computer Science)","author":"Loveland","year":"1978"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C6","author":"Burel","year":"2009"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C7","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time temporal logic to synthesize synchronization skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Sci. Comput. Program."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of branching time","volume":"30","author":"Emerson","year":"1985","journal-title":"J. Comput. Syst. Sci."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C9","author":"Zhang","year":"2014"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C10","author":"Ji","year":"2015"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C11","author":"Mu\u00f1oz","year":"2004"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C12","volume-title":"Abstract Model of SATS Concept of Operations: Initial Results and Recommendations","author":"NASA\/TM-2004-213006","year":"2004"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C13","author":"Bhat","year":"1995"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C14","author":"Vergauwen","year":"1993"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C15","volume-title":"Compiling with Continuations (Corr. Version)","author":"Appel","year":"2006"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C16","author":"Biere","year":"1999"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C17","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"Biere","year":"2003","journal-title":"Adv. Comput."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C18","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","article-title":"Clausal temporal resolution","volume":"2","author":"Fisher","year":"2001","journal-title":"ACM Trans. Comput. Log."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C19","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1093\/jigpal\/jzn018","article-title":"A sound and complete deductive system for ctl* verification","volume":"16","author":"Gabbay","year":"2008","journal-title":"Logic J. IGPL"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C20","author":"Pnueli","year":"2002"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C21","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.2307\/2695091","article-title":"An axiomatization of full computation tree logic","volume":"66","author":"Reynolds","year":"2001","journal-title":"J. Symb. Log."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C22","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1016\/j.jlap.2008.02.004","article-title":"Cut-free sequent systems for temporal logic","volume":"76","author":"Br\u00fcnnler","year":"2008","journal-title":"J. Log. Algebr. Program."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C23","author":"Partovi","year":"2014"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C24","volume-title":"Introduction to Robotics\u2014Mechanics and Control","author":"Craig","year":"1989","edition":"2nd edn"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C25","volume-title":"A Logical Approach to CTL","author":"ISCAS-SKLCS-14-01","year":"2014"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-4156-3","volume-title":"Programming Language Concepts","author":"Sestoft","year":"2012"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C27","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symb. Comput."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C28","author":"Sarnat","year":"2009"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model checking","author":"McMillan","year":"1993"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C30","author":"Cimatti","year":"1999"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C31","author":"Cavada","year":"2014"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C32","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF01019459","article-title":"The discoveries of continuations","volume":"6","author":"Reynolds","year":"1993","journal-title":"Lisp Symbolic Comput."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C33","author":"Burel","year":"2011"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C34","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","article-title":"Myths about the mutual exclusion problem","volume":"12","author":"Peterson","year":"1981","journal-title":"Inf. Process. Lett."},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C35","author":"Liu","year":"2017"},{"key":"key\n\t\t\t\t2019012510015667400_bxy112C36","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","article-title":"CADP 2011: a toolbox for the construction and analysis of distributed processes","volume":"15","author":"Garavel","year":"2013","journal-title":"STTT"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxy112\/26761923\/bxy112.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,26]],"date-time":"2019-10-26T15:09:02Z","timestamp":1572102542000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/advance-article\/doi\/10.1093\/comjnl\/bxy112\/5210380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,27]]},"references-count":36,"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxy112","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,27]]}}}