On undecidability results of real programming languages
Raimund Kirner, Wolf Zimmermann, Dirk Richter · University of Hertfordshire Research Archive (University of Hertfordshire) · 2009
Abstract. Often, it is argued that some problems in data-flow analysis such as e.g. worst case execution time analysis are undecidable (because the halting problem is) and therefore only a conservative approximation of the desired information is possible. In this paper, we show that the semantics for some important real programming languages – in particular those used for programming embedded devices – can be modeled as finite state systems or pushdown machines. This implies that the halting problem becomes decidable and therefore invalidates popular arguments for using conservative analysis. 1