{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:57:48Z","timestamp":1729645068113,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1109\/tase.2017.8285642","type":"proceedings-article","created":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T22:54:03Z","timestamp":1518476043000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["VMDV: A 3D visualization tool for modeling, demonstration, and verification"],"prefix":"10.1109","author":[{"given":"Jian","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ying","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanyun","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.096"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"ref12","first-page":"149","article-title":"Efficient and high quality force-directed graph drawing","volume":"10","author":"hu","year":"2005","journal-title":"The Matematical Journal"},{"journal-title":"SCTL towards combining model checking and proof checking","year":"2017","author":"jiang","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.167.6"},{"journal-title":"Automated Theorem Proving A Logical Basis (Fun-damental Studies in Computer Science)","year":"1978","author":"loveland","key":"ref15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1117\/12.871402"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"98679e","DOI":"10.1371\/journal.pone.0098679","article-title":"Forceatlas 2, a continuous graph layout algorithm for handy network visualization designed for the gephi software","volume":"9","author":"mathieu","year":"2014","journal-title":"PLoS ONE"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20551-4_6"},{"key":"ref19","first-page":"179","article-title":"Visualising first-order proof search","volume":"2005","author":"steel","year":"2005","journal-title":"Proc User Interfaces for Theorem Provers"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.095"},{"journal-title":"Interactive Theorem Proving and Program Development Coq'Art The Calculus of Inductive Constructions","year":"2013","author":"bertot","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"journal-title":"A logical approach to CTL","year":"2013","author":"dowek","key":"ref7"},{"journal-title":"Interactive symbolic visualization of semi-automatic theorem proving","year":"2003","author":"bajaj","key":"ref2"},{"journal-title":"Principles of Model Checking","year":"2008","author":"baier","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"}],"event":{"name":"2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)","start":{"date-parts":[[2017,9,13]]},"location":"Sophia Antipolis","end":{"date-parts":[[2017,9,15]]}},"container-title":["2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8277122\/8285614\/08285642.pdf?arnumber=8285642","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T21:22:01Z","timestamp":1570742521000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8285642\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/tase.2017.8285642","relation":{},"subject":[],"published":{"date-parts":[[2017,9]]}}}