@InProceedings{Gan-Nav-Sch-Son-Stu_APLAS19,
  author    = {Graeme Gange and 
		Jorge A. Navas and 
		Peter Schachte and 
		Harald S{\o}ndergaard and 
		Peter J. Stuckey},
  title     = {Dissecting Widening: Separating Termination from Information},
  editor    = {A. W. Lin},
  booktitle = {Proceedings of the 17th Asian Symposium on Programming 
		Languages and Systems},
  series    = {Lecture Notes in Computer Science},
  volume    = {11893},
  pages     = {95--114},
  publisher = {Springer},
  year      = {2019},
  doi       = {10.1007/978-3-030-34175-6_6},
  abstract  = {Widening ensures or accelerates convergence of a program 
		analysis, and sometimes contributes a guarantee of soundness 
		that would otherwise be absent. In this paper we propose a 
		generalised view of widening, in which widening operates on 
		values that are not necessarily elements of the given abstract
		domain, although they must be in a correspondence, the details
		of which we spell out. We show that the new view generalizes 
		the traditional view, and that at least three distinct 
		advantages flow from the generalization. First, it gives a 
		handle on ``compositional safety'', the problem of creating 
		widening operators for product domains. Second, it adds a 
		degree of flexibility, allowing us to define variants of 
		widening, such as delayed widening, without resorting to 
		intrusive surgery on an underlying fixpoint engine.  Third, 
		it adds a degree of robustness, by making it difficult for
		an analysis implementor to make certain subtle (syntactic vs 
		semantic) category mistakes. The paper supports these claims 
		with examples. Our proposal has been implemented in a 
		state-of-the-art abstract interpreter, and we briefly report 
		on the changes that the revised view necessitated.},
  keywords  = {Fixed points, Abstract domains, Abstract interpretation, Widening},
}

{"_id":"v67Lr934LhdnppuYG","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-dissectingwideningseparatingterminationfrominformation-2019","author_short":["Gange, G.","Navas, J. A.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Jorge","A."],"propositions":[],"lastnames":["Navas"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Schachte"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]}],"title":"Dissecting Widening: Separating Termination from Information","editor":[{"firstnames":["A.","W."],"propositions":[],"lastnames":["Lin"],"suffixes":[]}],"booktitle":"Proceedings of the 17th Asian Symposium on Programming Languages and Systems","series":"Lecture Notes in Computer Science","volume":"11893","pages":"95–114","publisher":"Springer","year":"2019","doi":"10.1007/978-3-030-34175-6_6","abstract":"Widening ensures or accelerates convergence of a program analysis, and sometimes contributes a guarantee of soundness that would otherwise be absent. In this paper we propose a generalised view of widening, in which widening operates on values that are not necessarily elements of the given abstract domain, although they must be in a correspondence, the details of which we spell out. We show that the new view generalizes the traditional view, and that at least three distinct advantages flow from the generalization. First, it gives a handle on ``compositional safety'', the problem of creating widening operators for product domains. Second, it adds a degree of flexibility, allowing us to define variants of widening, such as delayed widening, without resorting to intrusive surgery on an underlying fixpoint engine. Third, it adds a degree of robustness, by making it difficult for an analysis implementor to make certain subtle (syntactic vs semantic) category mistakes. The paper supports these claims with examples. Our proposal has been implemented in a state-of-the-art abstract interpreter, and we briefly report on the changes that the revised view necessitated.","keywords":"Fixed points, Abstract domains, Abstract interpretation, Widening","bibtex":"@InProceedings{Gan-Nav-Sch-Son-Stu_APLAS19,\n author = {Graeme Gange and \n\t\tJorge A. Navas and \n\t\tPeter Schachte and \n\t\tHarald S{\\o}ndergaard and \n\t\tPeter J. Stuckey},\n title = {Dissecting Widening: Separating Termination from Information},\n editor = {A. W. Lin},\n booktitle = {Proceedings of the 17th Asian Symposium on Programming \n\t\tLanguages and Systems},\n series = {Lecture Notes in Computer Science},\n volume = {11893},\n pages = {95--114},\n publisher = {Springer},\n year = {2019},\n doi = {10.1007/978-3-030-34175-6_6},\n abstract = {Widening ensures or accelerates convergence of a program \n\t\tanalysis, and sometimes contributes a guarantee of soundness \n\t\tthat would otherwise be absent. In this paper we propose a \n\t\tgeneralised view of widening, in which widening operates on \n\t\tvalues that are not necessarily elements of the given abstract\n\t\tdomain, although they must be in a correspondence, the details\n\t\tof which we spell out. We show that the new view generalizes \n\t\tthe traditional view, and that at least three distinct \n\t\tadvantages flow from the generalization. First, it gives a \n\t\thandle on ``compositional safety'', the problem of creating \n\t\twidening operators for product domains. Second, it adds a \n\t\tdegree of flexibility, allowing us to define variants of \n\t\twidening, such as delayed widening, without resorting to \n\t\tintrusive surgery on an underlying fixpoint engine. Third, \n\t\tit adds a degree of robustness, by making it difficult for\n\t\tan analysis implementor to make certain subtle (syntactic vs \n\t\tsemantic) category mistakes. The paper supports these claims \n\t\twith examples. Our proposal has been implemented in a \n\t\tstate-of-the-art abstract interpreter, and we briefly report \n\t\ton the changes that the revised view necessitated.},\n keywords = {Fixed points, Abstract domains, Abstract interpretation, Widening},\n}\n\n","author_short":["Gange, G.","Navas, J. A.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"editor_short":["Lin, A. W."],"key":"Gan-Nav-Sch-Son-Stu_APLAS19","id":"Gan-Nav-Sch-Son-Stu_APLAS19","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-dissectingwideningseparatingterminationfrominformation-2019","role":"author","urls":{},"keyword":["Fixed points","Abstract domains","Abstract interpretation","Widening"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","BNGFBQQncqevukxoe","q5pWX4XZgAS4TQBof","yb3uN577XrYa7qf57","9jmvjAEoFta6emcgS","XqcrNTrCCBr9mSd37"],"keywords":["fixed points","abstract domains","abstract interpretation","widening"],"search_terms":["dissecting","widening","separating","termination","information","gange","navas","schachte","søndergaard","stuckey"],"title":"Dissecting Widening: Separating Termination from Information","year":2019}