bibthese

Bibliography in English

[AAB00] Aurore Annichini, Eugene Asarin, and Ahmed Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In Computer Aided Verification, pages 419-434, 2000. [ bib ]

[ACH⁺95] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science B, 138:3-34, January 1995. [ bib ]

[AD90] R. Alur and D. Dill. Automata for modeling real-time systems. In ICALP'90, 1990. [ bib ]

[AMP95] Eugene Asarin, Oded Maler, and Amir Pnueli. Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science, 138(1):35-65, 1995. [ bib | .html ]

[AMS06] Karine Altisen, Florence Maraninchi, and David Stauch. Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework. Science of Computer Programming, Special Issue on Foundations of Aspect-Oriented Programming, 63(3):297-320, 2006. [ bib ]

[ANA] ANALYSER. http://pop-art.inrialpes.fr/people/bjeannet/analyzer/index.html. [ bib ]

[ARG] ARGOS. http://www-verimag.imag.fr/~stauch/ArgosCompiler/introduction.html. [ bib ]

[ASP] ASPIC. http://www-verimag.imag.fr/~gonnord/aspic/aspic.html. [ bib ]

[Bar05] Sébastien Bardin. Vers un model checking avec accélération plate de systèmes hétérogènes. Phd thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005. [ bib | .pdf ]

[BB03] Constantinos Bartzis and Tevfik Bultan. Efficient symbolic representations for arithmetic constraints in verification. In International Journal of Foundations of Computer Science (IJFCS), special issue on Verification and Analysis of Infinite State Systems, volume 14.4, pages 605-624, August 2003. [ bib ]

[BBH⁺06] Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tomáš Vojnar. Programs with lists are counter automata. In Thomas Ball and Robert B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 517-531, Seattle, Washington, USA, August 2006. Springer. [ bib | DOI | .pdf ]

[BCALS06] A. Bouajjani, A. Collomb-Annichini, Y. Lakhnech, and M. Sighireanu. Analysing fair parametric extended automata. In ICALP (2), pages 577-588, 2006. [ bib ]

[BCC⁺03] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI 2003, ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, pages 196-207, San Diego (Ca.), June 2003. [ bib ]

[BFL04] Sébastien Bardin, Alain Finkel, and Jérôme Leroux. FASTer acceleration of counter automata in practice. In Kurt Jensen and Andreas Podelski, editors, Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 576-590, Barcelona, Spain, March 2004. Springer. [ bib | .ps ]

[BFLP03] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: Fast acceleration of symbolic transition systems. In CAV'03, pages 118-121, Boulder (Colorado), July 2003. LNCS 2725, Springer-Verlag. [ bib ]

[BFLS05] Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Philippe Schnoebelen. Flat acceleration in symbolic model checking. In Doron A. Peled and Yih-Kuen Tsay, editors, Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 474-488, Taipei, Taiwan, ROC, October 2005. Springer. [ bib | .pdf ]

[BHRZ03] R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337-354, San Diego, California, USA, 2003. Springer-Verlag, Berlin. [ bib | .pdf ]

[BIL06] Marius Bozga, Radu Iosif, and Yassine Lakhnech. Flat parametric counter automata. In ICALP (2), pages 577-588, 2006. [ bib ]

[BJH03] B. Boigelot, S. Jodogne, and F. Herbreteau. Hybrid acceleration using real vector automata. In Proc. of the 15th International Conference on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 193-205, Boulder (CO, USA), July 2003. Springer-Verlag. [ bib | .html ]

[BLW03] Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large. In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 223-235, Boulder, July 2003. Springer-Verlag. [ bib ]

[Boi99] B. Boigelot. Symbolic methods for exploring infinite state spaces. Phd thesis, University of Liège, 1999. [ bib ]

[Bou92] F. Bourdoncle. Sémantique des langages impératifs d'ordre supérieur et interprétation abstraite. Phd thesis, Ecole Polytechnique, Paris, 1992. [ bib ]

[Bou93] F. Bourdoncle. Efficient chaotic iteration strategies with widenings. Lecture Notes in Computer Science, 735:128-??, 1993. [ bib | .html ]

