{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:52Z","timestamp":1760202772928,"version":"3.37.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961446"},{"type":"electronic","value":"9783319961453"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_13","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"230-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Direct Encoding for NNC Polyhedra"],"prefix":"10.1007","author":[{"given":"Anna","family":"Becchi","sequence":"first","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"13_CR1","unstructured":"4ti2 team: 4ti2\u2014a software package for algebraic, geometric and combinatorial problems on linear spaces. \nwww.4ti2.de"},{"issue":"1","key":"13_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s12532-016-0104-z","volume":"9","author":"B Assarf","year":"2017","unstructured":"Assarf, B., Gawrilow, E., Herr, K., Joswig, M., Lorenz, B., Paffenholz, A., Rehn, T.: Computing convex hulls and counting integer points with polymake. Math. Program. Comput. 9(1), 1\u201338 (2017)","journal-title":"Math. Program. Comput."},{"issue":"2","key":"13_CR3","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/s00165-005-0061-1","volume":"17","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Form. Asp. Comput. 17(2), 222\u2013257 (2005)","journal-title":"Form. Asp. Comput."},{"issue":"46","key":"13_CR4","doi-asserted-by":"crossref","first-page":"4672","DOI":"10.1016\/j.tcs.2009.07.033","volume":"410","author":"R Bagnara","year":"2009","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410(46), 4672\u20134691 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213\u2013229. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45789-5_17"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Bastoul, C.: Code generation in the polyhedral model is easier than you think. In: Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques (PACT 2004), Antibes Juan-les-Pins, France, pp. 7\u201316. IEEE Computer Society (2004)","DOI":"10.1109\/PACT.2004.1342537"},{"key":"13_CR7","unstructured":"Becchi, A., Zaffanella, E.: A conversion procedure for NNC polyhedra. CoRR, abs\/1711.09593 (2017)"},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1016\/j.tcs.2012.10.042","volume":"493","author":"M Benerecetti","year":"2013","unstructured":"Benerecetti, M., Faella, M., Minopoli, S.: Automatic synthesis of switching controllers for linear hybrid systems: safety control. Theor. Comput. Sci. 493, 116\u2013138 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR9","unstructured":"Birkhoff, G.: Lattice Theory. 3rd edn. Volume XXV of Colloquium Publications. American Mathematical Society, Providence (1967)"},{"issue":"4","key":"13_CR10","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0041-5553(64)90009-6","volume":"4","author":"NV Chernikova","year":"1964","unstructured":"Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of system of linear equations. U.S.S.R. Comput. Math. Math. Phys. 4(4), 151\u2013158 (1964)","journal-title":"U.S.S.R. Comput. Math. Math. Phys."},{"issue":"2","key":"13_CR11","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1016\/0041-5553(65)90045-5","volume":"5","author":"NV Chernikova","year":"1965","unstructured":"Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Comput. Math. Math. Phys. 5(2), 228\u2013233 (1965)","journal-title":"U.S.S.R. Comput. Math. Math. Phys."},{"issue":"6","key":"13_CR12","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"NV Chernikova","year":"1968","unstructured":"Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Comput. Math. Math. Phys. 8(6), 282\u2013293 (1968)","journal-title":"U.S.S.R. Comput. Math. Math. Phys."},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45319-9_6"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, TX, USA, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/11596356_21","volume-title":"Embedded and Ubiquitous Computing \u2013 EUC 2005","author":"D Doose","year":"2005","unstructured":"Doose, D., Mammeri, Z.: Polyhedra-based approach for incremental validation of real-time systems. In: Yang, L.T., Amamiya, M., Liu, Z., Guo, M., Rammig, F.J. (eds.) EUC 2005. LNCS, vol. 3824, pp. 184\u2013193. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11596356_21"},{"key":"13_CR17","unstructured":"Ellenbogen, R.: Fully automatic verification of absence of errors via interprocedural integer analysis. Master\u2019s thesis, School of Computer Science, Tel-Aviv University, Tel-Aviv, Israel, December 2004"},{"issue":"3","key":"13_CR18","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008)","journal-title":"Softw. Tools Technol. Transf."},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science","author":"K Fukuda","year":"1996","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Euler, R., Manoussakis, I. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91\u2013111. Springer, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-61576-8_77"},{"key":"13_CR20","unstructured":"Genov, B.: The Convex Hull Problem in Practice: Improving the Running Time of the Double Description Method. Ph.D. thesis, University of Bremen, Germany (2014)"},{"key":"13_CR21","unstructured":"Gopan, D.: Numeric Program Analysis Techniques with Applications to Array Analysis and Library Summarization. Ph.D. thesis, University of Wisconsin, Madison, Wisconsin, USA, August 2007"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis","author":"N Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223\u2013237. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/3-540-58485-4_43"},{"issue":"2","key":"13_CR23","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Methods Syst. Des. 11(2), 157\u2013185 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR24","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"issue":"3","key":"13_CR26","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0925-7721(02)00103-7","volume":"23","author":"V Kaibel","year":"2002","unstructured":"Kaibel, V., Pfetsch, M.E.: Computing the face lattice of a polytope from its vertex-facet incidences. Comput. Geom. 23(3), 281\u2013290 (2002)","journal-title":"Comput. Geom."},{"key":"13_CR27","unstructured":"Loechner, V.: PolyLib: a library for manipulating parameterized polyhedra (1999). \nhttp:\/\/icps.u-strasbg.fr\/PolyLib\/"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Contributions to the Theory of Games - Volume II, number 28 in Annals of Mathematics Studies, pp. 51\u201373. Princeton University Press, Princeton (1953)","DOI":"10.1515\/9781400881970-004"},{"key":"13_CR29","unstructured":"Pop, S., Silber, G.-A., Cohen, A., Bastoul, C., Girbal, S., Vasilache, N.: GRAPHITE: Polyhedral analyses and optimizations for GCC. Technical Report A\/378\/CRI, Centre de Recherche en Informatique, \u00c9cole des Mines de Paris, Fontainebleau, France (2006)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, pp. 46\u201359 (2017)","DOI":"10.1145\/3009837.3009885"},{"issue":"19","key":"13_CR31","doi-asserted-by":"crossref","first-page":"2229","DOI":"10.1093\/bioinformatics\/btn401","volume":"24","author":"M Terzer","year":"2008","unstructured":"Terzer, M., Stelling, J.: Large-scale computation of elementary flux modes with bit pattern trees. Bioinformatics 24(19), 2229\u20132235 (2008)","journal-title":"Bioinformatics"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-14403-5_32","volume-title":"Parallel Processing and Applied Mathematics","author":"M Terzer","year":"2010","unstructured":"Terzer, M., Stelling, J.: Parallel extreme ray and pathway computation. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Wasniewski, J. (eds.) PPAM 2009. LNCS, vol. 6068, pp. 300\u2013309. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14403-5_32"},{"issue":"1","key":"13_CR33","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1134\/S0965542512010162","volume":"52","author":"NY Zolotykh","year":"2012","unstructured":"Zolotykh, N.Y.: New modification of the double description method for constructing the skeleton of a polyhedral cone. Comput. Math. Math. Phys. 52(1), 146\u2013156 (2012)","journal-title":"Comput. Math. Math. Phys."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:37:09Z","timestamp":1532111829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}