{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T03:07:36Z","timestamp":1762916856368,"version":"3.43.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1023\/a:1024480913162","type":"journal-article","created":{"date-parts":[[2003,9,15]],"date-time":"2003-09-15T13:22:37Z","timestamp":1063632157000},"page":"5-37","source":"Crossref","is-referenced-by-count":57,"title":["Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems"],"prefix":"10.1007","volume":"23","author":[{"given":"B.","family":"Jeannet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5127648_CR1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Bouajjani, and B. Jonsson, \u201cOn-the-fly analysis of systems with unbounded, lossy fifo channels,\u201d in Computer Aided Verification, CAV'98, Vol. 1427 of LNCS, July 1998.","DOI":"10.1007\/BFb0028754"},{"key":"5127648_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, \u201cMinimization of timed transition systems,\u201d in Proceedings of the Third Conference on Concurrency Theory CONCUR'92, Lecture Notes in Computer Science 630, Springer-Verlag, 1992, pp. 340\u2013354.","DOI":"10.1007\/BFb0084802"},{"key":"5127648_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, \u201cThe algorithmic analysis of hybrid systems,\u201d Theoretical Computer Science B, Vol. 138, pp. 3\u201334, 1995.","journal-title":"Theoretical Computer Science B"},{"key":"5127648_CR4","doi-asserted-by":"crossref","unstructured":"G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and W. Yi, \u201cEfficient timed reachability analysis using clock difference diagrams,\u201d in Computer Aided Verification, CAV'99, Vol. 1633 of LNCS, July 1999.","DOI":"10.1007\/3-540-48683-6_30"},{"key":"5127648_CR5","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre, \u201cComputing abstractions of infinite state systems compositionally and automatically,\u201d in Computer Aided Verification, CAV'98, Vol. 1427 of LNCS, July 1998.","DOI":"10.1007\/BFb0028755"},{"key":"5127648_CR6","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Sadi, \u201cPowerful techniques for the automatic generation of invariants,\u201d in Computer Aided Verification, CAV'96, Vol. 1102 of LNCS, July 1996.","DOI":"10.1007\/3-540-61474-5_80"},{"key":"5127648_CR7","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, A. Browne, and Z. Manna, \u201cAutomatic generation of invariants and intermediate assertions,\u201d Theoretical Computer Science, Vol. 173, No. 1, 1997.","DOI":"10.1016\/S0304-3975(96)00191-0"},{"key":"5127648_CR8","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Godefroid, \u201cSymbolic verification of communication protocols with infinite state spaces using QDDs,\u201d in Computer Aided Verification, CAV'96, Vol. 1102 of LNCS, July 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"key":"5127648_CR9","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel, \u201cMinimal state graph generation,\u201d Science of Computer Programming, Vol. 18, pp. 247\u2013269, 1992.","journal-title":"Science of Computer Programming"},{"key":"5127648_CR10","doi-asserted-by":"crossref","unstructured":"A. Bouali and R. de Simone, \u201cSymbolic bisimulation minimisation,\u201d in Computer Aided Verification, CAV'92, Vol. 663 of LNCS, July 1992.","DOI":"10.1007\/3-540-56496-9_9"},{"key":"5127648_CR11","doi-asserted-by":"crossref","unstructured":"F. Bourdoncle, \u201cAbstract interpretation by dynamic partitionning,\u201d Journal of Functional Programming, Vol. 2, No. 4, 1992.","DOI":"10.1017\/S0956796800000496"},{"key":"5127648_CR12","unstructured":"F. Bourdoncle, \u201cEfficient chaotic iteration strategies with widenings,\u201d in International Conference on Formal Methods in Programming and their Applications, Vol. 735 of LNCS, 1993."},{"key":"5127648_CR13","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, \u201cCounterexample-guided abstraction refinement,\u201d in Computer Aided Verification, CAV'2000, Vol. 1855 of LNCS, July 2000.","DOI":"10.1007\/10722167_15"},{"key":"5127648_CR14","doi-asserted-by":"crossref","unstructured":"M.A. Col\u00f3n and T.E. Uribe, \u201cGenerating finite-state abstractions of reactive systems using decision procedures,\u201d in Computer Aided Verification, CAV'98, Vol. 1427 of LNCS, July 1998.","DOI":"10.1007\/BFb0028753"},{"key":"5127648_CR15","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \u201cVerification of synchronous sequential machines based on symbolic execution,\u201d in International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"5127648_CR16","unstructured":"P. Cousot, \u201cAsynchronous iterative methods for solving a fixpoint system of monotone equations,\u201d Technical Report IMAG-RR-88, Universit scientifique et mdicale de Grenoble, 1977."},{"key":"5127648_CR17","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cStatic determination of dynamic properties of programs,\u201d in 2nd Int. Symp. on Programming. Dunod, Paris, 1976.","DOI":"10.1145\/390018.808314"},{"key":"5127648_CR18","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cAbstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,\u201d in 4thACMSymposium on Principles of Programming Languages, POPL'77, Los Angeles, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"5127648_CR19","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cSystematic design of program analysis frameworks,\u201d in 6th ACM Symposium on Principles of Programming Languages, POPL'79, San Antonio, January 1979.","DOI":"10.1145\/567752.567778"},{"key":"5127648_CR20","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cAbstract interpretation frameworks,\u201d Journal of Logic and Computation, 1992.","DOI":"10.1093\/logcom\/2.4.511"},{"key":"5127648_CR21","unstructured":"P. Cousot and R. Cousot, \u201cComparing the Galois connection and widening\/narrowing approaches to abstract interpretation,\u201d in M. Bruynooghe and M. Wirsing (eds.), PLILP'92, Leuven (Belgium), LNCS 631, Springer Verlag, January 1992."},{"key":"5127648_CR22","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs, \u201cAutomatic discovery of linear restraints among variables of a program,\u201d in 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978.","DOI":"10.1145\/512760.512770"},{"key":"5127648_CR23","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine, \u201cThe tool KRONOS,\u201d In Hybrid Systems III, Verification and Control, Vol. 1066 of LNCS, 1996.","DOI":"10.1007\/BFb0020947"},{"key":"5127648_CR24","doi-asserted-by":"crossref","unstructured":"D. Dill and H. Wong-To, \u201cVerification of real-time systems by successive over and under approximations,\u201d in Seventh Conference on Computer-Aided Verification, CAV'95, Lige (Belgium), LNCS 939, Springer Verlag, July 1995.","DOI":"10.1007\/3-540-60045-0_66"},{"key":"5127648_CR25","unstructured":"L. Du Bousquet, \u201cTest fonctionnel statistique de syst\u00e8mes sp\u00e9cifi\u00e9s en LUSTRE,\u201d PhD thesis Universit\u00e9 Joseph Fourier, Grenoble, 1999."},{"key":"5127648_CR26","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi, \u201cConstruction of abstract state graphs with PVS,\u201d in Conference on Computer Aided Verification CAV'97, Haifa, Vol. 1254 of LNCS, June 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"5127648_CR27","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, \u201cAbout synchronous programming and abstract interpretation,\u201d Science of Computer Programming, Special Issue on SAS'94, Vol. 31, No. 1, May 1998.","DOI":"10.1016\/S0167-6423(96)00041-X"},{"issue":"9","key":"5127648_CR28","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, \u201cThe synchronous dataflow programming language LUSTRE,\u201d Proceedings of the IEEE, Vol. 79, No. 9, pp. 1305\u20131320, 1991.","journal-title":"Proceedings of the IEEE"},{"key":"5127648_CR29","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, and P. Raymond, \u201cSynchronous observers and the verification of reactive systems,\u201d in M. Nivat, C. Rattray, T. Rus, and G. Scollo (Eds.), Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, Workshops in Computing, Springer Verlag, June 1993.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"issue":"2","key":"5127648_CR30","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y.E. Proy, and P. Roumanoff, \u201cVerification of real-time systems using linear relation analysis,\u201d Formal Methods in System Design, Vol. 11, No. 2, pp. 157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"key":"5127648_CR31","unstructured":"T. Henzinger, P. Ho, and H. Wong-To, \u201cHyTech: The next generation,\u201d in RTSS'95, 1995."},{"key":"5127648_CR32","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In LICS'92, June 1992."},{"key":"5127648_CR33","unstructured":"B. Jeannet, \u201cThe convex polyhedra library NEW POLKA,\u201d http:\/\/www.irisa.fr\/prive\/bjeannet\/newpolka.html."},{"key":"5127648_CR34","doi-asserted-by":"crossref","unstructured":"B. Jeannet, N. Halbwachs, and P. Raymond, \u201cDynamic partitioning in analyses of numerical properties,\u201d in Static Analysis Symposium, SAS'99, Vol. 1694 of LNCS, Venezia (Italy), September 1999.","DOI":"10.1007\/3-540-48294-6_3"},{"key":"5127648_CR35","unstructured":"N.D. Jones, C. Gomard, and P. Sestoft, Partial Evaluation and Automatic Program Generation, Prentice Hall International, 1993."},{"key":"5127648_CR36","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"M. Karr, \u201cAffine relationships among variables of a program,\u201d Acta Informatica, Vol. 6, pp. 133\u2013151, 1976.","journal-title":"Acta Informatica"},{"key":"5127648_CR37","unstructured":"F. Larsson, K.G. Larsen, P. Pettersson, and W. Yi, \u201cEfficient verification of real-time systems: Compact data structures and state-space reduction,\u201d in Proc. of the 18th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, December 1997."},{"key":"5127648_CR38","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi, \u201cUPPAAL in a nutshell,\u201d Springer International Journal of Software Tools for Technology Transfer, Vol. 1, Nos. (1\/2), 1997.","DOI":"10.1007\/s100090050010"},{"issue":"9","key":"5127648_CR39","doi-asserted-by":"crossref","first-page":"1321","DOI":"10.1109\/5.97301","volume":"79","author":"P. LeGuernic","year":"1991","unstructured":"P. LeGuernic, T. Gautier, M. LeBorgne, and C. LeMaire, \u201cProgramming real time applications with SIGNAL,\u201d Proceedings of the IEEE, Vol. 79, No. 9, pp. 1321\u20131336, 1991.","journal-title":"Proceedings of the IEEE"},{"key":"5127648_CR40","unstructured":"C. Mauras, \u201cCalcul symbolique et automates interpr\u00e9t\u00e9s,\u201d Technical Report 10, IRCyN, November 1996."},{"key":"5127648_CR41","unstructured":"A. Min\u00e9, \u201cRepr\u00e9sentation d'ensembles de contraintes de somme ou de diff\u00e9rence de deux variables et application\u00e0 l'analyse automatique de programmes,\u201d Master's thesis, Laboratoire d'Informatique de l' \u00c8cole Normale Sup\u00e9rieure de Paris, July 2000."},{"key":"5127648_CR42","doi-asserted-by":"crossref","unstructured":"J. M\u00f8ller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard, \u201cDifference decision diagrams,\u201d in Computer Science Logic, The IT University of Copenhagen, Denmark, September 1999.","DOI":"10.1007\/3-540-48168-0_9"},{"key":"5127648_CR43","doi-asserted-by":"crossref","unstructured":"C. Ratel, N. Halbwachs, and P. Raymond, \u201cProgramming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE,\u201d in ACM-SIGSOFT'91 Conference on Software for Critical Systems, New Orleans, December 1991.","DOI":"10.1145\/125083.123062"},{"key":"5127648_CR44","unstructured":"P. Raymond, \u201cCompilation efficace d'un langage d\u00e9claratif synchrone: Le g\u00e9n\u00e9rateur de code LUSTRE-V3,\u201d PhD thesis, Institut National Polytechnique de Grenoble, November 1991."},{"key":"5127648_CR45","doi-asserted-by":"crossref","unstructured":"H. Sipma, T.E. Uribe, and Z. Manna, \u201cDeductive model checking,\u201d in 8th International Conference on Computer Aided Verification, CAV'96, Vol. 1102 of LNCS, July 1996.","DOI":"10.1007\/3-540-61474-5_70"},{"key":"5127648_CR46","unstructured":"F. Somenzi, \u201cCUDD: Colorado University decision diagram package,\u201d ftp:\/\/vlsi.colorado.edu\/pub."},{"key":"5127648_CR47","doi-asserted-by":"crossref","unstructured":"R.F.L. Spelberg, W.J. Toetenel, and M. Ammerlaan, \u201cPartition refinement in real-time model checking,\u201d in 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486, Springer Verlag, 1998, pp. 143\u2013157.","DOI":"10.1007\/BFb0055344"},{"key":"5127648_CR48","unstructured":"The Caml language. http:\/\/caml.inria.fr\/."},{"key":"5127648_CR49","doi-asserted-by":"crossref","unstructured":"M. Yanakakis and D. Lee, \u201cAn efficient algorithm for minimizing real-time transition systems,\u201d in Fifth Conference on Computer-Aided Verification, CAV'93, Elounda (Greece), LNCS 697, Springer Verlag, July 1993.","DOI":"10.1007\/3-540-56922-7_18"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024480913162.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1024480913162\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024480913162.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:13:02Z","timestamp":1754421182000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1024480913162"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["5127648"],"URL":"https:\/\/doi.org\/10.1023\/a:1024480913162","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}