[BW94] B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In CAV'94, Stanford (Ca.), 1994. LNCS 818, Springer Verlag. [ bib ]

[BW02] Bernard Boigelot and Pierre Wolper. Representing arithmetic constraints with finite automata: An overview. In Proc. International Conference on Logic Programming (ICLP), volume 2401 of Lecture Notes in Computer Science, pages 1-19, Copenhagen, July 2002. Springer-Verlag. [ bib ]

[CC76] P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd Int. Symp. on Programming. Dunod, Paris, 1976. [ bib ]

[CC77] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, POPL'77, Los Angeles, January 1977. [ bib ]

[CC92a] P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(1-4):103-179, 1992. (Also, Research report LIX/RR/92/08, Ecole Polytechnique). [ bib ]

[CC92b] P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP'92,, Leuven, Belgium, 13-17 August 1992, Lecture Notes in Computer Science 631, pages 269-295. Springer-Verlag, Berlin, Germany, 1992. [ bib ]

[CC04] R. C. Clarisó and J. Cortadella. Verification of parametric timed circuits using octahedra. In Designing correct circuits, DCC'04, Barcelona, March 2004. [ bib ]

[CF99] Agostino Cortesi and Gilberto Filé, editors. Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22-24, 1999, Proceedings, volume 1694 of Lecture Notes in Computer Science. Springer, 1999. [ bib ]

[CGL94] E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM TOPLAS, 16(5):1512-1542, 1994. [ bib ]

[CH78] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978. [ bib ]

[CHR91a] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269-276, 1991. [ bib ]

[CHR91b] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5), 1991. [ bib ]

[CJ98] H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV'98, Vancouver (B.C.), 1998. LNCS 1427, Springer Verlag. [ bib ]

[CJ99] Hubert Comon and Yan Jurski. Timed automata and the theory of real numbers. In Proc. Conf. on Concurrency theory, volume 1664 of lncs, pages 242-257, Eindhoven, 1999. Springer Verlag. [ bib | .ps ]

[CMMC07] Jérôme Cornet, Florence Maraninchi, and Laurent Maillet-Contox. Formalizing systemc transaction-level models of systems-on-chip : a component-based approach. Submitted ???, 2007. [ bib ]

[CSE⁺05] A. Costan, S.Gaubert, E.Goubault, M.Martel, and S.Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. In Proc. of the 17th International Conference on Computer Aided Verification. Springer-Verlag, 2005. [ bib ]

[DFV05] Christophe Darlot, Alain Finkel, and Laurent Van Begin. About Fast and TReX accelerations. In Michael R. A. Huth, editor, Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87-103, London, UK, May 2005. Elsevier Science Publishers. [ bib | .pdf ]

[DG03] L. Danthony-Gonnord. Du calcul des durées aux automates symboliques. Master thesis, University of Paris VI/VII, June 2003. www-verimag.imag.fr/~gonnord/papers/rapport_dea.ps. [ bib ]

[FAS] FAST. http://www.lsv.ens-cachan.fr/fast/. [ bib ]

[FL02] A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Proceedings of the 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FSTTCS'2002), volume 2556 of Lecture Notes in Computer Science, pages 145-156, Kanpur, India, December 2002. Springer. [ bib ]

[FO97] Laurent Fribourg and Hans Olsén. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97), volume 1243 of Lecture Notes in Computer Science, pages 213-227, Warsaw, Poland, July 1997. Springer. [ bib | .ps ]

