{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:05Z","timestamp":1776333485221,"version":"3.51.2"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,10,18]],"date-time":"2012-10-18T00:00:00Z","timestamp":1350518400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10703-012-0176-y","type":"journal-article","created":{"date-parts":[[2012,10,17]],"date-time":"2012-10-17T19:08:59Z","timestamp":1350500939000},"page":"221-261","source":"Crossref","is-referenced-by-count":19,"title":["Loop summarization using state and transition invariants"],"prefix":"10.1007","volume":"42","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,18]]},"reference":[{"key":"176_CR1","first-page":"43","volume-title":"Workshop on program analysis for software tools and engineering","author":"A Aiken","year":"2007","unstructured":"Aiken A, Bugrara S, Dillig I, Dillig T, Hackett B, Hawkins P (2007) An overview of the Saturn project. In: Das M, Grossman D (eds) Workshop on program analysis for software tools and engineering. ACM, New York, pp\u00a043\u201348"},{"key":"176_CR2","first-page":"49","volume-title":"Classics in software engineering","author":"E Ashcroft","year":"1979","unstructured":"Ashcroft E, Manna Z (1979) The translation of \u2018go to\u2019 programs to \u2018while\u2019 programs. In: Classics in software engineering. Yourdon Press, Upper Saddle River, pp\u00a049\u201361"},{"key":"176_CR3","series-title":"Lecture notes in computer science","first-page":"267","volume-title":"Verification, model checking, and abstract interpretation (VMCAI)","author":"I Balaban","year":"2006","unstructured":"Balaban I, Cohen A, Pnueli A (2006) Ranking abstraction of recursive programs. In: Emerson E, Namjoshi K (eds) Verification, model checking, and abstract interpretation (VMCAI). Lecture notes in computer science, vol\u00a03855. Springer, Berlin, pp\u00a0267\u2013281"},{"key":"176_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer aided verification (CAV)","author":"T Ball","year":"2001","unstructured":"Ball T, Rajamani SK (2001) The SLAM toolkit. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a02102. Springer, Berlin, pp\u00a0260\u2013264"},{"key":"176_CR5","volume-title":"Logical methods in computer science","author":"AM Ben-Amram","year":"2009","unstructured":"Ben-Amram AM, Lee CS (2009) Ranking functions for size-change termination II. In: Logical methods in computer science, vol\u00a05. Chapter\u00a08"},{"key":"176_CR6","series-title":"POPL\u201907","first-page":"211","volume-title":"Principles of programming languages (POPL)","author":"J Berdine","year":"2007","unstructured":"Berdine J, Chawdhary A, Cook B, Distefano D, O\u2019Hearn P (2007) Variance analyses from invariance analyses. In: Principles of programming languages (POPL). POPL\u201907. ACM, New York, pp\u00a0211\u2013224. doi: 10.1145\/1190216.1190249"},{"key":"176_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer aided verification (CAV)","author":"D Beyer","year":"2006","unstructured":"Beyer D, Henzinger TA, Th\u00e9oduloz G (2006) Lazy shape analysis. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a04144. Springer, Berlin, pp\u00a0532\u2013546"},{"key":"176_CR8","first-page":"118","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:118\u2013149","journal-title":"Adv Comput"},{"key":"176_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/FAMCAD.2007.35","volume-title":"Formal methods in computer-aided design (FMCAD)","author":"R Cavada","year":"2007","unstructured":"Cavada R, Cimatti A, Franz\u00e9n A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: Formal methods in computer-aided design (FMCAD). IEEE Computer Society, Los Alamitos, pp\u00a069\u201376"},{"issue":"6","key":"176_CR10","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in C. IEEE Trans Softw Eng 30(6):388\u2013402","journal-title":"IEEE Trans Softw Eng"},{"key":"176_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-540-89754-5","volume-title":"Programming languages and systems","author":"A Chawdhary","year":"2008","unstructured":"Chawdhary A, Cook B, Gulwani S, Sagiv M, Yang H (2008) Ranking abstractions. In: Drossopoulou S (ed) Programming languages and systems. Lecture notes in computer science, vol\u00a04960. Springer, Berlin, pp\u00a0148\u2013162"},{"key":"176_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer aided verification","author":"E Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson E, Sistla A (eds) Computer aided verification. Lecture notes in computer science, vol\u00a01855. Springer, Berlin, pp\u00a0154\u2013169"},{"key":"176_CR13","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"176_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A\u00a0tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a02988. Springer, Berlin, pp\u00a0168\u2013176"},{"issue":"2\u20133","key":"176_CR15","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Kroening D, Sharygina N, Yorav K (2004) Predicate abstraction of ANSI-C programs using SAT. Form Methods Syst Des 25(2\u20133):105\u2013127","journal-title":"Form Methods Syst Des"},{"key":"176_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"EM Clarke","year":"2005","unstructured":"Clarke EM, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science. Springer, Berlin, pp\u00a0570\u2013574"},{"key":"176_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"International symposium on static analysis (SAS)","author":"B Cook","year":"2005","unstructured":"Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: International symposium on static analysis (SAS). Lecture notes in computer science, vol\u00a03672. Springer, Berlin, pp\u00a087\u2013101"},{"key":"176_CR18","first-page":"415","volume-title":"Programming language design and implementation (PLDI)","author":"B Cook","year":"2006","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Programming language design and implementation (PLDI). ACM, New York, pp\u00a0415\u2013426"},{"key":"176_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer aided verification (CAV)","author":"B Cook","year":"2008","unstructured":"Cook B, Gulwani S, Lev-Ami T, Rybalchenko A, Sagiv M (2008) Proving conditional termination. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a05123. Springer, Berlin, pp\u00a0328\u2013340"},{"issue":"3","key":"176_CR20","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10703-009-0087-8","volume":"35","author":"B Cook","year":"2009","unstructured":"Cook B, Podelski A, Rybalchenko A (2009) Summarization for termination: no return! Form Methods Syst Des 35(3):369\u2013387","journal-title":"Form Methods Syst Des"},{"key":"176_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"B Cook","year":"2010","unstructured":"Cook B, Kroening D, Ruemmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a06015. Springer, Berlin, pp\u00a0236\u2013250"},{"key":"176_CR22","first-page":"238","volume-title":"Principles of programming languages (POPL)","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a\u00a0unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages (POPL), pp\u00a0238\u2013252"},{"key":"176_CR23","first-page":"84","volume-title":"Principles of programming languages (POPL)","author":"P Cousot","year":"1978","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Principles of programming languages (POPL), pp\u00a084\u201396"},{"key":"176_CR24","first-page":"1","volume-title":"Proceedings of the workshop on advances in verification (WAVE)","author":"D Dams","year":"2000","unstructured":"Dams D, Gerth R, Grumberg O (2000) A\u00a0heuristic for the automatic generation of ranking functions. In: Proceedings of the workshop on advances in verification (WAVE), pp\u00a01\u20138"},{"key":"176_CR25","first-page":"155","volume-title":"Programming language design and implementation (PLDI)","author":"N Dor","year":"2003","unstructured":"Dor N, Rodeh M, Sagiv S (2003) CSSV: towards a realistic tool for statically detecting all buffer overflows in\u00a0C. In: Programming language design and implementation (PLDI), pp\u00a0155\u2013167"},{"key":"176_CR26","first-page":"48","volume-title":"TACAS","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva V, Haller L, Kroening D, Tautschnig M (2012) Numeric bounds analysis with conflict-driven learning. In: TACAS. Springer, Berlin, pp\u00a048\u201363"},{"key":"176_CR27","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: formal methods for increasing software productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC\/Java. In: Oliveira J, Zave P (eds) FME 2001: formal methods for increasing software productivity. Lecture notes in computer science. Springer, Berlin, pp\u00a0500\u2013517"},{"key":"176_CR28","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the ACM SIGPLAN 2002 conference on programming language design and implementation (PLDI\u201902)","author":"C Flanagan","year":"2002","unstructured":"Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 conference on programming language design and implementation (PLDI\u201902). ACM, New York, pp\u00a0234\u2013245. doi: 10.1145\/512529.512558"},{"key":"176_CR29","unstructured":"Frama-C: http:\/\/frama-c.com\/"},{"key":"176_CR30","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-73368-3_10","volume-title":"Computer aided verification (CAV)","author":"D Gopan","year":"2007","unstructured":"Gopan D, Reps TW (2007) Low-level library analysis and summarization. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a04590. Springer, Berlin, pp\u00a068\u201381"},{"key":"176_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer aided verification (CAV)","author":"S Graf","year":"1997","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a01254. Springer, Berlin, pp\u00a072\u201383. doi: 10.1007\/3-540-63166-6_10"},{"key":"176_CR32","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"BS Gulavani","year":"2006","unstructured":"Gulavani BS, Rajamani SK (2006) Counterexample driven refinement for abstract interpretation. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp\u00a0474\u2013488"},{"issue":"16","key":"176_CR33","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1016\/j.ipl.2010.05.021","volume":"110","author":"BS Gulavani","year":"2010","unstructured":"Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2010) Refining abstract interpretations. Inf Process Lett 110(16):666\u2013671","journal-title":"Inf Process Lett"},{"key":"176_CR34","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1145\/1480881.1480912","volume-title":"POPL\u201909: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"S Gulwani","year":"2009","unstructured":"Gulwani S, Lev-Ami T, Sagiv M (2009) A\u00a0combination framework for tracking partition sizes. In: POPL\u201909: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp\u00a0239\u2013251. doi: 10.1145\/1480881.1480912"},{"key":"176_CR35","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1145\/1480881.1480898","volume-title":"POPL\u201909: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"S Gulwani","year":"2009","unstructured":"Gulwani S, Mehra KK, Chilimbi T (2009) Speed: precise and efficient static estimation of program computational complexity. In: POPL\u201909: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp\u00a0127\u2013139. doi: 10.1145\/1480881.1480898"},{"key":"176_CR36","series-title":"Lecture notes in computer science","first-page":"22","volume-title":"Static analysis","author":"M Heizmann","year":"2011","unstructured":"Heizmann M, Jones N, Podelski A (2011) Size-change termination and transition invariants. In: Cousot\u00a0R, Martel M (eds) Static analysis. Lecture notes in computer science, vol\u00a06337. Springer, Berlin, pp\u00a022\u201350"},{"key":"176_CR37","first-page":"58","volume-title":"Principles of programming languages (POPL)","author":"TA Henzinger","year":"2002","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Principles of programming languages (POPL). ACM, New York, pp\u00a058\u201370"},{"issue":"10","key":"176_CR38","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"T Hoare","year":"1969","unstructured":"Hoare T (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580. doi: 10.1145\/363235.363259","journal-title":"Commun ACM"},{"key":"176_CR39","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/347324.383378","volume-title":"Proceedings of the international symposium on software testing and analysis (ISSTA)","author":"D Jackson","year":"2000","unstructured":"Jackson D, Vaziri M (2000) Finding bugs with a constraint solver. In: Proceedings of the international symposium on software testing and analysis (ISSTA), pp\u00a014\u201325"},{"key":"176_CR40","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/11691372_16","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"D Kroening","year":"2006","unstructured":"Kroening D, Sharygina N (2006) Approximating predicate images for bit-vector logic. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp\u00a0242\u2013256"},{"key":"176_CR41","series-title":"Lecture notes in computer science","volume-title":"International conference on computer-aided verification (CAV)","author":"D Kroening","year":"2010","unstructured":"Kroening D, Sharygina N, Tsitovich A, Wintersteiger CM (2010) Termination analysis with compositional transition invariants. In: International conference on computer-aided verification (CAV). Lecture notes in computer science, vol\u00a06174. Springer, Edinburgh"},{"key":"176_CR42","first-page":"389","volume-title":"Automated software engineering (ASE)","author":"K Ku","year":"2007","unstructured":"Ku K, Hart TE, Chechik M, Lie D (2007) A\u00a0buffer overflow benchmark for software model checkers. In: Automated software engineering (ASE). ACM, New York, pp\u00a0389\u2013392"},{"key":"176_CR43","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer aided verification (CAV)","author":"SK Lahiri","year":"2005","unstructured":"Lahiri SK, Ball T, Cook B (2005) Predicate abstraction via symbolic decision procedures. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a03576. Springer, Berlin, pp\u00a024\u201338"},{"key":"176_CR44","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer aided verification (CAV)","author":"SK Lahiri","year":"2006","unstructured":"Lahiri SK, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: Computer aided verification (CAV). Lecture notes in computer science, vol\u00a04144. Springer, Berlin, pp\u00a0424\u2013437"},{"key":"176_CR45","first-page":"81","volume-title":"Principles of programming languages (POPL)","author":"CS Lee","year":"2001","unstructured":"Lee CS, Jones ND, Ben-Amram AM (2001) The size-change principle for program termination. In: Principles of programming languages (POPL), vol\u00a036. ACM, New York, pp\u00a081\u201392. doi: 10.1145\/360204.360210"},{"key":"176_CR46","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Proceedings of the 16th international conference on logic for programming, artificial intelligence, and reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th international conference on logic for programming, artificial intelligence, and reasoning. Lecture notes in computer science, vol\u00a06355. Springer, Berlin, pp\u00a0348\u2013370. URL: http:\/\/dl.acm.org\/citation.cfm?id=1939141.1939161"},{"key":"176_CR47","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static analysis (SAS)","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami T, Sagiv S (2000) TVLA: a system for implementing static analyses. In: Static analysis (SAS). Lecture notes in computer science, vol\u00a01824. Springer, Berlin, pp\u00a0280\u2013301"},{"key":"176_CR48","series-title":"Lecture notes in computer science","first-page":"273","volume-title":"Program analysis and compilation (PAC)","author":"R Manevich","year":"2006","unstructured":"Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M (2006) Abstract counterexample-based refinement for powerset domains. In: Program analysis and compilation (PAC). Lecture notes in computer science, vol\u00a04444. Springer, Berlin, pp\u00a0273\u2013292"},{"key":"176_CR49","unstructured":"Moy Y (2009) Automatic modular static safety checking for C programs. PhD thesis, Universit\u00e9 Paris-Sud. URL: http:\/\/www.lri.fr\/~marche\/moy09phd.pdf"},{"key":"176_CR50","first-page":"32","volume-title":"IEEE symposium on logic in computer science (LICS)","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: IEEE symposium on logic in computer science (LICS). IEEE Computer Society, Los Alamitos, pp\u00a032\u201341"},{"key":"176_CR51","first-page":"245","volume-title":"Practical aspects of declarative languages (PADL)","author":"A Podelski","year":"2007","unstructured":"Podelski A, Rybalchenko A (2007) ARMC: the logical choice for software model checking with abstraction refinement. In: Practical aspects of declarative languages (PADL). Springer, Berlin, pp\u00a0245\u2013259"},{"key":"176_CR52","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/199448.199462","volume-title":"POPL\u201995: proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"T Reps","year":"1995","unstructured":"Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL\u201995: proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp\u00a049\u201361. doi: 10.1145\/199448.199462"},{"key":"176_CR53","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, model checking, and abstract interpretation (VMCAI)","author":"TW Reps","year":"2004","unstructured":"Reps TW, Sagiv S, Yorsh G (2004) Symbolic implementation of the best transformer. In: Verification, model checking, and abstract interpretation (VMCAI). Lecture notes in computer science, vol\u00a02937. Springer, Berlin, pp\u00a0252\u2013266"},{"key":"176_CR54","first-page":"94","volume-title":"International conference on computer design (ICCD)","author":"J Scott","year":"1999","unstructured":"Scott J, Lee LH, Chin A, Arends J, Moyer B (1999) Designing the m\u22c5coretm m3 cpu architecture. In: International conference on computer design (ICCD), pp\u00a094\u2013101"},{"key":"176_CR55","volume-title":"Program flow analysis: theory and applications","author":"M Sharir","year":"1981","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Program flow analysis: theory and applications, Prentice-Hall, New York"},{"key":"176_CR56","unstructured":"SNU real-time benchmarks. http:\/\/archi.snu.ac.kr\/realtime\/benchmark\/"},{"key":"176_CR57","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1145\/512950.512963","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL\u201977)","author":"N Suzuki","year":"1977","unstructured":"Suzuki N, Ishihata K (1977) Implementation of an array bound checker. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL\u201977). ACM, New York, pp\u00a0132\u2013143. doi: 10.1145\/512950.512963"},{"issue":"3","key":"176_CR58","doi-asserted-by":"crossref","first-page":"594","DOI":"10.1145\/322261.322273","volume":"28","author":"RE Tarjan","year":"1981","unstructured":"Tarjan RE (1981) Fast algorithms for solving path problems. J ACM 28(3):594\u2013614. http:\/\/doi.acm.org\/10.1145\/322261.322273","journal-title":"J ACM"},{"issue":"42","key":"176_CR59","first-page":"230","volume":"2","author":"AM Turing","year":"1936","unstructured":"Turing AM (1936) On computable numbers, with an application to the entscheidungsproblem. Proc Lond Math Soc 2(42):230\u2013265","journal-title":"Proc Lond Math Soc"},{"key":"176_CR60","first-page":"67","volume-title":"Report of a conference on high speed automatic calculating machines","author":"AM Turing","year":"1949","unstructured":"Turing AM (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines. Cambridge, pp\u00a067\u201369"},{"key":"176_CR61","first-page":"97","volume-title":"International symposium on foundations of software engineering","author":"M Zitser","year":"2004","unstructured":"Zitser M, Lippmann R, Leek T (2004) Testing static analysis tools using exploitable buffer overflows from open source code. In: International symposium on foundations of software engineering. ACM, New York, pp\u00a097\u2013106"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0176-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0176-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0176-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T07:46:55Z","timestamp":1687765615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0176-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,18]]},"references-count":61,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["176"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0176-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,18]]}}}