{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T02:30:38Z","timestamp":1730255438968,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,5,30]],"date-time":"2021-05-30T00:00:00Z","timestamp":1622332800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,5,30]],"date-time":"2021-05-30T00:00:00Z","timestamp":1622332800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,5,30]]},"DOI":"10.1109\/icra48506.2021.9561191","type":"proceedings-article","created":{"date-parts":[[2021,10,20]],"date-time":"2021-10-20T00:28:35Z","timestamp":1634689715000},"page":"9368-9374","source":"Crossref","is-referenced-by-count":8,"title":["Formal Verification of ROS Based Systems Using a Linear Logic Theorem Prover"],"prefix":"10.1109","author":[{"given":"Sitar","family":"Kortik","sequence":"first","affiliation":[{"name":"Fraunhofer IPA,Stuttgart,Germany,70569"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tejas Kumar","family":"Shastha","sequence":"additional","affiliation":[{"name":"Fraunhofer IPA,Stuttgart,Germany,70569"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"1","article-title":"BRIDE - A toolchain for framework-independent development of industrial service robot applications","author":"bubeck","year":"2014","journal-title":"ISR\/Robotik 2014 41st International Symposium on Robotics"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480693"},{"key":"ref12","article-title":"Survey of existing tools for formal verification","author":"armstrong","year":"2014","journal-title":"SANDIA REPORT SAND2014-20533"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3342355"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11900-7_18"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2017.9"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6630618"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_20"},{"key":"ref18","article-title":"User’s guide of a linear logic theorem prover (llprover)","author":"tamura","year":"1998","journal-title":"tech rep Department of Computer and Systems Engineering Faculty of Engineering"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48754-9_20"},{"year":"0","key":"ref28","article-title":"SeRoNet project website"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10846-018-0971-9"},{"year":"0","key":"ref27","article-title":"Source codes of the verifier and ros components"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907404"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s10489-017-0936-x"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-008-9079-0"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-450010-5.50026-8"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2017.04.004"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MODELS.2019.00-11"},{"key":"ref1","first-page":"5","article-title":"Ros: an open-source robot operating system","volume":"3","author":"quigley","year":"2009","journal-title":"Proc of the IEEE Workshop on Open Source Software"},{"journal-title":"Type theory and functional programming","year":"1991","author":"thompson","key":"ref20"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2016.7759661"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"journal-title":"Kobuki robot","year":"0","key":"ref24"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3278186.3278195"},{"year":"0","key":"ref26","article-title":"Kobuki random walker application"},{"journal-title":"Kobuki gazebo simulation","year":"0","key":"ref25"}],"event":{"name":"2021 IEEE International Conference on Robotics and Automation (ICRA)","start":{"date-parts":[[2021,5,30]]},"location":"Xi'an, China","end":{"date-parts":[[2021,6,5]]}},"container-title":["2021 IEEE International Conference on Robotics and Automation (ICRA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9560720\/9560666\/09561191.pdf?arnumber=9561191","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T23:22:33Z","timestamp":1659482553000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9561191\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,30]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/icra48506.2021.9561191","relation":{},"subject":[],"published":{"date-parts":[[2021,5,30]]}}}