{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:03:49Z","timestamp":1743041029891,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642115110"},{"type":"electronic","value":"9783642115127"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-11512-7_18","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T11:11:26Z","timestamp":1265886686000},"page":"277-299","source":"Crossref","is-referenced-by-count":1,"title":["Integrated and Automated Abstract Interpretation, Verification and Testing of C\/C++ Modules"],"prefix":"10.1007","author":[{"given":"Jan","family":"Peleska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"IEC\u00a061508 Functional safety of electric\/electronic\/programmable electronic safety-related systems. International Electrotechnical Commission (2006)","key":"18_CR1"},{"key":"18_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"1991","unstructured":"Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (1991)"},{"doi-asserted-by":"crossref","unstructured":"Badban, B., Fr\u00e4nzle, M., Peleska, J., Teige, T.: Test automation for hybrid systems. In: Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), Portland Oregon, USA (November 2006)","key":"18_CR3","DOI":"10.1145\/1188895.1188902"},{"key":"18_CR4","volume-title":"Test-Driven Development","author":"K. Beck","year":"2003","unstructured":"Beck, K.: Test-Driven Development. Addison-Wesley, Reading (2003)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P. Cousot","year":"2008","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min, A., Monniaux, D., Rival, X.: Combination of abstractions in the Astr\u00e9e static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 272\u2013300. Springer, Heidelberg (2008) (to appear)"},{"key":"18_CR6","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W.-P. de Roever","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press, Cambridge (1998)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., et al.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"unstructured":"European Committee for\u00a0Electrotechnical Standardization. EN 50128 \u2013 Railway applications \u2013 Communications, signalling and processing systems \u2013 Software for railway control and protection systems. CENELEC, Brussels (2001)","key":"18_CR8"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-540-70952-7_20","volume-title":"Formal Methods: Applications and Technology","author":"A. Fehnker","year":"2007","unstructured":"Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., Rauch, F.: Goanna - a static model checker. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol.\u00a04346, pp. 297\u2013300. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation (2007)","key":"18_CR10","DOI":"10.3233\/SAT190012"},{"unstructured":"GCC, the GNU Compiler Collection. The GIMPLE family of intermediate representations, \n                    http:\/\/gcc.gnu.org\/wiki\/GIMPLE","key":"18_CR11"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C\u00a0code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"key":"18_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0249-6","volume-title":"Applied Interval Analysis","author":"L. Jaulin","year":"2001","unstructured":"Jaulin, L., Kieffer, M., Didrit, O., Walter, \u00c9.: Applied Interval Analysis. Springer, London (2001)"},{"key":"18_CR14","volume-title":"Safeware","author":"N.G. Leveson","year":"1995","unstructured":"Leveson, N.G.: Safeware. Addison-Wesley, Reading (1995)"},{"unstructured":"L\u00f6ding, H.: Behandlung komplexer Datentypen in der automatischen Testdatengenerierung. Master\u2019s thesis, University of Bremen (May 2007)","key":"18_CR15"},{"unstructured":"Peleska, J., L\u00f6ding, H.: Static Analysis By Abstract Interpretation. University of Bremen, Centre of Information Technology (2008), \n                    http:\/\/www.informatik.uni-bremen.de\/agbs\/lehre\/ws0708\/ai\/saai_script.pdf","key":"18_CR16"},{"key":"18_CR17","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the 3rd intl Workshop on Systems Software Verification (SSV 2008)","author":"J. Peleska","year":"2008","unstructured":"Peleska, J., L\u00f6ding, H.: Symbolic and abstract interpretation for c\/c++ programs. In: Proceedings of the 3rd intl Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2008)"},{"unstructured":"Peleska, J., L\u00f6ding, H., Kotas, T.: Test automation meets static analysis. In: Koschke, R., Herzog, K.-H.R.O., Ronthaler, M. (eds.) Proceedings of the INFORMATIK 2007, Band 2, Bremen (Germany), September 24-27, pp. 280\u2013286 (2007)","key":"18_CR18"},{"unstructured":"Peleska, J., Zahlten, C.: Integrated automated test case generation and static analysis. In: Proceedings of the QA+Test 2007 International Conference on QA+Testing Embedded Systems, Bilbao (Spain), October 17-19 (2007)","key":"18_CR19"},{"issue":"6","key":"18_CR20","first-page":"71","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. TRENDS and CONTROVERSIES\u2013IEEE Magazine on Intelligent Systems\u00a021(6), 71\u201381 (2006)","journal-title":"TRENDS and CONTROVERSIES\u2013IEEE Magazine on Intelligent Systems"},{"unstructured":"SC-167. Software Considerations in Airborne Systems and Equipment Certification. RTCA (1992)","key":"18_CR21"},{"key":"18_CR22","volume-title":"Proc. IEEE 2nd Int\u2019l Symp. Industrial Embedded Systems (SIES 2007)","author":"B. Schlich","year":"2007","unstructured":"Schlich, B., Salewski, F., Kowalewski, S.: Applying model checking to an automotive microcontroller application. In: Proc. IEEE 2nd Int\u2019l Symp. Industrial Embedded Systems (SIES 2007). IEEE, Los Alamitos (2007)"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-36126-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Strichman","year":"2002","unstructured":"Strichman, O.: On solving presburger and linear arithmetic with sat. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 160\u2013170. Springer, Heidelberg (2002)"},{"key":"18_CR24","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part 2","author":"G.S. Tseitin","year":"1962","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, p. 115. Consultants Bureau, New York (1962)"},{"key":"18_CR25","volume-title":"Proceedings of the PLDI 2004","author":"A. Venet","year":"2004","unstructured":"Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded c programs. In: Proceedings of the PLDI 2004, Washington, DC, USA, June 9-11. ACM, New York (2004)"},{"unstructured":"Verified Systems International GmbH, Bremen. RT-Tester\u00a06.2 \u2013 User Manual (2007)","key":"18_CR26"}],"container-title":["Lecture Notes in Computer Science","Concurrency, Compositionality, and Correctness"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11512-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T07:16:40Z","timestamp":1715239000000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-11512-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642115110","9783642115127"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11512-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}