{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T08:00:27Z","timestamp":1648540827980},"reference-count":78,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,6,2]],"date-time":"2012-06-02T00:00:00Z","timestamp":1338595200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Informatik Spektrum"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s00287-012-0627-2","type":"journal-article","created":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T18:33:08Z","timestamp":1338575588000},"page":"271-279","source":"Crossref","is-referenced-by-count":2,"title":["Turing und die Verifikation"],"prefix":"10.1007","volume":"35","author":[{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"first","affiliation":[]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,2]]},"reference":[{"issue":"1\u20132","key":"627_CR1","first-page":"1","volume":"77","author":"JR Abrial","year":"2007","unstructured":"Abrial JR, Hallerstede S (2007) Refinement, decomposition and instantiation of discrete models: Application to Event-B. Fundam Informaticae 77(1\u20132):1\u201328","journal-title":"Fundam Informaticae"},{"key":"627_CR2","doi-asserted-by":"crossref","unstructured":"Alkassar E, B\u00f6hme S, Mehlhorn K, Rizkallah C (2011) Verification of certifying computations. In: Gopalakrishnan G, Qadeer S (eds) Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, Springer, pp 67\u201382","DOI":"10.1007\/978-3-642-22110-1_7"},{"key":"627_CR3","doi-asserted-by":"crossref","unstructured":"Alkassar E, Hillebrand MA, Leinenbach D, Schirmer NW, Starostin A (2008) The Verisoft approach to systems verification. In: Shankar N, Woodcock J (eds) Verified Software: Theories, Tools, Experiments (VSTTE), vol 5295 of Lecture Notes in Computer Science, Springer, pp 209\u2013224","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"627_CR4","doi-asserted-by":"crossref","unstructured":"Apt KR, de Boer FS, Olderog ER (2009) Verification of Sequential and Concurrent Programs, 3rd, extended edn. Springer","DOI":"10.1007\/978-1-84882-745-5"},{"issue":"3","key":"627_CR5","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","unstructured":"Apt KR, Francez N, de Roever WP (1980) A proof system for communicating sequential processes. ACM Trans Prog Lang Syst 2(3):359\u2013385","journal-title":"ACM Trans Prog Lang Syst"},{"key":"627_CR6","volume-title":"Program Construction and Verification","author":"RC Backhouse","year":"1986","unstructured":"Backhouse RC (1986) Program Construction and Verification. Prentice-Hall International, Englewood Cliffs, NJ"},{"key":"627_CR7","unstructured":"Baier C, Katoen JP (2008) Principles of Model Checking. MIT Press"},{"key":"627_CR8","doi-asserted-by":"crossref","unstructured":"Balser M, Reif W, Schellhorn G, Stenzel K, Thums A (2000) Formal system development in KIV. In: Maibaum T (ed) Proc. Fundamental Approaches to Software Engineering, vol 1783 of Lecture Notes in Computer Science, Springer, pp 363\u2013366","DOI":"10.1007\/3-540-46428-X_25"},{"key":"627_CR9","doi-asserted-by":"crossref","unstructured":"Becker B, Podelski A, Damm W, Fr\u00e4nzle M, Olderog ER, Wilhelm R (2007) SFB\/TR 14 AVACS \u2013 Automatic Verification and Analysis of Complex Systems. it \u2013 Information Technology 49(2):118\u2013126","DOI":"10.1524\/itit.2007.49.2.118"},{"key":"627_CR10","doi-asserted-by":"crossref","unstructured":"Beckert B, H\u00e4hnle R, Schmitt PH (eds) (2007) Verification of Object-Oriented Software: The KeY Approach, vol 4334 of Lecture Notes in Computer Science. Springer","DOI":"10.1007\/978-3-540-69061-0"},{"key":"627_CR11","doi-asserted-by":"crossref","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer","DOI":"10.1007\/978-3-662-07964-5"},{"key":"627_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: PLDI. ACM, pp 196\u2013207","DOI":"10.1145\/781131.781153"},{"key":"627_CR13","unstructured":"Brockschmidt M, Otto C, Giesl J (2011) Modular termination proofs of recursive Java bytecode programs by term rewriting. In: Schmidt-Schau\u00df M (ed) RTA, vol 10 of LIPIcs. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, pp 155\u2013170"},{"key":"627_CR14","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J B\u00fcchi","year":"1969","unstructured":"B\u00fcchi J, Landweber L (1969) Solving sequential conditions by finite-state strategies. Trans Amer Math Society 138:367\u2013378","journal-title":"Trans Amer Math Society"},{"key":"627_CR15","unstructured":"Church A (1957) Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol 1. Cornell Univ, Ithaca, NY, pp 3\u201350"},{"issue":"1","key":"627_CR16","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"EM Clarke","year":"1979","unstructured":"Clarke EM (1979) Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J ACM 26(1):129\u2013147","journal-title":"J ACM"},{"issue":"11","key":"627_CR17","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke EM, Emerson EA, Sifakis J (2009) Model checking: algorithmic verification and debugging. Commun ACM 52(11):74\u201384","journal-title":"Commun ACM"},{"key":"627_CR18","unstructured":"Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, Ness LA (1993) Verification of the Futurebus+ cache coherence protocol. In: Agnew D, Claesen LJM, Camposano R (eds) Proc. 11th IFIP WG 10.2 Intern. Conf. on Computer Hardware Description Languages and their Applications (CHDL), vol A-32 of IFIP Transactions. North-Holland, pp 15\u201330"},{"key":"627_CR19","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model Checking. MIT Press"},{"issue":"5","key":"627_CR20","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook B, Podelski A, Rybalchenko A (2011) Proving program termination. Commun ACM 54(5):88\u201398","journal-title":"Commun ACM"},{"key":"627_CR21","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"627_CR22","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (2012) An abstract interpretation framework for termination. In: Field J, Hicks M (eds) POPL. ACM, pp 245\u2013258","DOI":"10.1145\/2103656.2103687"},{"key":"627_CR23","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","volume":"20","author":"W Damm","year":"1983","unstructured":"Damm W, Josko B (1983) A sound and relatively omplete Hoare-logic for a language with higher type procedures. Acta Inf 20:59\u2013101","journal-title":"Acta Inf"},{"key":"627_CR24","unstructured":"de Bakker JW (1975) Inleiding bewijsmethoden. In: Colloquium Programmcorrectheid, MC Syllabus 21. Mathematisch Centrum, Amsterdam, pp 3\u201317"},{"key":"627_CR25","doi-asserted-by":"crossref","unstructured":"de Boer FS (1991) A proof system for the language POOL. In: de Bakker JW, de Roever WP, Rozenberg G (eds) Foundations of Object-Oriented Languages, vol 489 of Lecture Notes in Computer Science. Springer, pp 124\u2013150","DOI":"10.1007\/BFb0019442"},{"key":"627_CR26","unstructured":"de Roever WP, de Boer FS, Hannemann U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency Verification \u2013 Introduction to Compositional and Noncompositional Methods. Cambridge University Press"},{"key":"627_CR27","unstructured":"Dijkstra EW (1976) A Discipline of Programming. Prentice-Hall"},{"key":"627_CR28","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger K, Kupriyanov A, Finkbeiner B, Wehrheim H (2010) SLAB: A certifying model checker for infinite-state concurrent systems. In: Esparza J, Majumdar R (eds) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol 6015 of Lecture Notes in Computer Science. Springer, pp 271\u2013274","DOI":"10.1007\/978-3-642-12002-2_22"},{"issue":"3","key":"627_CR29","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson EA, Clarke EM (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Programming 2(3):241\u2013266","journal-title":"Sci Comput Programming"},{"key":"627_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3126-2","volume-title":"On a Method of Multiprogramming","author":"WHJ Feijen","year":"1999","unstructured":"Feijen WHJ, van Gasteren AJM (1999) On a Method of Multiprogramming. Springer, New York"},{"key":"627_CR31","doi-asserted-by":"crossref","unstructured":"Ferdinand C, Heckmann R, Langenbach M, Martin F, Schmidt M, Theiling H, Thesing S, Wilhelm R (2001) Reliable and precise WCET determination for a real-life processor. In: Henzinger TA, Kirsch CM (eds) EMSOFT, vol 2211 of Lecture Notes in Computer Science. Springer, pp 469\u2013485","DOI":"10.1007\/3-540-45449-7_32"},{"key":"627_CR32","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Schewe S (2005) Uniform distributed synthesis. In: Proc. LICS. IEEE Computer Society Press, pp 321\u2013330","DOI":"10.1109\/LICS.2005.53"},{"key":"627_CR33","doi-asserted-by":"crossref","unstructured":"Floyd RW (1967) Assigning meaning to programs. In: Schwartz JT (ed) Proc. Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science, American Mathematical Society, New York, pp 19\u201332","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"627_CR34","doi-asserted-by":"crossref","unstructured":"Giesl J, Thiemann R, Schneider-Kamp P, Falke S (2004) Automated termination proofs with AProVE. In: van Oostrom V (ed) RTA, vol 3091 of Lecture Notes in Computer Science. Springer, pp 210\u2013220","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"627_CR35","doi-asserted-by":"crossref","unstructured":"Gorn S (1967) Handling the growth by definition of mechanical languages. In: Proceedings of the 1967 Spring Joint Computer Conference, pp 213\u2013224","DOI":"10.1145\/1465482.1465513"},{"key":"627_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries D (1981) The Science of Programming. Springer, New York"},{"key":"627_CR37","doi-asserted-by":"crossref","unstructured":"Grumberg O, Veith H (eds) (2008) 25 Years of Model Checking \u2013 History, Achievements, Perspectives, vol 5000 of Lecture Notes in Computer Science. Springer","DOI":"10.1007\/978-3-540-69850-0"},{"key":"627_CR38","doi-asserted-by":"crossref","unstructured":"Halbwachs N (1998) Synchronous programming of reactive systems. In: Hu AJ, Vardi MY (eds) CAV, vol 1427 of Lecture Notes in Computer Science. Springer, pp 1\u201316","DOI":"10.1007\/BFb0028726"},{"key":"627_CR39","doi-asserted-by":"crossref","unstructured":"Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"627_CR40","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund K, Ro\u015fu G (2004) An overview of the runetime verification tool Java PathExplorer. Formal Methods Syst Des 24:189\u20132004","journal-title":"Formal Methods Syst Des"},{"key":"627_CR41","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12:576\u2013580, 583","journal-title":"Commun ACM"},{"key":"627_CR42","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1971) Procedures and parameters: an axiomatic approach. In: Engeler E (ed) Proceedings of Symposium on the Semantics of Algorithmic Languages, vol 188 of Lecture Notes in Mathematics. Springer, pp 102\u2013116","DOI":"10.1007\/BFb0059696"},{"key":"627_CR43","doi-asserted-by":"crossref","unstructured":"Ihlemann C, Sofronie-Stokkermans V (2010) On hierarchical reasoning in combinations of theories. In: Giesl J, H\u00e4hnle R (eds) International Joint Conference on Automated Reasoning (IJCAR), vol 6173 of Lecture Notes in Artificial Intelligence. Springer, pp 30\u201345","DOI":"10.1007\/978-3-642-14203-1_4"},{"issue":"6","key":"627_CR44","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein G, Andronick J, Elphinstone K, Heiser G, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2010) sel4: formal verification of an operating-system kernel. Commun ACM 53(6):107\u2013115","journal-title":"Commun ACM"},{"issue":"1","key":"627_CR45","first-page":"21","volume":"1","author":"J Kreiker","year":"2011","unstructured":"Kreiker J, Tarlecki A, Vardi MY, Wilhelm R (2011) Modeling, analysis, and verification \u2013 the formal methods manifesto 2010 (Dagstuhl Perspectives Workshop 10482). Dagstuhl Manifestos 1(1):21\u201340","journal-title":"Dagstuhl Manifestos"},{"key":"627_CR46","unstructured":"Kupferman O, Vardi MY (2001) Synthesizing distributed systems. In: Proc. LICS. IEEE Computer Society Press, pp 389\u2013398"},{"key":"627_CR47","doi-asserted-by":"crossref","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng SE-3:2:125\u2013143","DOI":"10.1109\/TSE.1977.229904"},{"key":"627_CR48","doi-asserted-by":"crossref","unstructured":"Langmaack H, Olderog ER (1980) Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely extensions. In: de Bakker JW, van Leeuwen J (eds) Automata, Languages and Programming, Proc 7th ICALP, vol 85 of Lecture Notes in Computer Science. Springer, pp 363\u2013373","DOI":"10.1007\/3-540-10003-2_84"},{"key":"627_CR49","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"GT Leavens","year":"2005","unstructured":"Leavens GT, Cheon Y, Clifton C, Ruby C, Cok DR (2005) How the design of JML accomodates both runtime assertion checking and formal verification. Sci Comput Prog 55:185\u2013208","journal-title":"Sci Comput Prog"},{"key":"627_CR50","doi-asserted-by":"crossref","unstructured":"Lee CS, Jones ND, Ben-Amram AM (2001) The size-change principle for program termination. In: POPL, pp 81\u201392","DOI":"10.1145\/360204.360210"},{"issue":"7","key":"627_CR51","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"key":"627_CR52","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/BF00289266","volume":"15","author":"G Levin","year":"1981","unstructured":"Levin G, Gries D (1981) A proof technique for communicating sequential processes. Acta Inf 15:281\u2013302","journal-title":"Acta Inf"},{"issue":"3","key":"627_CR53","first-page":"93","volume":"17","author":"G Lowe","year":"1996","unstructured":"Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Softw Concepts Tools 17(3):93\u2013102","journal-title":"Softw Concepts Tools"},{"key":"627_CR54","volume-title":"The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification. Springer, New York"},{"key":"627_CR55","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems \u2013 Safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal Verification of Reactive Systems \u2013 Safety. Springer, New York"},{"issue":"2","key":"627_CR56","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell RM, Mehlhorn K, N\u00e4her S, Schweitzer P (2011) Certifying algorithms. Comput Sci Rev 5(2):119\u2013161","journal-title":"Comput Sci Rev"},{"key":"627_CR57","unstructured":"Meyer B (1997) Object-Oriented Software Construction, 2nd edn. Prentice Hall"},{"key":"627_CR58","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming: Programming Theory for Distributed Applications","author":"J Misra","year":"2001","unstructured":"Misra J (2001) A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer, New York"},{"key":"627_CR59","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan C (1994) Programming from Specifications, 2nd edn. Prentice-Hall International, London","edition":"2"},{"key":"627_CR60","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"FL Morris","year":"1984","unstructured":"Morris FL, Jones CB (1984) An early program proof by Alan Turing. Ann Hist Comput 6:139\u2013143","journal-title":"Ann Hist Comput"},{"key":"627_CR61","doi-asserted-by":"crossref","unstructured":"Nicolescu G, Mosterman P (2009) Model-Based Design for Embedded Systems (Computational Analysis, Synthesis, and Design of Dynamic Systems). CRC Press","DOI":"10.1201\/9781420067859"},{"key":"627_CR62","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, vol 2283 of Lecture Notes in Computer Science. Springer","DOI":"10.1007\/3-540-45949-9"},{"key":"627_CR63","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00261258","volume":"16","author":"ER Olderog","year":"1981","unstructured":"Olderog ER (1981) Sound and complete Hoare-like calculi based on copy rules. Acta Inf 16:161\u2013197","journal-title":"Acta Inf"},{"key":"627_CR64","doi-asserted-by":"crossref","unstructured":"Olderog ER (1983) A characterization of Hoare\u2019s logic for programs with Pascal-like procedures. In: Proc. 15th ACM Symp. on Theory of Computing (STOC). ACM, pp 320\u2013329","DOI":"10.1145\/800061.808761"},{"key":"627_CR65","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inf 6:319\u2013340","journal-title":"Acta Inf"},{"key":"627_CR66","unstructured":"Owre S, Shankar N. Writing PVS proof strategies. In: Archer M, Vito BD, Mu\u00f1oz C (eds) Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), number CP-2003-212448 in NASA Conference Publication, Hampton, VA, Sept. 2003. NASA Langley Research Center, pp 1\u201315"},{"key":"627_CR67","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proc. 18th IEEE Symposium on Foundations of Computer Science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"627_CR68","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1990) Distributed reactive systems are hard to synthesize. In: Proc. FOCS. IEEE Computer Society Press, pp 746\u2013757","DOI":"10.1109\/FSCS.1990.89597"},{"key":"627_CR69","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: 19th IEEE Symp. on Logic in Computer Science (LICS). IEEE Computer Society, pp 32\u201341","DOI":"10.1109\/LICS.2004.1319598"},{"key":"627_CR70","doi-asserted-by":"crossref","unstructured":"Queille JP, Sifakis J (1981) Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming, Paris","DOI":"10.1007\/3-540-11494-7_22"},{"key":"627_CR71","doi-asserted-by":"crossref","unstructured":"Rabin M (1972) Automata on infinite objects and Church\u2019s problem. Trans. Amer. Math. Society, Providence RI","DOI":"10.1090\/cbms\/013"},{"issue":"3","key":"627_CR72","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv M, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217\u2013298","journal-title":"ACM Trans Program Lang Syst"},{"key":"627_CR73","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp P, Giesl J, Serebrenik A, Thiemann R (2009) Automated termination proofs for logic programs by term rewriting. ACM Trans Comput Log 11(1):2:1\u20132:52","DOI":"10.1145\/1614431.1614433"},{"key":"627_CR74","doi-asserted-by":"crossref","unstructured":"Seidl H, Wilhelm R, Hack S (2010) \u00dcbersetzerbau: Analyse und Transformation. Springer","DOI":"10.1007\/978-3-642-03331-5"},{"key":"627_CR75","unstructured":"Spivey JM (1992) The Z Notation: A Reference Manual, 2nd edn. Prentice Hall"},{"key":"627_CR76","doi-asserted-by":"crossref","unstructured":"Stephan W, Langenstein B, Nonnengart A, Rock G (2005) Verification support environment. In: Hutter D, Stephan W (eds) Mechanizing Mathematical Reasoning, vol 2605 of Lecture Notes in Computer Science. Springer, pp 476\u2013493","DOI":"10.1007\/978-3-540-32254-2_27"},{"key":"627_CR77","doi-asserted-by":"crossref","unstructured":"Thomas W (2009) Facets of synthesis: Revisiting Church\u2019s problem. In: de Alfaro L (ed) Foundations of Software Science and Computational Structures (FOSSACS), vol 5504 of Lecture Notes in Computer Science. Springer, pp 1\u201314","DOI":"10.1007\/978-3-642-00596-1_1"},{"key":"627_CR78","unstructured":"Turing AM (1949) On checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp 67\u201369"}],"container-title":["Informatik-Spektrum"],"original-title":[],"language":"de","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00287-012-0627-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00287-012-0627-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00287-012-0627-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,16]],"date-time":"2022-01-16T15:55:55Z","timestamp":1642348555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00287-012-0627-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,2]]},"references-count":78,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["627"],"URL":"https:\/\/doi.org\/10.1007\/s00287-012-0627-2","relation":{},"ISSN":["0170-6012","1432-122X"],"issn-type":[{"value":"0170-6012","type":"print"},{"value":"1432-122X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,2]]}}}