{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:37Z","timestamp":1760202517709},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Since the seminal work of Cousot and Halbwachs, the domain of convex polyhedra has been employed in several systems for the analysis and verification of hardware and software components. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a higher dimensional vector space and reuse the tools and techniques already available for closed polyhedra. In this work we highlight and discuss the issues underlying such an embedding for those implementations that are based on the\n            <jats:italic>double description<\/jats:italic>\n            method, where a polyhedron may be described by a system of linear constraints or by a system of generating rays and points. Two major achievements are the definition of a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.\n          <\/jats:p>","DOI":"10.1007\/s00165-005-0061-1","type":"journal-article","created":{"date-parts":[[2005,6,18]],"date-time":"2005-06-18T05:36:01Z","timestamp":1119072961000},"page":"222-257","source":"Crossref","is-referenced-by-count":31,"title":["Not necessarily closed convex polyhedra and the double description method"],"prefix":"10.1145","volume":"17","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[{"name":"Department of Mathematics, University of Parma, Italy"}]},{"given":"Patricia M.","family":"Hill","sequence":"additional","affiliation":[{"name":"School of Computing, University of Leeds, UK"}]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[{"name":"Department of Mathematics, University of Parma, Italy"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Cousot R, (ed), Static analysis: Proceedings of the 10th international symposium, vol 2694 of Lecture Notes in Computer Science","author":"Bagnara R","year":"2003"},{"key":"p_2","volume-title":"Precise widening operators for convex polyhedra. Sci Comput Programming, (To appear)","author":"Bagnara R","year":"2005"},{"key":"p_3","first-page":"161","volume-title":"Proceedings of the 3rd workshop on automated verification of critical systems, Southampton. Published as TR Number DSSE-TR-2003-2","author":"Bagnara R","year":"2003"},{"key":"p_4","volume-title":"The parma polyhedra library user's manual. Department of Mathematics","author":"Bagnara R","year":"2004"},{"key":"p_5","series-title":"Colloquium Publications 3rd edn","volume-title":"Lattice Theory","author":"Bir G","year":"1967"},{"key":"p_6","first-page":"51","volume-title":"Cortesi A, Fil\u00e9 G, (eds)., Static analysis: Proceedings of the 6th international symposium, vol 1694 of Lecture Notes in Computer Science, Venice","author":"Besson F","year":"1999"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/3-540-62718-9_12","volume-title":"Gallagher JP, (ed), Logic program synthesis and transformation: proceedings of the 6th international workshop, vol 1207 of Lecture Notes in Computer Science","author":"Benoy F","year":"1997"},{"key":"p_8","first-page":"213","volume-title":"Hermenegildo MV, Puebla G, (eds), Static analysis: proceedings of the 9th international symposium, vol 2477 of Lecture Notes in Computer Science","author":"Bagnara R","year":"2002"},{"key":"p_9","volume-title":"Dipartimento di Matematica, Universit\u00e0 di Parma, Italy, . See also [BRZH02c].","author":"Bagnara R","year":"2002"},{"key":"p_10","volume-title":"Errata for technical report \"Quaderno 286\".","author":"Bagnara R","year":"2002"},{"key":"p_11","first-page":"238","volume-title":"Proceedings of the 4th annual ACM symposium on principles of programming languages, ACM Press, New York","author":"Cousot P","year":"1977"},{"key":"p_12","first-page":"84","volume-title":"Conference record of the 5th annual ACM symposium on principles of programming languages, ACM Press","author":"Cousot P","year":"1978"},{"issue":"4","key":"p_13","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0041-5553(64)90009-6","article-title":"Algorithm for finding a general formula for the non-negative solutions of system of linear equations","volume":"4","author":"Che NV","year":"1964","journal-title":"USSR Comput Math Math Phys"},{"issue":"2","key":"p_14","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1016\/0041-5553(65)90045-5","article-title":"Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities","volume":"5","author":"Che NV","year":"1965","journal-title":"USSR Comput Math Math Phys"},{"issue":"6","key":"p_15","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","article-title":"Algorithm for discovering the set of all solutions of a linear programming problem","volume":"8","author":"Che NV","year":"1968","journal-title":"USSR Comput Math Math Phys"},{"key":"p_16","series-title":"Lecture Notes in Computer Science","volume-title":"SAS","author":"Cou P","year":"2001"},{"key":"p_17","first-page":"67","volume-title":"7th international conference, TACAS 2001","author":"Col\u00f3n MA","year":"2001"},{"key":"p_18","first-page":"194","volume-title":"Cousot [Cou01]","author":"Dor N"},{"issue":"1","key":"p_19","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF01407931","article-title":"Dataflow analysis of scalar and array references","volume":"20","author":"Fea P","year":"1991","journal-title":"Int J Parallel Programming"},{"key":"p_20","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification: Proceedings of the 5th International Conference","volume":"697","author":"Hal N","year":"1993"},{"key":"p_21","first-page":"252","volume-title":"Antsaklis PJ, Kohn W, Nerode A, Sastry S, (eds), Hybrid systems II, vol 999 of Lecture Notes in Computer Science","author":"Henzinger TA","year":"1995"},{"key":"p_22","volume-title":"HyTech: a model checker for hybrid systems. Softw Tools Technol Transfer, 1(1+2):110-122","author":"Henzinger TA","year":"1997"},{"key":"p_23","volume-title":"Polyhedra integrated environment","author":"Halbwachs N","year":"1995"},{"key":"p_24","first-page":"223","volume-title":"Le Charlier B, (ed), Static analysis: proceedings of the 1st international symposium, vol 864 of Lecture Notes in Computer Science","author":"Halbwachs N","year":"1994"},{"issue":"2","key":"p_25","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","article-title":"Verification of real-time systems using linear relation analysis","volume":"11","author":"Halbwachs N","year":"1997","journal-title":"Formal Methods Sys Des"},{"key":"p_26","volume-title":"Documentation of the \"New Polka","author":"Jea B","year":"2002"},{"key":"p_27","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF01204720","article-title":"Lattice translates of a polytope and the Frobenius problem","volume":"12","author":"Kan R","year":"1992","journal-title":"Combinatorica"},{"key":"p_28","volume-title":"IRISA","author":"Le","year":"1992"},{"key":"p_29","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-7091-6355-9_13","volume-title":"Berghammer R, Lakhnech Y, (eds), Tool support for system specification, development and verification, advances in computing sciences","author":"Manna Z","year":"1999"},{"key":"p_30","first-page":"51","volume-title":"Kuhn HW, Tucker AW, (eds), Contributions to the Theory of Games - Vol II, no 28 in Annals of Mathematics Studies","author":"Motzkin TS","year":"1953"},{"issue":"8","key":"p_31","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","article-title":"A practical algorithm for exact array dependence analysis","volume":"35","author":"Pug W","year":"1992","journal-title":"Commun ACM"},{"key":"p_32","volume-title":"Theory of linear and integer programming","author":"Sch A","year":"1999"},{"key":"p_33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-46216-0","volume-title":"Convexity and Optimization in Finite Dimensions I","author":"Stoer J","year":"1970"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0061-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0061-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0061-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:50:52Z","timestamp":1641484252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0061-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1007\/s00165-005-0061-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0061-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}