{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T05:35:49Z","timestamp":1789709749157,"version":"4.0.1"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,5]]},"DOI":"10.1109\/icra.2012.6225285","type":"proceedings-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T17:23:24Z","timestamp":1341854604000},"page":"4718-4723","source":"Crossref","is-referenced-by-count":4,"title":["Proving the correctness of concurrent robot software"],"prefix":"10.1109","author":[{"given":"Peter","family":"Kazanzides","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanni","family":"Kouskoulas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anton","family":"Deguet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"15","first-page":"275","article-title":"Assume-guarantee reasoning for hierarchical hybrid systems","volume":"2034","author":"henzinger","year":"2001","journal-title":"LNCS"},{"key":"16","doi-asserted-by":"crossref","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","author":"hoare","year":"1969","journal-title":"Communications of the ACM"},{"key":"13","first-page":"54","article-title":"Model checking","volume":"1346","author":"clarke","year":"1997","journal-title":"LNCS"},{"key":"14","first-page":"219","article-title":"Verification of medical guidelines by model checking - A case study","volume":"3925","author":"ba?umler","year":"2006","journal-title":"LNCS"},{"key":"11","first-page":"6107","article-title":"A component-based architecture for flexible integration of robotic systems","author":"jung","year":"0","journal-title":"IEEE\/RSJ Intl Conf on Intelligent Robots and Systems (IROS) 2010"},{"key":"12","first-page":"1","article-title":"A verifiable and correct-by-construction controller for robot functional levels","volume":"2","author":"bensalem","year":"2011","journal-title":"J of Software Engin for Robotics (JOSER)"},{"key":"21","author":"vafeiadis","year":"2007","journal-title":"Modular Fine-grained Concurrency Verification"},{"key":"20","first-page":"49","article-title":"Resources, concurrency and local reasoning","volume":"3170","author":"o'hearn","year":"2004","journal-title":"LNCS"},{"key":"22","author":"kouskoulas","year":"2011","journal-title":"Certifying the Concurrent State Table Implementation in A Surgical Robotic System (Extended Version)"},{"key":"23","article-title":"Certifying the concurrent state table implementation in a surgical robotic system","author":"kouskoulas","year":"0","journal-title":"3rd Joint Workshop on High Confidence Medical Devices Software and Systems (HCMDSS) and Medical Device Plug-and-Play Interoperability (MDPnP) Apr 2011"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.180"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/129630.376083"},{"key":"3","first-page":"317","article-title":"The Player\/Stage project: Tools for multi-robot and distributed sensor systems","author":"gerkey","year":"0","journal-title":"Proc Intl Conf on Advanced Robotics (ICAR) 2003"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2009.934837"},{"key":"10","first-page":"571","article-title":"Concolic testing","author":"sen","year":"0","journal-title":"Proc 22nd IEEE\/ACM Intl Conf on Automated Software Engineering (ASE) 2007"},{"key":"1","author":"szyperski","year":"1997","journal-title":"Component Software Beyond Object-Oriented Programming"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2006.1642285"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2003.1242011"},{"key":"5","article-title":"ROS: An open-source robot operating system","author":"quigley","year":"0","journal-title":"ICRA Workshop on Open Source Software 2009"},{"key":"4","article-title":"Orca: Components for robotics","author":"makarenko","year":"0","journal-title":"IEEE\/RSJ Intl Conf on Intelligent Robots and Systems (IROS) Workshop on Robotic Standardization Dec 2006"},{"key":"9","year":"0","journal-title":"Cisst ROS Package"},{"key":"8","year":"0","journal-title":"Orocos ROS Package"}],"event":{"name":"2012 IEEE International Conference on Robotics and Automation (ICRA)","location":"St Paul, MN, USA","start":{"date-parts":[[2012,5,14]]},"end":{"date-parts":[[2012,5,18]]}},"container-title":["2012 IEEE International Conference on Robotics and Automation"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6215071\/6224548\/06225285.pdf?arnumber=6225285","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T17:08:15Z","timestamp":1497978495000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6225285\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/icra.2012.6225285","relation":{},"subject":[],"published":{"date-parts":[[2012,5]]}}}