[FS00a] A. Finkel and G. Sutre. An algorithm constructing the semilinear post* for 2-dim reset/transfer vass. In 25th Int. Symp. Math. Found. Comp. Sci. (MFCS'2000), Bratislava, Slovakia, August 2000. LNCS 1893, Springer Verlag. [ bib ]

[FS00b] Alain Finkel and Grégoire Sutre. An algorithm constructing the semilinear Post* for 2-dim ResetashTransfer VASS. In Mogens Nielsen and Branislav Rovan, editors, Proceedings of the 25th International Symposium on Mathematical Fundations of Computer Science (MFCS 2000), volume 1893 of Lecture Notes in Computer Science, pages 353-362, Bratislava, Slovakia, August 2000. Springer. [ bib | .ps ]

[GGTZ07] S. Gaubert, E. Goubault, A. Taly, and S. Zennou. Static analysis by policy iteration on relational domains. In European Symposium On Programming, Braga (Portugal), April 2007. Springer Verlag. [ bib ]

[GH06] L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS'06, Seoul, Korea, August 2006. [ bib ]

[GHR04] L. Gonnord, N. Halbwachs, and P. Raymond. From discrete duration calculus to symbolic automata. In 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04, Barcelona, Spain, March 2004. [ bib ]

[GL93] S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In Fifth Conference on Computer-Aided Verification, CAV'93, Elounda (Greece), July 1993. LNCS 697, Springer Verlag. [ bib ]

[Gou01] Eric Goubault. Static analyses of the precision of floating-point operations. In SAS, pages 234-259, 2001. [ bib ]

[GR06] D. Gopan and T. Reps. Lookahead widening. In CAV'06, Seattle, 2006. [ bib ]

[Gra91] Ph. Granger. Analyses sémantiques de congruence. Phd thesis, Ecole Polytechnique, July 1991. [ bib ]

[Hal79a] N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Thèse de troisième cycle, University of Grenoble, March 1979. [ bib ]

[Hal79b] N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Thèse de 3e cycle, University of Grenoble, March 1979. [ bib ]

[Hal93] N. Halbwachs. Delay analysis in synchronous programs. In Fifth Conference on Computer-Aided Verification, CAV'93, Elounda (Greece), July 1993. LNCS 697, Springer Verlag. [ bib ]

[HCRP91] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305-1320, September 1991. [ bib ]

[HHWT97] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110-122, 1997. [ bib ]

[HLR92] N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow programming language lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, pages 785-793, September 1992. [ bib ]

[HLR93] N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag. [ bib ]

[HNSY92] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In LICS'92, June 1992. [ bib ]

[HPR97] N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157-185, August 1997. [ bib ]

[HRR91] N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from data-flow programs. In Third International Symposium on Programming Language Implementation and Logic Programming, Passau (Germany), August 1991. LNCS 528, Springer Verlag. [ bib ]

[IJT91] F. Irigoin, P. Jouvelot, and R. Triolet. Semantical interprocedural parallelization: An overview of the PIPS project. In ACM Int. Conf. on Supercomputing, ICS'91, Köln, 1991. [ bib ]

[Iri05] F. Irigoin. Detecting affine loop invariants using modular static analysis. Technical Report A/367/CRI, Centre de Recherche en Informatique, Ecole des Mines de Paris, July 2005. [ bib ]

[Jea00] B. Jeannet. Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones. Phd thesis, Institut National Polytechnique, Grenoble, September 2000. [ bib ]

[Jur99] Yan Jurski. Expression de la relation binaire d'accessibilité pour les automates à compteurs plats et les automates temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 1999. [ bib | .ps ]

[Kar76] M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133-151, 1976. [ bib ]

[L2C] L2CA. http://www-verimag.imag.fr/~async/L2CA/l2ca.html. [ bib ]

[Lam77] L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, 1977. [ bib ]

[LAS] LASH. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/. [ bib ]

[Ler03] J. Leroux. Algorithmique de la vérification des systèmes à compteurs - approximation et accélération - implémentation dans l'outil Fast. Phd thesis, Ecole Normale Supérieure de Cachan, December 2003. [ bib ]

[Mer05] D. Merchat. Réduction du nombre de variables en analyse de relations linéaires. Phd thesis, University Joseph Fourier, Grenole, May 2005. [ bib ]

[Mil87] William Miller. The maximum order of an element of a finite symmetric group. Am. Math. Monthly, 94(6):497-506, 1987. [ bib | DOI ]

[Min01] A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310-319. IEEE CS Press, October 2001. [ bib ]

[MT53] Thompson Motzkin, Raiffa and Thrall. The double description method. Theodore S. Motzkin: Selected Papers, 1953. [ bib ]

[New] NewPolka. http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html. [ bib ]

[Ope05] Open SystemC Initiative. IEEE 1666: SystemC Language Reference Manual, 2005. www.systemc.org. [ bib ]

[Pan01] P.K. Pandya. Specifying and deciding quantified discrete-time duration calculus formulae using dcvalid. In Real-Time Tools, RTTOOLS'2001, Aalborg, August 2001. [ bib ]

[PS87] J. A. Plaice and J-B. Saint. The lustre-esterel portable format. Unpublished report, INRIA, Sophia Antipolis, 1987. [ bib ]

[SK06] Axel Simon and Andy King. Widening Polyhedra with Landmarks. In Fourth Asian Symposium on Programming Languages and Systems, volume 4279 of Lecture Notes in Computer Science, pages 166-182. Springer Verlag, November 2006. [ bib ]

[SMMM06] Ludovic Samper, Florence Maraninchi, Laurent Mounier, and Louis Mandel. GLONEMO: Global and accurate formal models for the analysis of ad-hoc sensor networks. In Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06), Nice, France, May 2006. [ bib ]

