{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:04:11Z","timestamp":1726409051658},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319335995"},{"type":"electronic","value":"9783319336008"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_28","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T04:15:15Z","timestamp":1462853715000},"page":"319-325","source":"Crossref","is-referenced-by-count":4,"title":["A Super Industrial Application of PSGraph"],"prefix":"10.1007","author":[{"given":"Yuhui","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"O\u2019Halloran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Priiya","family":"G.","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-45221-5_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Grov","year":"2013","unstructured":"Grov, G., Kissinger, A., Lin, Y.: A graphical language for proof strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 324\u2013339. Springer, Heidelberg (2013)"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Grov, G., Kissinger, A., Lin, Y.: Tinker, tailor, solver, proof. In: UITP 2014, vol. 167 of ENTCS, pp. 23\u201334. Open Publishing Association (2014)","DOI":"10.4204\/EPTCS.167.5"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-06410-9_2","volume-title":"FM 2014: Formal Methods","author":"G Klein","year":"2014","unstructured":"Klein, G.: Proof engineering considered essential. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 16\u201321. Springer, Heidelberg (2014)"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Lin, Y., Bras, P.L., Grov, G.: Developing & debugging proof strategies by tinkering. In: TACAS (2016). to appear","DOI":"10.1007\/978-3-662-49674-9_37"},{"key":"28_CR6","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1999)"},{"issue":"2","key":"28_CR7","first-page":"237","volume":"20","author":"C O\u2019Halloran","year":"2013","unstructured":"O\u2019Halloran, C.: Automated verification of code automatically generated from Simulink. ASE 20(2), 237\u2013264 (2013)","journal-title":"ASE"},{"key":"28_CR8","unstructured":"O\u2019Halloran, C.: Nose-gear velocity-a challenge problem for software safety. In: Australian System Safety Conference (ASSC 2014), Held in Melbourne 28\u201330, May 2014 (2014)"},{"key":"28_CR9","doi-asserted-by":"publisher","first-page":"e12","DOI":"10.1017\/S0956796815000118","volume":"25","author":"B Ziliani","year":"2015","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. J. Funct. Program. 25, e12 (2015)","journal-title":"J. Funct. Program."}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33600-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,7]],"date-time":"2019-09-07T09:20:08Z","timestamp":1567848008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}