{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:57:04Z","timestamp":1743130624873,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319036014"},{"type":"electronic","value":"9783319036021"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-03602-1_1","type":"book-chapter","created":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T21:03:55Z","timestamp":1389215035000},"page":"1-11","source":"Crossref","is-referenced-by-count":0,"title":["Software Quality Assurance by Static Program Analysis"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Wilhelm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"AbsSint, \n                    \n                      http:\/\/www.absint.com\/ait"},{"key":"1_CR2","unstructured":"AbsSint, \n                    \n                      http:\/\/www.absint.com\/stackanalyzer\/index.htm"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI 2003","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Riva, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI 2003, pp. 196\u2013207. ACM, New York (2003)"},{"key":"1_CR4","first-page":"238","volume-title":"POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C. Ferdinand","year":"2001","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 469\u2013485. Springer, Heidelberg (2001)"},{"key":"1_CR6","unstructured":"Ferdinand, C., Heckmann, R., Sergent, T.L., Lopes, D., Martin, B., Fornari, X., Martin, F.: Combining a high-level design tool for safety-critical systems with a tool for WCET analysis on executables. In: ERTS2 (2008)"},{"issue":"2-3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1023\/A:1008186323068","volume":"17","author":"C. Ferdinand","year":"1999","unstructured":"Ferdinand, C., Wilhelm, R.: Efficient and precise cache behavior prediction for real-time systems. Real-Time Systems\u00a017(2-3), 131\u2013181 (1999)","journal-title":"Real-Time Systems"},{"key":"1_CR8","unstructured":"K\u00e4stner, D., Ferdinand, C.: Efficient verification of non-functional safety properties by abstract interpretation: Timing, stack consumption, and absence of runtime errors. In: Proceedings of the 29th International System Safety Conference, ISSC 2011, Las Vegas (2011)"},{"key":"1_CR9","unstructured":"K\u00e4stner, D., Ferdinand, C.: Static verification of non-functional requirements in the ISO-26262. Embedded World Congress (2012)"},{"key":"1_CR10","unstructured":"K\u00e4stner, D., Kiffmeier, U., Fleischer, D., Nenova, S., Schlickling, M., Ferdinand, C.: Integrating model-based code generators with static program analyzers. In: Embedded World. Design & Elektronik (2013)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Fischer, P.C., Ullman, J.D. (eds.) POPL, pp. 194\u2013206. ACM (1973)","DOI":"10.1145\/512927.512945"},{"issue":"1","key":"1_CR12","first-page":"21","volume":"1","author":"J. Kreiker","year":"2011","unstructured":"Kreiker, J., Tarlecki, A., Vardi, M.Y., Wilhelm, R.: Modeling, Analysis, and Verification - the Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482). Dagstuhl Manifestos\u00a01(1), 21\u201340 (2011)","journal-title":"Dagstuhl Manifestos"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formally verifying a compiler: Why? how? how far? In: CGO. IEEE (2011)","DOI":"10.1109\/CGO.2011.5764668"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T.W., Sagiv, S., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: ISSTA, pp. 26\u201338 (2000)","DOI":"10.1145\/347636.348031"},{"key":"1_CR15","unstructured":"PolySpace, \n                    \n                      http:\/\/www.mathworks.de\/products\/polyspace\/"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Raymond, P., Maiza, C., Parent-Vigouroux, C., Carrier, F.: Timing analysis enhancement for synchronous program. In: RNTS (2013)","DOI":"10.1145\/2516821.2516841"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Seidl, H., Wilhelm, R., Hack, S.: Compiler Design - Analysis and Transformation. Springer (2012)","DOI":"10.1007\/978-3-642-17548-0"},{"key":"1_CR18","unstructured":"Souyris, J., Pavec, E.L., Himbert, G., Jgu, V., Borios, G.: Computing the worst-case execution time of an avionics program by abstract interpretation. In: Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis, pp. 21\u201324 (2005)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Wilhelm, R.: Determining bounds on execution times. In: Zurawski, R. (ed.) Handbook on Embedded Systems, ch. 14. CRC Press (2006)","DOI":"10.1201\/9781420038163.ch14"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: Hankin, C., Schmidt, D. (eds.) POPL, pp. 27\u201340. ACM (2001)","DOI":"10.1145\/373243.360206"}],"container-title":["Lecture Notes in Business Information Processing","Software Quality. Model-Based Approaches for Advanced Software and Systems Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03602-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T21:12:13Z","timestamp":1558818733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03602-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319036014","9783319036021"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03602-1_1","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2014]]}}}