{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T23:20:03Z","timestamp":1792797603884,"version":"4.5.0"},"reference-count":88,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100004807","name":"DFG","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/100004807","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DFG as part of the Germany's Excellence Strategy EXC 2050\/1","award":["390696704"],"award-info":[{"award-number":["390696704"]}]},{"name":"Cluster of Excellence \u201cCentre for Tactile Internet\u201d (CeTI) of TU Dresden","id":[{"id":"https:\/\/ror.org\/042aqky30","id-type":"ROR","asserted-by":"crossref"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"name":"German Israeli Foundation","award":["1-1513-407.\/2019"],"award-info":[{"award-number":["1-1513-407.\/2019"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Visual. Comput. Graphics"],"published-print":{"date-parts":[[2022,1]]},"DOI":"10.1109\/tvcg.2021.3114866","type":"journal-article","created":{"date-parts":[[2021,9,29]],"date-time":"2021-09-29T17:37:32Z","timestamp":1632937052000},"page":"357-367","source":"Crossref","is-referenced-by-count":13,"title":["Visual Analysis of Hyperproperties for Understanding Model Checking Results"],"prefix":"10.1109","volume":"28","author":[{"given":"Tom","family":"Horak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Norine","family":"Coenen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tamara","family":"Flemisch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Mendez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dennis","family":"Dimov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Raimund","family":"Dachselt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2019.2950932"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1109\/CMV.2007.20"},{"key":"ref71","article-title":"Towards a universal interface for real-time mathematical communication","author":"pollanen","year":"0","journal-title":"CIC-Workshop"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9657.001.0001"},{"key":"ref76","author":"seoul-oh","year":"2012","journal-title":"Mathquill"},{"key":"ref77","article-title":"Going beyond visualization: Verbalization as complementary medium to explain machine learning models","author":"sevastjanova","year":"0","journal-title":"Workshop on Visualization for AI Explainability at IEEE VIS"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.3929\/ETHZ-A-010608394"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_8"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_32"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2020.3030403"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2019.2934629"},{"key":"ref33","author":"frisch","year":"2012","journal-title":"Interaction and visualization techniques for node-link diagram editing and exploration"},{"key":"ref32","article-title":"Towards designing a tool for understanding proofs in ontologies through combined node-link diagrams","author":"flemisch","year":"0","journal-title":"International Workshop on Visualization and Interaction for Ontologies and Linked Data"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2134-0"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11880240_49"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2016.2618797"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_28"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3313831.3376148"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1111\/cgf.13717"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/SCORED.2017.8305431"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303947"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1177\/1473871618806555"},{"key":"ref64","year":"2017","journal-title":"Handwriting recognition - MyScript"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"ref65","doi-asserted-by":"crossref","first-page":"138","DOI":"10.18653\/v1\/2020.inlg-1.20","article-title":"Chart-to-Text: Generating natural language descriptions for charts by adapting the transformer model","author":"obeid","year":"2020","journal-title":"Proc International Conference on Natural Language Generation"},{"key":"ref66","year":"1999","journal-title":"Opencores"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ACPR.2015.7486478"},{"key":"ref67","year":"2009","journal-title":"Node js"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8472025"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2015.7281905"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2591062.2591134"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/CCECE.2004.1347584"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029908"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2020.3030338"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"ref23","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785713"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-012-0113-x"},{"key":"ref51","article-title":"A temporal logic of security","volume":"abs 1306 5678","author":"koleini","year":"2013","journal-title":"CoRR"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-006-7999-y"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/PacificVis48177.2020.1043"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/3357033"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_18"},{"key":"ref54","article-title":"Proposal for coexistence of mathematical handwritten and keyboard input in a wysiwyg expression editor","author":"lao-tebar","year":"0","journal-title":"FM4M\/MathUI\/ThEdu\/DP\/WIP CIKM"},{"key":"ref53","author":"lahtinen","year":"2012","journal-title":"Model Checking Methodology for Large Systems Faults and Asynchronous Behaviour SARANA 2011 Work Report"},{"key":"ref52","author":"koutsofios","year":"1992","journal-title":"Drawing Graphs with Dot"},{"key":"ref10","author":"biere","year":"2011","journal-title":"Aiger 1 9 and Beyond"},{"key":"ref40","author":"gunning","year":"2016","journal-title":"Explainable artificial intelligence (xai)"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2010.15"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2010.5641711"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2011.185"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/VISUAL.1991.175794"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2018.2865044"},{"key":"ref16","article-title":"User-friendly model checking integration in model-based development","author":"campetelli","year":"0","journal-title":"International Conference on Computer Applications in Industry and Engineering"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2018.2865145"},{"key":"ref17","author":"carlisle","year":"2014","journal-title":"Mathematical Markup Language (MathML) Version 3 0 2nd Edition"},{"key":"ref84","author":"wiehr","year":"2020","journal-title":"Safe handover in mixed-initiative control for cyber-physical systems"},{"key":"ref18","article-title":"Towards meaningful visual abstraction of mathematical notation","author":"cervone","year":"0","journal-title":"Proc CIC"},{"key":"ref83","author":"thielke","year":"2013","journal-title":"Code geknackt"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1145\/3399715.3399829"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1515\/9783110636420"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.40"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2017.2674958"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3375633"},{"key":"ref85","first-page":"177","article-title":"Using automatic speech recognition to dictate mathematical expressions: The development of the “talkmaths” application at kingston university","volume":"28","author":"wigmore","year":"2009","journal-title":"Journal of Computers in Mathematics and Science Teaching"},{"key":"ref49","author":"kohlhase","year":"2008","journal-title":"Adaptation of notations in living mathematical documents"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_11"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1145\/3341.3347"},{"key":"ref87","author":"woos","year":"2019","journal-title":"A Step-through Debugger for Distributed Systems"},{"key":"ref9","author":"biere","year":"2007","journal-title":"The AIGER And-Inverter Graph (AIG) format version 20071012"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1111\/cgf.14035"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_32"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2010.41"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/VISUAL.2019.8933695"},{"key":"ref41","author":"haverbeke","year":"2011","journal-title":"CodeMirror"},{"key":"ref44","first-page":"171","article-title":"Fbdverifier: Interactive and visual analysis of counter-example in formal verification of function block diagram","volume":"42","author":"jee","year":"2010","journal-title":"Journal of Research and Practice in Information Technology"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2006.99495"}],"container-title":["IEEE Transactions on Visualization and Computer Graphics"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/2945\/9663056\/09552899.pdf?arnumber=9552899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:12:45Z","timestamp":1725829965000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9552899\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1]]},"references-count":88,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tvcg.2021.3114866","relation":{},"ISSN":["1077-2626","1941-0506","2160-9306"],"issn-type":[{"value":"1077-2626","type":"print"},{"value":"1941-0506","type":"electronic"},{"value":"2160-9306","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1]]}}}