[SSG06] Ilya Shlyakhter Sriram Sankaranarayanan, Franjo Ivancic and Aarti Gupta. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS'2006. LNCS 4134, Springer Verlag, 2006. [ bib ]

[SSM04] Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS'2004, pages 53-68. LNCS 3148, Springer Verlag, 2004. [ bib ]

[StI] StInG. http://theory.stanford.edu/~srirams/Software/sting.html. [ bib ]

[SW04] Z. Su and D. Wagner. A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In TACAS'04, pages 280-295, Barcelona, 2004. [ bib ]

[Tar72] R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1:146-160, 1972. [ bib ]

[TRE] TREX. http://www.liafa.jussieu.fr/~sighira/trex/. [ bib ]

[WB98] P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In CAV'98, pages 88-97, Vancouver, June 1998. LNCS 1427, Springer-Verlag. [ bib ]

This file has been generated by bibtex2html 1.85.

[AAB00]	Aurore Annichini, Eugene Asarin, and Ahmed Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In Computer Aided Verification, pages 419-434, 2000. [ bib ]
[ACH⁺95]	R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science B, 138:3-34, January 1995. [ bib ]
[AD90]	R. Alur and D. Dill. Automata for modeling real-time systems. In ICALP'90, 1990. [ bib ]
[AMP95]	Eugene Asarin, Oded Maler, and Amir Pnueli. Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science, 138(1):35-65, 1995. [ bib \| .html ]
[AMS06]	Karine Altisen, Florence Maraninchi, and David Stauch. Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework. Science of Computer Programming, Special Issue on Foundations of Aspect-Oriented Programming, 63(3):297-320, 2006. [ bib ]
[ANA]	ANALYSER. http://pop-art.inrialpes.fr/people/bjeannet/analyzer/index.html. [ bib ]
[ARG]	ARGOS. http://www-verimag.imag.fr/~stauch/ArgosCompiler/introduction.html. [ bib ]
[ASP]	ASPIC. http://www-verimag.imag.fr/~gonnord/aspic/aspic.html. [ bib ]
[Bar05]	Sébastien Bardin. Vers un model checking avec accélération plate de systèmes hétérogènes. Phd thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005. [ bib \| .pdf ]
[BB03]	Constantinos Bartzis and Tevfik Bultan. Efficient symbolic representations for arithmetic constraints in verification. In International Journal of Foundations of Computer Science (IJFCS), special issue on Verification and Analysis of Infinite State Systems, volume 14.4, pages 605-624, August 2003. [ bib ]
[BBH⁺06]	Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tomáš Vojnar. Programs with lists are counter automata. In Thomas Ball and Robert B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 517-531, Seattle, Washington, USA, August 2006. Springer. [ bib \| DOI \| .pdf ]
[BCALS06]	A. Bouajjani, A. Collomb-Annichini, Y. Lakhnech, and M. Sighireanu. Analysing fair parametric extended automata. In ICALP (2), pages 577-588, 2006. [ bib ]
[BCC⁺03]	B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI 2003, ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, pages 196-207, San Diego (Ca.), June 2003. [ bib ]
[BFL04]	Sébastien Bardin, Alain Finkel, and Jérôme Leroux. FASTer acceleration of counter automata in practice. In Kurt Jensen and Andreas Podelski, editors, Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 576-590, Barcelona, Spain, March 2004. Springer. [ bib \| .ps ]
[BFLP03]	S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: Fast acceleration of symbolic transition systems. In CAV'03, pages 118-121, Boulder (Colorado), July 2003. LNCS 2725, Springer-Verlag. [ bib ]
[BFLS05]	Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Philippe Schnoebelen. Flat acceleration in symbolic model checking. In Doron A. Peled and Yih-Kuen Tsay, editors, Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 474-488, Taipei, Taiwan, ROC, October 2005. Springer. [ bib \| .pdf ]
[BHRZ03]	R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337-354, San Diego, California, USA, 2003. Springer-Verlag, Berlin. [ bib \| .pdf ]
[BIL06]	Marius Bozga, Radu Iosif, and Yassine Lakhnech. Flat parametric counter automata. In ICALP (2), pages 577-588, 2006. [ bib ]
[BJH03]	B. Boigelot, S. Jodogne, and F. Herbreteau. Hybrid acceleration using real vector automata. In Proc. of the 15th International Conference on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 193-205, Boulder (CO, USA), July 2003. Springer-Verlag. [ bib \| .html ]
[BLW03]	Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large. In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 223-235, Boulder, July 2003. Springer-Verlag. [ bib ]
[Boi99]	B. Boigelot. Symbolic methods for exploring infinite state spaces. Phd thesis, University of Liège, 1999. [ bib ]
[Bou92]	F. Bourdoncle. Sémantique des langages impératifs d'ordre supérieur et interprétation abstraite. Phd thesis, Ecole Polytechnique, Paris, 1992. [ bib ]
[Bou93]	F. Bourdoncle. Efficient chaotic iteration strategies with widenings. Lecture Notes in Computer Science, 735:128-??, 1993. [ bib \| .html ]
[BW94]	B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In CAV'94, Stanford (Ca.), 1994. LNCS 818, Springer Verlag. [ bib ]
[BW02]	Bernard Boigelot and Pierre Wolper. Representing arithmetic constraints with finite automata: An overview. In Proc. International Conference on Logic Programming (ICLP), volume 2401 of Lecture Notes in Computer Science, pages 1-19, Copenhagen, July 2002. Springer-Verlag. [ bib ]
[CC76]	P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd Int. Symp. on Programming. Dunod, Paris, 1976. [ bib ]
[CC77]	P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, POPL'77, Los Angeles, January 1977. [ bib ]
[CC92a]	P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(1-4):103-179, 1992. (Also, Research report LIX/RR/92/08, Ecole Polytechnique). [ bib ]
[CC92b]	P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP'92,, Leuven, Belgium, 13-17 August 1992, Lecture Notes in Computer Science 631, pages 269-295. Springer-Verlag, Berlin, Germany, 1992. [ bib ]
[CC04]	R. C. Clarisó and J. Cortadella. Verification of parametric timed circuits using octahedra. In Designing correct circuits, DCC'04, Barcelona, March 2004. [ bib ]
[CF99]	Agostino Cortesi and Gilberto Filé, editors. Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22-24, 1999, Proceedings, volume 1694 of Lecture Notes in Computer Science. Springer, 1999. [ bib ]
[CGL94]	E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM TOPLAS, 16(5):1512-1542, 1994. [ bib ]
[CH78]	P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978. [ bib ]
[CHR91a]	Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269-276, 1991. [ bib ]
[CHR91b]	Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5), 1991. [ bib ]
[CJ98]	H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV'98, Vancouver (B.C.), 1998. LNCS 1427, Springer Verlag. [ bib ]
[CJ99]	Hubert Comon and Yan Jurski. Timed automata and the theory of real numbers. In Proc. Conf. on Concurrency theory, volume 1664 of lncs, pages 242-257, Eindhoven, 1999. Springer Verlag. [ bib \| .ps ]
[CMMC07]	Jérôme Cornet, Florence Maraninchi, and Laurent Maillet-Contox. Formalizing systemc transaction-level models of systems-on-chip : a component-based approach. Submitted ???, 2007. [ bib ]
[CSE⁺05]	A. Costan, S.Gaubert, E.Goubault, M.Martel, and S.Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. In Proc. of the 17th International Conference on Computer Aided Verification. Springer-Verlag, 2005. [ bib ]
[DFV05]	Christophe Darlot, Alain Finkel, and Laurent Van Begin. About Fast and TReX accelerations. In Michael R. A. Huth, editor, Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87-103, London, UK, May 2005. Elsevier Science Publishers. [ bib \| .pdf ]
[DG03]	L. Danthony-Gonnord. Du calcul des durées aux automates symboliques. Master thesis, University of Paris VI/VII, June 2003. www-verimag.imag.fr/~gonnord/papers/rapport_dea.ps. [ bib ]
[FAS]	FAST. http://www.lsv.ens-cachan.fr/fast/. [ bib ]
[FL02]	A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Proceedings of the 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FSTTCS'2002), volume 2556 of Lecture Notes in Computer Science, pages 145-156, Kanpur, India, December 2002. Springer. [ bib ]
[FO97]	Laurent Fribourg and Hans Olsén. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97), volume 1243 of Lecture Notes in Computer Science, pages 213-227, Warsaw, Poland, July 1997. Springer. [ bib \| .ps ]
[FS00a]	A. Finkel and G. Sutre. An algorithm constructing the semilinear post* for 2-dim reset/transfer vass. In 25th Int. Symp. Math. Found. Comp. Sci. (MFCS'2000), Bratislava, Slovakia, August 2000. LNCS 1893, Springer Verlag. [ bib ]
[FS00b]	Alain Finkel and Grégoire Sutre. An algorithm constructing the semilinear Post* for 2-dim ResetashTransfer VASS. In Mogens Nielsen and Branislav Rovan, editors, Proceedings of the 25th International Symposium on Mathematical Fundations of Computer Science (MFCS 2000), volume 1893 of Lecture Notes in Computer Science, pages 353-362, Bratislava, Slovakia, August 2000. Springer. [ bib \| .ps ]
[GGTZ07]	S. Gaubert, E. Goubault, A. Taly, and S. Zennou. Static analysis by policy iteration on relational domains. In European Symposium On Programming, Braga (Portugal), April 2007. Springer Verlag. [ bib ]
[GH06]	L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS'06, Seoul, Korea, August 2006. [ bib ]
[GHR04]	L. Gonnord, N. Halbwachs, and P. Raymond. From discrete duration calculus to symbolic automata. In 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04, Barcelona, Spain, March 2004. [ bib ]
[GL93]	S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In Fifth Conference on Computer-Aided Verification, CAV'93, Elounda (Greece), July 1993. LNCS 697, Springer Verlag. [ bib ]
[Gou01]	Eric Goubault. Static analyses of the precision of floating-point operations. In SAS, pages 234-259, 2001. [ bib ]
[GR06]	D. Gopan and T. Reps. Lookahead widening. In CAV'06, Seattle, 2006. [ bib ]
[Gra91]	Ph. Granger. Analyses sémantiques de congruence. Phd thesis, Ecole Polytechnique, July 1991. [ bib ]
[Hal79a]	N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Thèse de troisième cycle, University of Grenoble, March 1979. [ bib ]
[Hal79b]	N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Thèse de 3e cycle, University of Grenoble, March 1979. [ bib ]
[Hal93]	N. Halbwachs. Delay analysis in synchronous programs. In Fifth Conference on Computer-Aided Verification, CAV'93, Elounda (Greece), July 1993. LNCS 697, Springer Verlag. [ bib ]
[HCRP91]	N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305-1320, September 1991. [ bib ]
[HHWT97]	T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110-122, 1997. [ bib ]
[HLR92]	N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow programming language lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, pages 785-793, September 1992. [ bib ]
[HLR93]	N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag. [ bib ]
[HNSY92]	T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In LICS'92, June 1992. [ bib ]
[HPR97]	N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157-185, August 1997. [ bib ]
[HRR91]	N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from data-flow programs. In Third International Symposium on Programming Language Implementation and Logic Programming, Passau (Germany), August 1991. LNCS 528, Springer Verlag. [ bib ]
[IJT91]	F. Irigoin, P. Jouvelot, and R. Triolet. Semantical interprocedural parallelization: An overview of the PIPS project. In ACM Int. Conf. on Supercomputing, ICS'91, Köln, 1991. [ bib ]
[Iri05]	F. Irigoin. Detecting affine loop invariants using modular static analysis. Technical Report A/367/CRI, Centre de Recherche en Informatique, Ecole des Mines de Paris, July 2005. [ bib ]
[Jea00]	B. Jeannet. Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones. Phd thesis, Institut National Polytechnique, Grenoble, September 2000. [ bib ]
[Jur99]	Yan Jurski. Expression de la relation binaire d'accessibilité pour les automates à compteurs plats et les automates temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 1999. [ bib \| .ps ]
[Kar76]	M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133-151, 1976. [ bib ]
[L2C]	L2CA. http://www-verimag.imag.fr/~async/L2CA/l2ca.html. [ bib ]
[Lam77]	L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, 1977. [ bib ]
[LAS]	LASH. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/. [ bib ]
[Ler03]	J. Leroux. Algorithmique de la vérification des systèmes à compteurs - approximation et accélération - implémentation dans l'outil Fast. Phd thesis, Ecole Normale Supérieure de Cachan, December 2003. [ bib ]
[Mer05]	D. Merchat. Réduction du nombre de variables en analyse de relations linéaires. Phd thesis, University Joseph Fourier, Grenole, May 2005. [ bib ]
[Mil87]	William Miller. The maximum order of an element of a finite symmetric group. Am. Math. Monthly, 94(6):497-506, 1987. [ bib \| DOI ]
[Min01]	A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310-319. IEEE CS Press, October 2001. [ bib ]
[MT53]	Thompson Motzkin, Raiffa and Thrall. The double description method. Theodore S. Motzkin: Selected Papers, 1953. [ bib ]
[New]	NewPolka. http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html. [ bib ]
[Ope05]	Open SystemC Initiative. IEEE 1666: SystemC Language Reference Manual, 2005. `www.systemc.org`. [ bib ]
[Pan01]	P.K. Pandya. Specifying and deciding quantified discrete-time duration calculus formulae using dcvalid. In Real-Time Tools, RTTOOLS'2001, Aalborg, August 2001. [ bib ]
[PS87]	J. A. Plaice and J-B. Saint. The lustre-esterel portable format. Unpublished report, INRIA, Sophia Antipolis, 1987. [ bib ]
[SK06]	Axel Simon and Andy King. Widening Polyhedra with Landmarks. In Fourth Asian Symposium on Programming Languages and Systems, volume 4279 of Lecture Notes in Computer Science, pages 166-182. Springer Verlag, November 2006. [ bib ]
[SMMM06]	Ludovic Samper, Florence Maraninchi, Laurent Mounier, and Louis Mandel. GLONEMO: Global and accurate formal models for the analysis of ad-hoc sensor networks. In Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06), Nice, France, May 2006. [ bib ]
[SSG06]	Ilya Shlyakhter Sriram Sankaranarayanan, Franjo Ivancic and Aarti Gupta. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS'2006. LNCS 4134, Springer Verlag, 2006. [ bib ]
[SSM04]	Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS'2004, pages 53-68. LNCS 3148, Springer Verlag, 2004. [ bib ]
[StI]	StInG. http://theory.stanford.edu/~srirams/Software/sting.html. [ bib ]
[SW04]	Z. Su and D. Wagner. A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In TACAS'04, pages 280-295, Barcelona, 2004. [ bib ]
[Tar72]	R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1:146-160, 1972. [ bib ]
[TRE]	TREX. http://www.liafa.jussieu.fr/~sighira/trex/. [ bib ]
[WB98]	P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In CAV'98, pages 88-97, Vancouver, June 1998. LNCS 1427, Springer-Verlag. [ bib ]