{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T02:08:47Z","timestamp":1725674927905},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,19]]},"DOI":"10.1145\/1707790.1707800","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T20:15:04Z","timestamp":1263932104000},"page":"57-62","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Challenge benchmarks for verification of real-time programs"],"prefix":"10.1145","author":[{"given":"Tomas","family":"Kalibera","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, IN, USA"}]},{"given":"Pavel","family":"Parizek","sequence":"additional","affiliation":[{"name":"Charles University, Prague, Czech Rep"}]},{"given":"Ghaith","family":"Haddad","sequence":"additional","affiliation":[{"name":"University of Central Florida, Orlando, FL, USA"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"University of Central Florida, Orlando, FL, USA"}]},{"given":"Jan","family":"Vitek","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, IN, USA"}]}],"member":"320","published-online":{"date-parts":[[2010,1,19]]},"reference":[{"volume-title":"http:\/\/www.rtems.com\/","year":"2009","key":"e_1_3_2_1_1_1","unstructured":"Real-time executive for multiprocessor\/missile systems (RTEMS). http:\/\/www.rtems.com\/ , 2009 . Real-time executive for multiprocessor\/missile systems (RTEMS). http:\/\/www.rtems.com\/, 2009."},{"volume-title":"Military Embedded Systems","year":"2006","key":"e_1_3_2_1_2_1","unstructured":"Aegis. Lockheed Martin selects Aonix PERC Virtual Machine for Aegis Weapon System . Military Embedded Systems , 2006 . http:\/\/www.mil-embedded.com\/news\/db\/?4224. Aegis. Lockheed Martin selects Aonix PERC Virtual Machine for Aegis Weapon System. Military Embedded Systems, 2006. http:\/\/www.mil-embedded.com\/news\/db\/?4224."},{"key":"e_1_3_2_1_3_1","unstructured":"aicas. The Jamaica Virtual Machine homepage. http:\/\/www.aicas.com 2005. aicas. The Jamaica Virtual Machine homepage. http:\/\/www.aicas.com 2005."},{"key":"e_1_3_2_1_4_1","volume-title":"http:\/\/research.aonix.com\/jsc\/pico-manual.4-19-08.pdf","author":"PERC","year":"2008","unstructured":"Aonix. PERC Pico 1.1 user manual. http:\/\/research.aonix.com\/jsc\/pico-manual.4-19-08.pdf , 2008 . Aonix. PERC Pico 1.1 user manual. http:\/\/research.aonix.com\/jsc\/pico-manual.4-19-08.pdf, 2008."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1324969.1324974"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/872024.872575"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1289927.1289967"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/556706"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2005.31"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/863631.880499"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.295895"},{"key":"e_1_3_2_1_12_1","volume-title":"EUROCAE ED-12B software considerations in airborne systems and equipment certification","author":"EUROCAE.","year":"1992","unstructured":"EUROCAE. EUROCAE ED-12B software considerations in airborne systems and equipment certification , 1992 . EUROCAE. EUROCAE ED-12B software considerations in airborne systems and equipment certification, 1992."},{"key":"e_1_3_2_1_13_1","unstructured":"European Space Agency. Venus express mission. http:\/\/www.esa.int\/SPECIALS\/Venus Express 2009. European Space Agency. Venus express mission. http:\/\/www.esa.int\/SPECIALS\/Venus Express 2009."},{"key":"e_1_3_2_1_14_1","unstructured":"J. Gaisler E. Catovic M. Isomki K. Glembo and S. Habinc. GRLIB IP core users manual. http:\/\/www.gaisler.com\/products\/grlib\/grip.pdf 2009. J. Gaisler E. Catovic M. Isomki K. Glembo and S. Habinc. GRLIB IP core users manual. http:\/\/www.gaisler.com\/products\/grlib\/grip.pdf 2009."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1288940.1288955"},{"key":"e_1_3_2_1_16_1","volume-title":"Certification of Safety-Critical Software Controlled Systems (SafeCert)","author":"Hunt J.","year":"2009","unstructured":"J. Hunt , D. Locke , K. Nilsen , M. Schoeberl , and J. Vitek . Java for safety-critical applications . In Certification of Safety-Critical Software Controlled Systems (SafeCert) , 2009 . J. Hunt, D. Locke, K. Nilsen, M. Schoeberl, and J. Vitek. Java for safety-critical applications. In Certification of Safety-Critical Software Controlled Systems (SafeCert), 2009."},{"volume-title":"Embedded Computing Design","year":"2007","key":"e_1_3_2_1_17_1","unstructured":"Inflight. Aonix PERC selected for inflight entertainment system . Embedded Computing Design , 2007 . http:\/\/www.embedded-computing.com\/news\/db\/?8205. Inflight. Aonix PERC selected for inflight entertainment system. Embedded Computing Design, 2007. http:\/\/www.embedded-computing.com\/news\/db\/?8205."},{"key":"e_1_3_2_1_18_1","volume-title":"Defense Industry Daily","author":"UCAS.","year":"2005","unstructured":"J- UCAS. Boeing selects software for J-UCAS X-45C . Defense Industry Daily , 2005 . http:\/\/www.defenseindustrydail.com\/boeing-selects-software-for-jucas-x45c-01413\/. J-UCAS. Boeing selects software for J-UCAS X-45C. Defense Industry Daily, 2005. http:\/\/www.defenseindustrydail.com\/boeing-selects-software-for-jucas-x45c-01413\/."},{"key":"e_1_3_2_1_19_1","volume-title":"Military Embedded Systems","author":"The JB.","year":"2006","unstructured":"JB. The Jamaica VM brings Java technology to mission software in an unmanned aircraft by EADS . Military Embedded Systems , 2006 . http:\/\/www.mil-embedded.com\/news\/db\/?3302. JB. The JamaicaVM brings Java technology to mission software in an unmanned aircraft by EADS. Military Embedded Systems, 2006. http:\/\/www.mil-embedded.com\/news\/db\/?3302."},{"key":"e_1_3_2_1_20_1","volume-title":"International Computer Music Conference (ICMC)","author":"Juillerat N.","year":"2007","unstructured":"N. Juillerat , S. M\u00fcller Arisona , and S. Schubiger-Banz . Real-time, low latency audio processing in Java . In International Computer Music Conference (ICMC) , 2007 . N. Juillerat, S. M\u00fcller Arisona, and S. Schubiger-Banz. Real-time, low latency audio processing in Java. In International Computer Music Conference (ICMC), 2007."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620405.1620412"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2009.40"},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of DAta Systems In Aerospace (DASIA)","author":"Kalibera T.","year":"2009","unstructured":"T. Kalibera , M. Prochazka , F. Pizlo , J. Vitek , M. Zulianello , and M. Decky . Real-time Java in space: Potential benefits and open challenges . In Proceedings of DAta Systems In Aerospace (DASIA) , 2009 . T. Kalibera, M. Prochazka, F. Pizlo, J. Vitek, M. Zulianello, and M. Decky. Real-time Java in space: Potential benefits and open challenges. In Proceedings of DAta Systems In Aerospace (DASIA), 2009."},{"key":"e_1_3_2_1_24_1","author":"Lee E.","year":"1987","unstructured":"E. Lee and D. Messerschmitt . Pipeline interleaved programmable dsp's: Architecture. IEEE Transactions on Acoustics, Speech and Signal Processing , 1987 . E. Lee and D. Messerschmitt. Pipeline interleaved programmable dsp's: Architecture. IEEE Transactions on Acoustics, Speech and Signal Processing, 1987.","journal-title":"Pipeline interleaved programmable dsp's: Architecture. IEEE Transactions on Acoustics, Speech and Signal Processing"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450095.1450117"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_33"},{"key":"e_1_3_2_1_27_1","volume-title":"IBM","author":"McCloskey B.","year":"2008","unstructured":"B. McCloskey , D. Bacon , P. Cheng , and D. Grove . Staccato: A parallel and concurrent real-time compacting garbage collector for multiprocessors. Research report , IBM , 2008 . http:\/\/www.eecs.berkeley.edu\/billm\/rc24504.pdf. B. McCloskey, D. Bacon, P. Cheng, and D. Grove. Staccato: A parallel and concurrent real-time compacting garbage collector for multiprocessors. Research report, IBM, 2008. http:\/\/www.eecs.berkeley.edu\/billm\/rc24504.pdf."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"e_1_3_2_1_30_1","unstructured":"National Aeronautics and Space Administration. Dawn mission. http:\/\/dawn.jpl.nasa.gov 2009. National Aeronautics and Space Administration. Dawn mission. http:\/\/dawn.jpl.nasa.gov 2009."},{"key":"e_1_3_2_1_31_1","volume-title":"International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES)","author":"Pizlo F.","year":"2009","unstructured":"F. Pizlo , L. Ziarek , and J. Vitek . Towards Java on bare metal with the Fiji VM . In International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES) , 2009 . F. Pizlo, L. Ziarek, and J. Vitek. Towards Java on bare metal with the Fiji VM. In International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES), 2009."},{"key":"e_1_3_2_1_32_1","volume-title":"Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics (RTCA)","author":"RTCA","year":"1992","unstructured":"RTCA and EUROCAE. Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics (RTCA) , European Organization for Civil Aviation Electronics (EUROCAE) , DO178- B , 1992 . RTCA and EUROCAE. Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics (RTCA), European Organization for Civil Aviation Electronics (EUROCAE), DO178-B, 1992."},{"key":"e_1_3_2_1_33_1","volume-title":"Memory issues in PRET machines. Technical report","author":"Shah N.R.","year":"2008","unstructured":"N.R. Shah . Memory issues in PRET machines. Technical report , Columbia University , 2008 . N.R. Shah. Memory issues in PRET machines. Technical report, Columbia University, 2008."},{"key":"e_1_3_2_1_34_1","volume-title":"CKJM Chidamber and Kemerer metrics software, v1.6. Technical report","author":"Spinellis D.D.","year":"2005","unstructured":"D.D. Spinellis . CKJM Chidamber and Kemerer metrics software, v1.6. Technical report , Athens University of Economics and Business , 2005 . http:\/\/spinellis.gr\/sw\/ckjm. D.D. Spinellis. CKJM Chidamber and Kemerer metrics software, v1.6. Technical report, Athens University of Economics and Business, 2005. http:\/\/spinellis.gr\/sw\/ckjm."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620405.1620428"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Madrid Spain","acronym":"POPL '10"},"container-title":["Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1707790.1707800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T00:22:05Z","timestamp":1672964525000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1707790.1707800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,19]]},"references-count":36,"alternative-id":["10.1145\/1707790.1707800","10.1145\/1707790"],"URL":"https:\/\/doi.org\/10.1145\/1707790.1707800","relation":{},"subject":[],"published":{"date-parts":[[2010,1,19]]},"assertion":[{"value":"2010-01-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}