{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:57Z","timestamp":1725511857707},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_4","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T06:37:44Z","timestamp":1210142264000},"page":"21-37","source":"Crossref","is-referenced-by-count":3,"title":["Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code"],"prefix":"10.1007","author":[{"given":"Bastian","family":"Schlich","sequence":"first","affiliation":[]},{"given":"Jann","family":"L\u00f6ll","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Kowalewski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Mehler, T.: Challenges and Applications of Assembly-Level Software Model Checking. PhD thesis, Universit\u00e4t Dortmund (2005)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Mercer, E.G., Jones, M.D.: Model checking machine code with the gnu debugger. In: SPIN Workshop on Model Checking of Software, San Francisco, USA (August 2005)","DOI":"10.1007\/11537328_20"},{"key":"#cr-split#-4_CR3.1","doi-asserted-by":"crossref","unstructured":"Schlich, B., Kowalewski, S.: [mc]square: A model checker for microcontroller code. In: Margaria, T., Philippou, A., Steffen, B. (eds.) Proc.\u00a02nd Int\u2019l Symp.\u00a0Leveraging Applications of Formal Methods, Verification and Validation (IEEE-ISoLA 2006) (2006);","DOI":"10.1109\/ISoLA.2006.62"},{"key":"#cr-split#-4_CR3.2","unstructured":"To appear in: IEEE proceedings"},{"key":"4_CR4","unstructured":"Schlich, B., Rohrbach, M., Weber, M., Kowalewski, S.: Model checking software for microcontrollers. Technical Report AIB-2006-11, RWTH Aachen University (August 2006)"},{"key":"4_CR5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Balakrishnan","year":"2007","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: Wysinwyx: What you see is not what you execute. In: Verified Software: Theories, Tools, Experiments. Springer, Heidelberg (to appear, 2007)"},{"key":"4_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"4_CR7","unstructured":"Schlich, B., Kowalewski, S.: An extendable architecture for model checking hardware-specific automotive microcontroller code. In: Schnieder, E., Tarnai, G. (eds.) Proc.\u00a06th Symp.\u00a0Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT 2007), Braunschweig, Germany, GZVB, pp. 202\u2013212 (2007)"},{"key":"#cr-split#-4_CR8.1","unstructured":"Schlich, B., Kowalewski, S.: Model checking c source code for embedded systems. In: Margaria, T., Steffen, B., Hinchey, M.G. (eds.) Proc.\u00a0IEEE\/NASA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (IEEE\/NASA ISoLA 2005), Maryland, USA, NASA, September 2005, pp. 65\u201377 (2005);"},{"key":"#cr-split#-4_CR8.2","unstructured":"NASA\/CP-2005-212788"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Proc. 18th\u00a0IEEE Real-Time Systems Symposium (RTSS 1997)","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. 18th\u00a0IEEE Real-Time Systems Symposium (RTSS 1997), pp. 14\u201324. IEEE Computer Society, Washington, DC, USA (1997)"},{"key":"4_CR10","unstructured":"Heljanko, K.: Model checking the branching time temporal logic ctl. Research Report A45, Helsinki University of Technology (May 1997)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/3-540-57208-2_31","volume-title":"CONCUR\u201993","author":"B. Vergauwen","year":"1993","unstructured":"Vergauwen, B., Lewi, J.: A linear local model checking algorithm for ctl. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 447\u2013461. Springer, Heidelberg (1993)"},{"key":"4_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/B:FORM.0000033963.55470.9e","volume":"25","author":"K. Yorav","year":"2004","unstructured":"Yorav, K., Grumberg, O.: Static analysis for state-space reductions preserving temporal logics. Form. Methods Syst. Des.\u00a025(1), 67\u201396 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"4_CR14","unstructured":"Quir\u00f3s, G.: Static byte-code analysis for state space reduction. Master\u2019s thesis, RWTH Aachen University (March 2006)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48234-2_18","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J.: The engineering of a model checker: The gnu i-protocol case study revisited. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 232\u2013244. Springer, Heidelberg (1999)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/1111542.1111551","volume-title":"Proc. 2006 ACM SIGPLAN Symp. Partial evaluation and semantics-based program manipulation (PEPM 2006)","author":"M. Lewis","year":"2006","unstructured":"Lewis, M., Jones, M.: A dead variable analysis for explicit model checking. In: Proc. 2006 ACM SIGPLAN Symp. Partial evaluation and semantics-based program manipulation (PEPM 2006), pp. 48\u201357. ACM Press, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:28:40Z","timestamp":1619522920000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_4","relation":{},"subject":[]}}