{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:28Z","timestamp":1772164048759,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,11,10]],"date-time":"2013-11-10T00:00:00Z","timestamp":1384041600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,11,10]]},"DOI":"10.1145\/2527269.2527272","type":"proceedings-article","created":{"date-parts":[[2013,11,12]],"date-time":"2013-11-12T10:29:36Z","timestamp":1384252176000},"page":"51-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Compositional verification of a medical device system"],"prefix":"10.1145","author":[{"given":"Anitha","family":"Murugesan","sequence":"first","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]},{"given":"Sanjai","family":"Rayadurgam","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]},{"given":"Mats P.E.","family":"Heimdahl","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,11,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Generic infusion pump project http:\/\/rtg.cis.upenn.edu\/gip.php3.  Generic infusion pump project http:\/\/rtg.cis.upenn.edu\/gip.php3."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77387"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146250"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_13"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15654-0_4"},{"key":"e_1_3_2_1_8_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts)","author":"Ganzinger H.","year":"2004","unstructured":"H. Ganzinger , G. Hagen , R. Nieuwenhuis , A. Oliveras , and C. Tinelli . DPLL(T): Fast decision procedures . In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts) , volume 3114 of Lecture Notes in Computer Science , pages 175 -- 188 . Springer , 2004 . H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts), volume 3114 of Lecture Notes in Computer Science, pages 175--188. Springer, 2004."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517439"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_3_2_1_13_1","first-page":"102","volume-title":"Requirements Engineering, 2001. Proceedings. Fifth IEEE International Symposium on","author":"Hammond J.","year":"2001","unstructured":"J. Hammond , R. Rawlings , and A. Hall . Will it work? {requirements engineering} . In Requirements Engineering, 2001. Proceedings. Fifth IEEE International Symposium on , pages 102 -- 109 , 2001 . J. Hammond, R. Rawlings, and A. Hall. Will it work? {requirements engineering}. In Requirements Engineering, 2001. Proceedings. Fifth IEEE International Symposium on, pages 102--109, 2001."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038686"},{"key":"e_1_3_2_1_16_1","volume-title":"Property Specification Language (PSL)","author":"Std IEEE. IEEE","year":"2005","unstructured":"IEEE. IEEE Std . 1850-2005. Property Specification Language (PSL) . IEEE , 2005 . IEEE. IEEE Std. 1850-2005. Property Specification Language (PSL). IEEE, 2005."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/225014.225016"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_19_1","volume-title":"UCLA","author":"Kamp J. A. W.","year":"1968","unstructured":"J. A. W. Kamp . Tense Logic and the Theory of Linear Order. PhD thesis , UCLA , 1968 . J. A. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, UCLA, 1968."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_19"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_3_2_1_22_1","volume-title":"The MathWorks Inc. corporate web page. Via the world-wide-web: http:\/\/www.mathworks.com","year":"2004","unstructured":"MathWorks. The MathWorks Inc. corporate web page. Via the world-wide-web: http:\/\/www.mathworks.com , 2004 . MathWorks. The MathWorks Inc. corporate web page. Via the world-wide-web: http:\/\/www.mathworks.com, 2004."},{"key":"e_1_3_2_1_23_1","unstructured":"Mathworks Inc. Simulink Design Verifier product web site. http:\/\/www.mathworks.com\/products\/sldesignverier\/.  Mathworks Inc. Simulink Design Verifier product web site. http:\/\/www.mathworks.com\/products\/sldesignverier\/."},{"key":"e_1_3_2_1_24_1","unstructured":"Mathworks Inc. Simulink product web site. http:\/\/www.mathworks.com\/products\/simulink.  Mathworks Inc. Simulink product web site. http:\/\/www.mathworks.com\/products\/simulink."},{"key":"e_1_3_2_1_25_1","unstructured":"Mathworks Inc. Stateow product web site. http:\/\/www.mathworks.com.  Mathworks Inc. Stateow product web site. http:\/\/www.mathworks.com."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00030-1"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0173-6"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MiSE.2013.6595290"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.910904"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/101969.101977"},{"key":"e_1_3_2_1_33_1","volume-title":"SAE","year":"2004","unstructured":"SAE-AS5506. Architecture Analysis and Design Language . SAE , Nov 2004 . SAE-AS5506. Architecture Analysis and Design Language. SAE, Nov 2004."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_3_2_1_35_1","volume-title":"http:\/\/www.speeds.eu.com\/","author":"Exporatory Eculative","year":"2006","unstructured":"SP Eculative and Exporatory Design in System engineering. http:\/\/www.speeds.eu.com\/ , 2006 -2009. SPEculative and Exporatory Design in System engineering. http:\/\/www.speeds.eu.com\/, 2006-2009."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"}],"event":{"name":"HILT 2013: High Integrity Language Technology ACM SIGAda Annual","location":"Pittsburgh Pennsylvania USA","acronym":"HILT 2013","sponsor":["Ada Europe Ada Europe","SIGAda ACM Special Interest Group on Ada Programming Language","SIGAPP ACM Special Interest Group on Applied Computing","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems","SIGSOFT ACM Special Interest Group on Software Engineering","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2527269.2527272","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2527269.2527272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:28Z","timestamp":1750217668000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2527269.2527272"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,10]]},"references-count":35,"alternative-id":["10.1145\/2527269.2527272","10.1145\/2527269"],"URL":"https:\/\/doi.org\/10.1145\/2527269.2527272","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2658982.2527272","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,11,10]]},"assertion":[{"value":"2013-11-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}