@inproceedings{Gan-Nav-Sch-Son-Stu_SAS16,
  author    = {Graeme Gange and 
		Jorge Navas and 
		Peter Schachte and
                Harald S{\o}ndergaard and 
		Peter J. Stuckey},
  title     = {Exploiting Sparsity in Difference-Bound Matrices},
  editor    = {X. Rival},
  booktitle = {Static Analysis:
                Proceedings of the 23rd International Symposium},
  series    = {Lecture Notes in Computer Science},
  volume    = {9837},
  pages     = {189--211},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-662-53413-7},
  abstract  = {Relational numeric abstract domains are very important in 
		program analysis. Common domains, such as Zones and Octagons, 
		are usually conceptualised with weighted digraphs and 
		implemented using difference-bound matrices (DBMs). 
		Unfortunately, though conceptually simple, direct 
		implementations of graph-based domains tend to perform
		poorly in practice, and are impractical for analyzing large 
		code-bases. We propose new DBM algorithms that exploit 
		sparsity and closed operands. In particular, a new 
		representation which we call split normal form reduces graph
		density on typical abstract states. We compare the resulting 
		implementation with several existing DBM-based abstract 
		domains, and show that we can substantially reduce the time
		to perform full DBM analysis, without sacrificing precision.},
  keywords  = {Abstract domains, Abstract interpretation, Static analysis},
}

{"_id":"zxBJn6DWseomtcfwH","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-exploitingsparsityindifferenceboundmatrices-2016","author_short":["Gange, G.","Navas, J.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Jorge"],"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":"Exploiting Sparsity in Difference-Bound Matrices","editor":[{"firstnames":["X."],"propositions":[],"lastnames":["Rival"],"suffixes":[]}],"booktitle":"Static Analysis: Proceedings of the 23rd International Symposium","series":"Lecture Notes in Computer Science","volume":"9837","pages":"189–211","publisher":"Springer","year":"2016","doi":"10.1007/978-3-662-53413-7","abstract":"Relational numeric abstract domains are very important in program analysis. Common domains, such as Zones and Octagons, are usually conceptualised with weighted digraphs and implemented using difference-bound matrices (DBMs). Unfortunately, though conceptually simple, direct implementations of graph-based domains tend to perform poorly in practice, and are impractical for analyzing large code-bases. We propose new DBM algorithms that exploit sparsity and closed operands. In particular, a new representation which we call split normal form reduces graph density on typical abstract states. We compare the resulting implementation with several existing DBM-based abstract domains, and show that we can substantially reduce the time to perform full DBM analysis, without sacrificing precision.","keywords":"Abstract domains, Abstract interpretation, Static analysis","bibtex":"@inproceedings{Gan-Nav-Sch-Son-Stu_SAS16,\n author = {Graeme Gange and \n\t\tJorge Navas and \n\t\tPeter Schachte and\n Harald S{\\o}ndergaard and \n\t\tPeter J. Stuckey},\n title = {Exploiting Sparsity in Difference-Bound Matrices},\n editor = {X. Rival},\n booktitle = {Static Analysis:\n Proceedings of the 23rd International Symposium},\n series = {Lecture Notes in Computer Science},\n volume = {9837},\n pages = {189--211},\n publisher = {Springer},\n year = {2016},\n doi = {10.1007/978-3-662-53413-7},\n abstract = {Relational numeric abstract domains are very important in \n\t\tprogram analysis. Common domains, such as Zones and Octagons, \n\t\tare usually conceptualised with weighted digraphs and \n\t\timplemented using difference-bound matrices (DBMs). \n\t\tUnfortunately, though conceptually simple, direct \n\t\timplementations of graph-based domains tend to perform\n\t\tpoorly in practice, and are impractical for analyzing large \n\t\tcode-bases. We propose new DBM algorithms that exploit \n\t\tsparsity and closed operands. In particular, a new \n\t\trepresentation which we call split normal form reduces graph\n\t\tdensity on typical abstract states. We compare the resulting \n\t\timplementation with several existing DBM-based abstract \n\t\tdomains, and show that we can substantially reduce the time\n\t\tto perform full DBM analysis, without sacrificing precision.},\n keywords = {Abstract domains, Abstract interpretation, Static analysis},\n}\n\n","author_short":["Gange, G.","Navas, J.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"editor_short":["Rival, X."],"key":"Gan-Nav-Sch-Son-Stu_SAS16","id":"Gan-Nav-Sch-Son-Stu_SAS16","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-exploitingsparsityindifferenceboundmatrices-2016","role":"author","urls":{},"keyword":["Abstract domains","Abstract interpretation","Static analysis"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/zarajoy/testbibtex/refs/heads/main/test.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","BNGFBQQncqevukxoe","q5pWX4XZgAS4TQBof","yb3uN577XrYa7qf57","9jmvjAEoFta6emcgS","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["abstract domains","abstract interpretation","static analysis"],"search_terms":["exploiting","sparsity","difference","bound","matrices","gange","navas","schachte","søndergaard","stuckey"],"title":"Exploiting Sparsity in Difference-Bound Matrices","year":2016}