@INPROCEEDING{abadi89, AUTHOR = {M. Abadi and L. Lamport and P. Wolper}, TITLE = {Realizable and unrealizable specifications of reactive systems}, BOOKTITLE = {16th ICALP}, EDITOR={G. Ausiello and M. Dezani-Ciancaglini and S. Ronchi Della Rocca}, PUBLISHER = {LNCS 372, Springer Verlag}, PAGES={1--17}, MONTH = jul , YEAR = {1989} } @ARTICLE{ada, AUTHOR = {R. Jha and J.M. {Kamrad II} and D.T. Cornhill}, TITLE = {{\sc Ada} program partitioning language: A notation for distributing {\sc Ada} programs}, JOURNAL = {IEEE Transactions on Software Engineering}, VOLUME = {15}, NUMBER = {3}, MONTH = mar, YEAR = 1989 } @BOOK{ada:manual, AUTHOR = {ADA}, TITLE = {The Programming Language {\sc Ada} Reference Manual}, PUBLISHER = {LNCS 155, Springer Verlag}, YEAR = {1983} } @BOOK{ada95, AUTHOR={N. H. Cohen}, TITLE = {{\sc Ada} as a second langguage}, PUBLISHER = {McGraw-Hill Series in Computer Science}, YEAR= 1996 } @BOOK{aho86, AUTHOR = {A. Aho and R. Sethi and J. Ullman }, TITLE = {Compilers : Principles, Techniques and Tools}, PUBLISHER = {Addison-Wesley}, YEAR = {1986} } @book{ahu, author = {A. Aho and J. Hopcroft and J. Ullman} , title = {Design and analysis of computer Algorithms} , publisher = {Addison Wesley} , year = {1974} } @INPROCEEDINGS{model, AUTHOR = {J.P. Gray and I. Buchanan and P.S. Robertson}, TITLE = {Desining gate arrays using a silicon compiler}, BOOKTITLE = {19th Design Automation Conference}, NUMBER = {24.3}, PAGES = {377--383}, YEAR = {1984} } @ARTICLE{alur, AUTHOR = {R. Alur and T.A. Henzinger}, TITLE = {A really temporal logic}, JOURNAL = {JACM}, VOLUME=41, NUMBER=1, MONTH=jan, YEAR = 1994 } @TECHREPORT{alur91, AUTHOR={R. Alur}, TITLE={ Techniques for Automatic Verification of Real-Time Systems}, TYPE = {PhD Thesis}, INSTITUTION = {Stanford University}, MONTH=aug , YEAR= 1991 } @article{alur90, author = {R. Alur and C. Courcoubetis and D. L. Dill}, title = {Model-checking in dense real-time}, journal = {Information and Computation}, year = {1993}, volume = {104}, number = {1}, pages = {2-34}, note = {Preliminary version appears in the Proc. of 5th LICS, 1990} } @INPROCEEDINGS{dill89, AUTHOR={D. L. Dill}, TITLE={Timing assumptions and verification of finite state concurrent systems}, BOOKTITLE= {Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, MONTH = jun , YEAR = 1989 } @INPROCEEDINGS{ostroff89, AUTHOR={J. S. Ostroff}, TITLE={Automated verification of timed transition systems}, BOOKTITLE= {Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, MONTH = jun , YEAR = 1989 } @INPROCEEDINGS{alur90a, AUTHOR={R. Alur and D. Dill}, TITLE = {Automata for modeling real-time systems}, BOOKTITLE={ICALP'90}, YEAR=1990 } @BOOK{ashcroft85, AUTHOR = {E. A. Ashcroft and W. W. Wadge }, TITLE = {\lucid, the data-flow programming language} , PUBLISHER = {Academic Press}, YEAR = 1985 } @ARTICLE{meije1, AUTHOR = {D. Austry and G. Boudol }, TITLE = {Alg\`{e}bre de processus et synchronisation} , JOURNAL = {TCS}, VOLUME = 30, MONTH = apr, YEAR = 1984 } @INPROCEEDINGS{boudol85, AUTHOR={G. Boudol}, TITLE={Calculs de processus et v\'erification}, BOOKTITLE={Colloque C$^3$, Angoul\^eme}, YEAR= 1985 } @TECHREPORT{lts, AUTHOR = {S. A. Babiker and R. A. Fleming and R. E. Milne }, TITLE = {A tutorial for {\sc LTS}}, TYPE = {RR}, NUMBER = {225. 84. 1}, INSTITUTION = {Standard Telecommunication Laboratories}, YEAR = 1984 } @TECHREPORT{halbwach84, AUTHOR = {N. Halbwachs}, TITLE = { Mod\'{e}lisation et analyse du comportement des syst\`{e}mes informatiques temporis\'{e}s}, TYPE = {Th\`{e}se d'Etat}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH = jun, YEAR = 1984 } @TECHREPORT{halbwach79, AUTHOR = {N. Halbwachs}, TITLE = {D\'{e}termination automatique de relations lin\'{e}aires v\'{e}rifi\'{e}es par les variables d'un programme}, TYPE = {Th\`{e}se de troisi\`{e}me cycle}, INSTITUTION = {\Universityof\ Grenoble}, MONTH = mar, YEAR = 1979 } @TECHREPORT{halbwach76, AUTHOR = {N. Halbwachs}, TITLE = {Propositions pour un syst\`{e}me interactif d'aide \`{a} la prise de d\'{e}cisions}, TYPE = {\DEA}, INSTITUTION = {\Universityof\ Grenoble}, MONTH =jun, YEAR = 1976 } @TECHREPORT{caspi81, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE = {An approach to real-time systems modelling}, TYPE = {\techreport}, NUMBER = {253}, INSTITUTION = {IMAG, Grenoble}, ADRESS = {Grenoble}, MONTH = jun , YEAR = 1981 } @TECHREPORT{caspi82, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE = { Algebra of events, a model for parallel and real time systems}, TYPE = {\techreport}, NUMBER = {285}, INSTITUTION = {IMAG, Grenoble}, MONTH = jan , YEAR = 1982 } @TECHREPORT{atp, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE = { Conception certifi\'{e}e de syst\`{e}mes temporis\'{e}s, un exemple}, TYPE = {Rapport final de l'ATP ``Parall\'{e}lisme, Communication,Synchronisation''}, INSTITUTION = {CNRS}, MONTH = sep , YEAR = 1983 } @ARTICLE{amblard86, AUTHOR = {P. Amblard and P. Caspi and N. Halbwachs }, TITLE ={Describing and reasoning about circuits behaviour by means of time functions}, JOURNAL ={IEE Proceedings-E}, VOLUME ={133}, NUMBER = {5}, PAGES = {271--275}, MONTH = sep , YEAR = {1986 }, } @ARTICLE{caspi86, AUTHOR = {P. Caspi and N. Halbwachs}, TITLE ={Analyse approch\'{e}e du comportement asymptotique de syst\`{e}mes temporis\'{e}s}, JOURNAL = {Technique et Science Informatiques}, VOLUME = {5}, NUMBER = {2}, PAGES = {75--88}, YEAR = 1986 } @ARTICLE{caspi86a, AUTHOR = {P. Caspi and N. Halbwachs}, TITLE = {A functional model for describing and reasoning about time behaviour of computing systems}, JOURNAL = {Acta Informatica}, VOLUME = {22}, PAGES = {595--697}, YEAR = 1986 } @INPROCEEDINGS{caspi82a, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE={ Algebra of events, A model for parallel and real-time systems}, BOOKTITLE = {International Conference on Parallel Processing, Bellaire (Michigan)}, MONTH = aug, YEAR = 1982 } @INPROCEEDINGS{caspi82b, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE = {An approach to real-time systems modeling }, BOOKTITLE = {International Conference on Distributed Computing Systems, Miami}, MONTH =oct, YEAR = 1982 } @INPROCEEDINGS{bergerand85a, AUTHOR = { J-L. Bergerand and P. Caspi and N. Halbwachs }, TITLE = {Specification and formal validation of distributed systems, the real-time approach}, BOOKTITLE = {IEE Conference Control 85, Cambridge }, MONTH = jul, YEAR = 1985 } @INPROCEEDINGS{amblard85, AUTHOR = {P. Amblard and P. Caspi and N. Halbwachs }, TITLE = { Describing and reasoning about circuits behaviour by means of time functions}, BOOKTITLE = {1985 Conference on Computer Hardware Description Languages, Tokyo}, MONTH = aug, YEAR = 1985 } @INPROCEEDINGS{caspi87a, AUTHOR ={ P. Caspi and N. Halbwachs and D. Pilaud and J. Plaice }, TITLE = {Le langage \lustre\ et sa s\'{e}mantique op\'{e}rationnelle}, BOOKTITLE = {2e Colloque C\,$^3$, Angoul\^{e}me}, MONTH = may, YEAR = 1987 } @INPROCEEDINGS{caspi87b, AUTHOR = {P. Caspi and N. Halbwachs }, TITLE = { Suites de dates et compteurs d'occurrences d'\'{e}v\'{e}nements}, BOOKTITLE = { S\'{e}minaire ``Alg\`{e}bres Exotiques et Syst\`{e}mes \`{a} Ev\'{e}nements Discrets'', Issy-les-Moulineaux}, MONTH = jun, YEAR = 1987 } @TECHREPORT{mauras87, AUTHOR = {Ch. Mauras }, TITLE = { Impl\'{e}mentation de la s\'{e}mantique statique de \lustre\ en Mentor-Typol}, TYPE = {\DEA}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH = jun , YEAR = 1987 } @INPROCEEDINGS{bergerand85, AUTHOR = {J-L. Bergerand and P. Caspi and N. Halbwachs and D. Pilaud and E. Pilaud }, TITLE = {Outline of a real-time data-flow language}, BOOKTITLE = {1985 Real-Time Symposium, San Diego}, MONTH = dec , YEAR = 1985 } @INPROCEEDINGS{sococo, AUTHOR = {J-L. Bergerand and P. Caspi and N. Halbwachs and J. Plaice }, TITLE = {Automatic control systems programming using a real-time declarative language}, BOOKTITLE = {IFAC/IFIP Symp. 'SOCOCO 86, Graz}, MONTH = may , YEAR = 1986 } @TECHREPORT{these:bergerand, AUTHOR = {J-L. Bergerand}, TITLE = {\lustre: un langage d\'{e}claratif pour le temps r\'{e}el}, TYPE = {\Thesis}, INSTITUTION = {Institut National Polytechnique de Grenoble}, YEAR = 1986 } @TECHREPORT{bernhard89, AUTHOR = {R. Bernhard and G. Berry and F. Boussinot}, TITLE = {The {\sc occ} C generated code interface manual}, TYPE = {\techreport\ }, INSTITUTION = {Ecole Nationale Sup\'{e}rieure des Mines de Paris}, MONTH = dec , YEAR = 1989 } @TECHREPORT{esterel:montre, AUTHOR = {G. Berry}, TITLE = {Programming a digital watch in \esterel~V3\_2}, TYPE = {\techreport\ 08/91}, INSTITUTION = {Centre de Math\'ematiques Appliqu\'ees, Ecole des Mines de Paris, Sophia-Antipolis}, YEAR = 1991 } @ARTICLE{esterel:tsi, AUTHOR = {G. Berry and P. Couronn\'{e} and G. Gonthier}, TITLE = { Programmation synchrone des syst\`{e}mes r\'{e}actifs , le langage \esterel}, JOURNAL = {Technique et Science Informatique}, VOLUME = 4, PAGES = {305--316}, YEAR = 1987 } @INCOLLECTION{berry87, AUTHOR = {G. Berry and P. Couronn\'{e} and G. Gonthier }, TITLE = {Synchronous programming of reactive systems, an introduction to \esterel}, BOOKTITLE = {Programming of Future Generation Computers}, EDITOR = {K. Fuchi and M. Nivat}, PUBLISHER = {Elsevier Science Publisher B.V.\ (North Holland)}, YEAR = 1988, NOTE = {INRIA Report 647} } @ARTICLE{esterel:scp, TITLE = {The {Esterel} Synchronous Programming Language: Design, Semantics, Implementation}, AUTHOR = {G. Berry and G. Gonthier}, JOURNAL = {Science of Computer Programming}, VOLUME = 19, NUMBER=2, YEAR=1992, PAGES={87--152} } @ARTICLE{berry&sethi, AUTHOR = {G. Berry and R. Sethi }, TITLE = {From regular expressions to deterministic automata}, JOURNAL = {TCS}, VOLUME = 25, NUMBER = 1, YEAR = 1987 } @INPROCEEDINGS{berry89, AUTHOR = {G. Berry}, TITLE = {Real Time programming: Special purpose or general purpose languages}, BOOKTITLE = {IFIP World Computer Congress}, ADDRESS={San Francisco}, YEAR = 1989 } @INPROCEEDINGS{esterel:hard, AUTHOR = {G. Berry}, TITLE = {A Hardware Implementation of Pure \esterel}, BOOKTITLE = {{ACM} Workshop on Formal Methods in {VLSI} Design, Miami}, MONTH = jan , YEAR = 1991 } @article{esterel:hard1, AUTHOR = {G. Berry}, TITLE = {Esterel on Hardware}, journal = {Philosophical Transactions Royal Society of London}, serie={A}, volume={339}, year=1992, pages={217---248} } @INPROCEEDINGS{BerryCosserat:Esterel, TITLE = {The Synchronous Programming Language {Esterel} and its Mathematical Semantics}, AUTHOR = {G. Berry and L. Cosserat}, BOOKTITLE = {Seminar on Concurrency}, EDITOR = {LNCS 197, S. Brookes and G. Winskel}, PUBLISHER = {Springer Verlag}, PAGES = {389--448}, YEAR = {1984} } @INPROCEEDINGS{andre91, AUTHOR={C. Andr\'e and J.P. Marmorat and J.P. Paris}, TITLE={Execution machines for {Esterel}}, BOOKTITLE={1st European Control Conference, Grenoble}, MONTH=jul , YEAR= 1992 } @INPROCEEDINGS{lustre:ecc, AUTHOR={N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud}, TITLE={The synchronous data-flow programming language {Lustre} (extended abstract)}, BOOKTITLE={1st European Control Conference, Grenoble, France}, PAGES= {1661--1665}, MONTH=jul , YEAR= 1992 } @ARTICLE{esterel:ieee, AUTHOR={F. Boussinot and {R. de} Simone}, TITLE={The \esterel\ language}, JOURNAL={Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, PAGES={1293--1304}, MONTH=sep , YEAR={1991} } @ARTICLE{ps:ieee, KEY={IEEE}, AUTHOR={}, TITLE={Another look at real-time programming}, JOURNAL={Special Section of the Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, MONTH=sep , YEAR={1991} } @ARTICLE{benveniste91, AUTHOR={A. Benveniste and G. Berry}, TITLE={The Synchronous Approach to Reactive and Real-Time Systems}, JOURNAL={Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, PAGES={1270--1282}, MONTH=sep , YEAR={1991} } @TECHREPORT{sahara, AUTHOR={G. Gherardi}, TITLE={Sahara: un environnement de mise au point graphique pour les programmes {Esterel} (\inpreparation)}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} de Nice}, YEAR = {1992} } @TECHREPORT{couronne:these, AUTHOR={Ph. Couronn\'{e}}, TITLE={Le syst\`{e}me {\sc Esterel v2} }, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Paris VII}, MONTH=dec , YEAR = {1990} } @ARTICLE{lustre:ieee, AUTHOR={N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud}, TITLE={The synchronous dataflow programming language \lustre}, JOURNAL={Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, PAGES={1305-1320}, MONTH=sep , YEAR={1991} } @Article{CGP99, author = {P. Caspi and A. Girault and D. Pilaud}, title = {Automatic Distribution of Reactive Systems for Asynchronous Networks of Processors}, journal = {IEEE Transactions on Software Engineering}, year = {1999}, volume = {25}, number = {3}, pages = {416--427}, note = {Research report INRIA 3491} } @InProceedings{caspi:safecomp99, author = {P. Caspi and C. Mazuet and R. Salem and D. Weber}, title = {Formal Design of Distributed Control Systems with {L}ustre}, booktitle = {Proc. Safecomp'99}, volume = {1698}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag}, year = 1999, month = {September} } @INCOLLECTION{pam, AUTHOR = { P. Bertin and D. Roncin and J. Vuillemin}, TITLE = {Introduction to programmable active memories}, BOOKTITLE = {Systolic Array Processors}, EDITOR = {J. McCanny and J. McWhirter and E. Swartzlander}, PUBLISHER={Prentice-Hall}, YEAR = 1990 } @UNPUBLISHED{xilinx, AUTHOR = {{Xilinx,~Inc.}}, TITLE = { The {P}rogrammable {G}ate {A}rray {D}ata {B}ook}, NOTE = {Product Specification}, YEAR = 1988 } @BOOK{grafcet, AUTHOR = {M. Blanchard}, TITLE = {Comprendre, Maitriser et Appliquer le Grafcet}, PUBLISHER = {Cepadues Editions}, YEAR = 1979 } @BOOK{vhdl, author={D. Perry}, title={VHDL}, publisher={McGraw-Hill}, year=1993 } @INPROCEEDINGS{borrione85, AUTHOR = { D. Borrione and C. {Le Faou}}, TITLE = {Overview of the {\sc Cascade} multilevel hardware description language and its mixed mode simulation mechanisms}, BOOKTITLE = { Computer Hardware Description Languages and Their Applications}, PUBLISHER = {Elsevier Science, North Holland}, YEAR = 1985 } @INPROCEEDINGS{bouajjani90, AUTHOR = {A. Bouajjani and J.-C. Fernandez and N. Halbwachs}, TITLE = {Minimal model generation}, BOOKTITLE= {International Workshop on Computer Aided Verification}, ADDRESS={Rutgers (N.J.)}, INSTITUTION= {AMS-DIMACS}, EDITOR= {R.~Kurshan}, MONTH = jun , YEAR = {1990} } @INPROCEEDINGS{concur92, author = {R. Alur and C. Courcoubetis and D. Dill and N. Halbwachs and H. Won{g-T}oi}, title = {Minimization of timed transition systems}, booktitle = {Proceedings of the Third Conference on Concurrency Theory CONCUR '92}, year = {1992}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science 630}, pages = {340-354} } @INPROCEEDINGS{rtss92, AUTHOR={R. Alur and C. Courcoubetis and D. Dill and N. Halbwachs and H. Wong-Toi}, TITLE={ An implementation of three algorithms for timing verification based on automata emptiness}, BOOKTITLE={13th IEEE Real-Time Systems Symposium}, address={Phoenix (Az)}, MONTH=dec , YEAR=1992 } @ARTICLE{bouajjani92, AUTHOR = {A. Bouajjani and J.-C. Fernandez and N. Halbwachs and P. Raymond and C. Ratel}, TITLE = {Minimal state graph generation}, JOURNAL = {Science of Computer Programming}, VOLUME = 18, PAGES={247--269}, YEAR = 1992 } @INPROCEEDINGS{yanakakis92, AUTHOR={D. Lee and M. Yanakakis}, TITLE={Online minimization of transition systems}, BOOKTITLE={24th ACM Symp. on the Theory of Computing, STOC'92, Vancouver, B.C.}, YEAR=1992 } @TECHREPORT{bouajjani90b, AUTHOR = {A. Bouajjani and J.-C. Fernandez and N. Halbwachs}, TITLE = {On the verification of safety properties}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L12}, INSTITUTION = {IMAG, Grenoble}, MONTH=mar , YEAR =1990 } @TECHREPORT {sml, AUTHOR = {M. C. Browne and E. M. Clarke}, TITLE = { {\sc Sml} --- a high-level language for the design and verification of finite state machines}, TYPE = { \researchreport\ }, INSTITUTION = {Carnegie Mellon University}, NUMBER = {CMU-CS-85-179}, YEAR = 1985 } @ARTICLE{sml:ieee, AUTHOR = {E. M. Clarke and D. E. Long and K. L. McMillan}, TITLE={A language for compositional specification and verification of finite state hardware controllers}, JOURNAL={Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, PAGES={1283--1292}, MONTH=sep , YEAR={1991} } @INPROCEEDINGS{broy, AUTHOR = {M. Broy}, TITLE = {Functional specification of time sensitive communicating systems}, BOOKTITLE= {REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness}, EDITOR={J.W. de Bakker and W.-P. de Roever and G. Rozemberg}, PUBLISHER={LNCS 430, Springer Verlag}, MONTH=may , YEAR=1989 } @ARTICLE{akers78, AUTHOR={S. B. Akers}, TITLE={Binary Decision Diagrams}, JOURNAL={IEEE Transactions on Computers}, VOLUME ={C-27}, NUMBER ={6}, YEAR = 1978 } @ARTICLE{bryant86, AUTHOR = {R. E. Bryant}, TITLE = { Graph-based algorithms for boolean function manipulation}, JOURNAL = {IEEE Transactions on Computers}, VOLUME ={C-35}, NUMBER ={8}, PAGES={677--692}, YEAR = 1986 } @ARTICLE{brzozowski, AUTHOR = {J. A. Brzozowski}, TITLE = {Derivative of regular expressions}, JOURNAL = {JACM}, VOLUME = {11}, NUMBER = {4}, YEAR = 1964 } @TECHREPORT{buggiani, AUTHOR = {B. Buggiani and P. Caspi and D. Pilaud}, TITLE = {Programming distributed automatic control systems: a language and compiler solution}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L4}, INSTITUTION = {IMAG, Grenoble}, MONTH = jul , YEAR = 1988 } @TECHREPORT{buors, AUTHOR = {C. Buors }, TITLE = {S\'{e}mantique op\'{e}rationnelle du langage \lustre}, TYPE = {\DEA}, INSTITUTION = {\Universityof\ Grenoble}, MONTH = jun , YEAR = 1986 } @INPROCEEDINGS{burch89, AUTHOR = {J.R. Burch and E.M. Clarke and K.L. McMillan and D.L. Dill and J. Hwang}, TITLE = {Symbolic Model Checking: $10^{20}$ states and beyond}, BOOKTITLE = {Fifth IEEE Symposium on Logic in Computer Science, Philadelphia}, YEAR = 1990, day={4--6}, month=jun, pages={428--439} } @INPROCEEDINGS{cousot78, AUTHOR = { P. Cousot and N. Halbwachs}, TITLE = {Automatic discovery of linear restraints among variables of a program}, BOOKTITLE = { 5th ACM Symposium on Principles of Programming Languages, POPL'78}, address={Tucson (Arizona)}, MONTH =jan, YEAR = 1978 } @TECHREPORT{halbwachs79, AUTHOR = {N. Halbwachs }, TITLE = {D\'etermination automatique de relations lin\'eaires v\'erifi\'ees par les variables d'un programme}, TYPE = {Th\`ese de 3e cycle}, INSTITUTION = {\Universityof\ Grenoble}, MONTH = mar, YEAR = 1979 } @TECHREPORT{halbwachs83, AUTHOR = {N. Halbwachs }, TITLE = { Analyse statique des proprie'te's line'aires des syste`mes inde'terministes et paralle`les}, TYPE = {\techreport\ }, NUMBER = {367}, INSTITUTION = {IMAG, Grenoble}, MONTH = apr , YEAR = 1983 } @INPROCEEDINGS{lustre:popl, AUTHOR = {P. Caspi and D. Pilaud and N. Halbwachs and J. Plaice }, TITLE = {\lustre: a declarative language for programming synchronous systems }, BOOKTITLE = {14th ACM Symposium on Principles of Programming Languages, POPL'87}, ADDRESS={Munchen}, MONTH = jan , YEAR = 1987 } @ARTICLE{clarke86, AUTHOR = {E. M. Clarke and E. A. Emerson and A. P. Sistla }, TITLE = {Automatic verification of finite-state concurrent systems using temporal logic specifications }, JOURNAL = {ACM TOPLAS}, VOLUME = 8, NUMBER = 2, YEAR = 1986 } @INPROCEEDINGS{clarke89, AUTHOR = {E. M. Clarke and D. E. Long and K. L. Mc Millan}, TITLE = {Compositional model checking}, BOOKTITLE = {Fourth IEEE Symposium on Logic in Computer Science}, ADDRESS = {Asilomar}, MONTH = jun , YEAR = 1989 } @INPROCEEDINGS{coudert89, AUTHOR = {O. Coudert and C. Berthet and J. C. Madre}, TITLE = {Verification of synchronous sequential machines based on symbolic execution}, BOOKTITLE = {International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, YEAR = {1989} } @INPROCEEDINGS{coudert90, AUTHOR = {O. Coudert and J. C. Madre and C. Berthet}, TITLE = {Verifying Temporal Properties of Sequential Machines Without Building Their State Diagrams}, BOOKTITLE= {International Workshop on Computer Aided Verification}, ADDRESS={Rutgers (N.J.)}, INSTITUTION= {AMS-DIMACS}, EDITOR= {R.~Kurshan}, MONTH = jun , YEAR = {1990} } @INPROCEEDINGS{courcoubetis90, AUTHOR ={C. Courcoubetis and M. Vardi and P. Wolper and M. Yanakakis}, TITLE={Memory efficient algorithms for the verification of temporal properties}, BOOKTITLE= {International Workshop on Computer Aided Verification}, ADDRESS={Rutgers (N.J.)}, INSTITUTION= {AMS-DIMACS}, EDITOR= {R.~Kurshan}, MONTH = jun , YEAR = {1990} } @INPROCEEDINGS{graf90, AUTHOR ={S. Graf and B. Steffen}, TITLE={Compositional Minimization of Finite State Systems}, BOOKTITLE= {International Workshop on Computer Aided Verification}, address={Rutgers (N.J.)}, INSTITUTION= {AMS-DIMACS}, EDITOR= {R.~Kurshan}, MONTH = jun , YEAR = {1990} } @INPROCEEDINGS{cousot77, AUTHOR = {P. Cousot and R. Cousot}, TITLE = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, BOOKTITLE = {4th ACM Symposium on Principles of Programming Languages, POPL'77}, address = {Los Angeles}, MONTH = jan , YEAR = 1977 } @TECHREPORT{l8, AUTHOR = {N. Halbwachs and P. Raymond and C. Ratel}, TITLE = {Generating Efficient Code From Data-Flow Programs}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L8}, INSTITUTION = {IMAG, Grenoble}, MONTH = feb , YEAR = 1991 } @INPROCEEDINGS{lustre:plilp, AUTHOR = {N. Halbwachs and P. Raymond and C. Ratel}, TITLE = {Generating Efficient Code From Data-Flow Programs}, BOOKTITLE = {Third International Symposium on Programming Language Implementation and Logic Programming}, PUBLISHER = {LNCS 528, Springer Verlag}, address={Passau (Germany)}, MONTH = aug , YEAR = 1991 } @INPROCEEDINGS{lesar:sigsoft, AUTHOR = {C. Ratel and N. Halbwachs and P. Raymond }, TITLE = {Programming and verifying critical systems by means of the synchronous data-flow programming language \lustre}, BOOKTITLE = {ACM-SIGSOFT'91 Conference on Software for Critical Systems}, address={New Orleans}, MONTH = dec , YEAR = 1991 } @ARTICLE{lesar:tse, AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel }, TITLE = {Programming and verifying real-time systems by means of the synchronous data-flow programming language \lustre}, JOURNAL = {IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems}, pages={785--793}, MONTH=sep , YEAR=1992 } @ARTICLE{fernandez90, AUTHOR = {J.-C. Fernandez} , TITLE = {An Implementation of an Efficient Algorithm for Bisimulation Equivalence}, JOURNAL = {Science of Computer Programming}, VOLUME = {13}, NUMBER = {2-3}, MONTH = may , YEAR = {1990} } @INPROCEEDINGS{gabay80, AUTHOR = {D. Gabbay and A. Pnueli and S. Shelah and J. Stavi }, TITLE = {On the temporal analysis of fairness }, BOOKTITLE = {7th ACM Symposium on Principles of Programming Languages, POPL'80}, ADDRESS = {Las Vegas}, MONTH = jan , YEAR = 1980 } @TECHREPORT{glory:these, AUTHOR = {A-C. Glory}, TITLE = {V\'{e}rification de propri\'{e}t\'{e}s de programmes flots de donn\'{e}es synchrones}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Joseph Fourier}, ADDRESS = {Grenoble, France}, MONTH = dec , YEAR = 1989 } @UNPUBLISHED{gonthier85, AUTHOR = {G. Gonthier }, TITLE = {Private communication}, NOTE={}, YEAR = 1985 } @TECHREPORT{gonthier:these, AUTHOR = {G. Gonthier}, TITLE = { S\'{e}mantiques et mod\`{e}les d'ex\'{e}cution des langages r\'{e}actifs synchrones; Application \`{a} \esterel}, TYPE = {\Thesis}, INSTITUTION = {\Universityof\ Paris VI}, ADDRESS = {Paris, France}, YEAR = 1988 } @INPROCEEDINGS{HDLC, TITLE = {Incremental Development of an {HDLC} Protocol in {Esterel}}, AUTHOR = {G. Berry and G. Gonthier}, BOOKTITLE = {Proc. Ninth International Symposium on Protocol Specification, Testing, and Verification}, PUBLISHER = {North-Holland}, YEAR = {1989} } @ARTICLE{HDLCJournal, AUTHOR = {G. Berry and G. Gonthier}, TITLE = {Incremental development of an HDLC entity in {Esterel}}, JOURNAL = {Comp. Networks and ISDN Systems}, VOLUME = 22, PAGES = {35--49}, YEAR = 1991 } @TECHREPORT{reflex:strl, TITLE = {Programming a Reflex Game in {Esterel} v3\_2}, AUTHOR = {F. Boussinot}, TYPE = {\researchreport\ 07/91}, INSTITUTION = {Centre de Math\'ematiques Appliqu\'ees, Ecole des Mines de Paris, Sophia-Antipolis}, YEAR = 1991 } @INPROCEEDINGS{lustre:systolique, AUTHOR = {N. Halbwachs and D. Pilaud }, TITLE = {Use of a real-time declarative language for systolic array design and simulation}, BOOKTITLE = {International Workshop on Systolic Arrays}, ADDRESS = {Oxford}, MONTH = jul , YEAR = 1986 } @INPROCEEDINGS{lustre:circuits1, AUTHOR = {N. Halbwachs and A. Lonchampt and D. Pilaud }, TITLE = {Describing and designing circuits by means of a synchronous declarative language}, BOOKTITLE = {IFIP Working Conference ``From HDL Descriptions To Guaranteed Correct Circuit Designs''}, ADDRESS = {Grenoble}, MONTH = sep , YEAR = 1986 } @INPROCEEDINGS{lustre:preuve, AUTHOR = {N. Halbwachs and D. Pilaud and F. Ouabdesselam and A.C. Glory}, TITLE = {Specifying, Programming and Verifying Real-Time Systems, using a synchronous declarative language}, BOOKTITLE= {Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, MONTH = jun , YEAR = 1989 } @ARTICLE{arbitre, AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel}, TITLE = {An experience in proving regular networks of processes by modular model checking}, JOURNAL={Acta Informatica}, VOLUME= 29, NUMBER= {6/7}, PAGES={523--543}, YEAR = 1992 } @INPROCEEDINGS{harel84, AUTHOR = {D. Harel }, TITLE = {Statecharts: A visual approach to complex systems}, BOOKTITLE = {Advanced NATO Institute on Logics and Models for Verification and Specification of Concurrent Systems}, ADDRESS = {La Colle-sur-Loup}, YEAR = 1984 } @ARTICLE{harel87, AUTHOR = {D. Harel }, TITLE = {Statecharts: A visual approach to complex systems}, JOURNAL = {Science of Computer Programming}, VOLUME = 8, NUMBER = 3, YEAR = 1987 } @BOOK{occam, AUTHOR={{INMOS~Ltd}}, TITLE={The Occam Programming Manual}, PUBLISHER={Prentice-Hall International}, YEAR=1984 } @ARTICLE{mok, AUTHOR = {F. Jahanian and A.K. Mok}, TITLE = {Safety analysis of timing properties in real-time systems}, JOURNAL = {IEEE Transactions on Software Engineering}, VOLUME = {SE-2}, YEAR = 1986 } @INPROCEEDINGS{kahn74, AUTHOR = {G. Kahn }, TITLE = {The semantics of a simple language for parallel programming}, BOOKTITLE = {IFIP 74}, PUBLISHER = {North Holland}, YEAR = 1974 } @INPROCEEDINGS{kahn77, AUTHOR = {G. Kahn and D. B. Mac~Queen}, TITLE = {Coroutines and networks of parallel processes}, BOOKTITLE = {IFIP Congress}, YEAR = 1977 } @INPROCEEDINGS{kanellakis83, AUTHOR = {P. Kanellakis and S. Smolka} , TITLE = {{\sc CCS} Expressions, Finite State Processes and Three Problems of Equivalence} , BOOKTITLE= {Proceedings ACM Symp. on Principles of Distribued Computing} , YEAR = 1983 } @INPROCEEDINGS{koymans83, AUTHOR = {R. Koymans and W. P. DeRoever}, TITLE = {Examples of a real-time temporal logic specification }, BOOKTITLE = {The analysis of Concurrent Systems}, PUBLISHER = {LNCS 207, Springer Verlag}, MONTH = aug , YEAR = 1983 } @INPROCEEDINGS{huizing88, AUTHOR={C. Huizing and R. Gerth and W. P. {de Roever}}, TITLE={Modelling {Statecharts} behaviour in a fully abstract way}, BOOKTITLE = {13th CAAP}, PUBLISHER={LNCS 299, Springer Verlag}, YEAR= 1988 } @TECHREPORT{signal1, AUTHOR = {P. Le~Guernic and A. Benveniste and P. Bournai and T. Gautier}, TITLE = {\signal: a data-flow oriented language for signal processing}, TYPE = {RR}, NUMBER = 378, INSTITUTION = {INRIA}, YEAR = 1985 } @TECHREPORT{signalea, AUTHOR = {A. Benveniste}, TITLE = {Constructive probability and the {SIGNALEA} language: building and handling stochastic processes via programming}, TYPE = {RR}, NUMBER = 1532, INSTITUTION = {INRIA}, YEAR = 1991 } @ARTICLE{signal2, AUTHOR = {P. Le~Guernic and A. Benveniste and P. Bournai and T. Gautier}, TITLE = {\signal , a data flow oriented language for signal processing}, JOURNAL = {IEEE-ASSP}, VOLUME = 34, NUMBER = 2, PAGES ={362--374}, YEAR = 1986 } @ARTICLE{signal:ieee, AUTHOR = {P. {Le~Guernic} and T. Gautier and M. {Le~Borgne} and C. {Le~Maire}}, TITLE = {Programming real time applications with \signal}, JOURNAL={Proceedings of the IEEE}, VOLUME={79}, NUMBER={9}, PAGES={1321-1336}, MONTH=sep , YEAR={1991} } @TECHREPORT{legoff, AUTHOR = {B. LeGoff}, TITLE = {Inf\'{e}rence de contr\^{o}le hi\'{e}rarchique, Application au temps r\'{e}el}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Rennes 1}, MONTH = jun , YEAR = 1989 } @ARTICLE{signal4, AUTHOR={A. Benveniste and P. Le~Guernic}, TITLE={Hybrid dynamical systems theory and the \signal\ language}, JOURNAL={IEEE Transactions on Automatic Control}, VOLUME= 35, NUMBER= 5, MONTH= may , YEAR = 1990, PAGES = {535-546} } @INPROCEEDINGS{signal5, TITLE = {{Signal}, a Declarative Language for Synchronous Programming of Real-Time Systems}, AUTHOR = {T. Gauthier and P. Le Guernic and L. Besnard}, BOOKTITLE = {Proc. 3rd. Conf. on Functional Programming Languages and Computer Architecture}, PUBLISHER={LNCS 274, Springer Verlag}, YEAR = {1987} } @INCOLLECTION {hale87, AUTHOR = {R. Hale}, TITLE = {Temporal logic programming}, CHAPTER = 3, BOOKTITLE = { Temporal logics and their applications}, EDITOR = {A. Galton}, PUBLISHER = {Academic Press, London}, MONTH = dec , YEAR = 1987 } @INPROCEEDINGS{holzmann87a, AUTHOR = {G. J. Holzmann}, TITLE = {On limits and possibilities of automated protocols analysis}, BOOKTITLE = {IFIP WG-6.1 7th. International Conference on Protocol Specification, Testing and Verification}, PUBLISHER = {North Holland}, ADDRESS = {Zurich}, YEAR = 1987 } @ARTICLE{holzmann87b, AUTHOR = {G. J. Holzmann}, TITLE = {Automated Protocol Validation in {\sc Argos}~: Assertion Proving and scatter searching}, JOURNAL = {IEEE Trans. on Software Ingineering}, VOLUME = {SE-13}, NUMBER = 6, PAGES = {683--696}, MONTH = jun , YEAR = 1987 } @INPROCEEDINGS{jard89, AUTHOR={C. Jard and Th. J\'{e}ron}, TITLE = {On-line model checking for finite linear temporal logic specifications}, BOOKTITLE = {International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, YEAR = {1989} } @INPROCEEDINGS{fernandez91, AUTHOR={J.-C. Fernandez and L. Mounier}, TITLE={On the fly verification of behavioural equivalences and preorders}, BOOKTITLE = {Workshop on Computer-Aided Verification, Aalborg (Denmark)}, MONTH = jun , YEAR = {1991} } @ARTICLE{lynch89, AUTHOR = {N. Lynch and E. W. Stark}, TITLE = { A Proof of Kahn Principle for Input/Output Automata}, JOURNAL = {Information and Computation}, NUMBER = 82, YEAR = 1989 } @INPROCEEDINGS{manna82, AUTHOR = {Z. Manna and A. Pnueli }, TITLE = {Verification of concurrent programs: the temporal framework }, BOOKTITLE = {The Correctness Problem in Computer Science }, PUBLISHER = {International Lecture Series in Computer Science, Academic Press}, ADDRESS = {London}, YEAR = 1982 } @ARTICLE{manna84, AUTHOR = {Z. Manna and P. Wolper}, TITLE = {Synthesis of communicating processes from temporal logic specifications}, JOURNAL = {ACM TOPLAS}, VOLUME = 6, NUMBER = 1, MONTH = jan , YEAR = 1984 } @INPROCEEDINGS{manna88, AUTHOR = {Z. Manna and A. Pnueli}, TITLE = {The anchored version of the temporal framework}, BOOKTITLE={Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency}, EDITOR={J.W. de Bakker, W.P. de Roever and G. Rozenberg}, PUBLISHER={LNCS 354, Springer Verlag}, MONTH= jun , YEAR= {1988} } @ARTICLE{val, AUTHOR = {J. R. Mc~Graw }, TITLE = {The {\sc Val} language: Description and analysis}, JOURNAL = {ACM TOPLAS}, VOLUME = 4, NUMBER = 1, MONTH = jan , YEAR = 1982 } @TECHREPORT{mauras:these, AUTHOR = {Ch. Mauras}, TITLE = {{\sc Alpha}~: un langage \'{e}quationnel pour la conception d'architectures parall\`{e}les synchrones}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Rennes 1}, MONTH = dec , YEAR = 1989 } @TECHREPORT{milner81, AUTHOR={R. Milner}, TITLE={On relating synchrony and asynchrony}, TYPE={\techreport\ }, NUMBER={CSR-75-80}, INSTITUTION={Computer Science Dept., Edimburgh Univ.}, YEAR= 1981 } @ARTICLE{milner83, AUTHOR = {R. Milner }, TITLE = {Calculi for synchrony and asynchrony}, JOURNAL = {TCS}, VOLUME = 25, NUMBER = 3, MONTH = jul , YEAR = 1983 } @BOOK{ccs, author = {R. Milner} , title = {A Calculus of Communicating Systems} , publisher= {LNCS 92, Springer Verlag} , year = {1980} } @ARTICLE{hennessy85, AUTHOR={M. Hennessy and R. Milner}, TITLE={Algebraic laws for nondeterminism and concurrency}, JOURNAL={JACM}, VOLUME= 32, NUMBER= 1, MONTH=jan , YEAR= 1985, PAGES={137--161} } @incollection{Park81, Author = {D. Park}, Title = {Concurrency and Automata on infinite sequences}, booktitle= {5th GI-Conference on Theoretical Computer Science}, note= {LNCS 104}, publisher= { Springer Verlag } , year = { 1981 } } @PHDTHESIS{moszkowski:these, AUTHOR = {B. C. Moszkowski }, TITLE = {Reasoning about digital circuits }, NOTE = {\researchreport\ STAN-CS-83-970}, SCHOOL = {Stanford University}, MONTH = jul, YEAR = 1983 } @INPROCEEDINGS{moszkowski84, AUTHOR = {B. Moszkowski and Z. Manna }, TITLE = {Reasoning in interval temporal logic}, BOOKTITLE = {Workshop on Logics of Programs}, PUBLISHER = {LNCS 164, Springer Verlag}, YEAR = 1984 } @ARTICLE{paige87, AUTHOR = {R. Paige and R. Tarjan} , TITLE = {Three Partition Refinement Algorithms} , JOURNAL= {SIAM J. Comput.} , NUMBER= 6, VOLUME = 16 , YEAR = 1987 } @INPROCEEDINGS{lustre:tl, AUTHOR = {D. Pilaud and N. Halbwachs }, TITLE = {From a synchronous declarative language to a temporal logic dealing with multiform time}, BOOKTITLE = {Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems}, EDITOR = {M. Joseph}, ADDRESS = {Warwick}, PUBLISHER = {LNCS 331, Springer Verlag}, MONTH = sep , YEAR = 1988 } @TECHREPORT{lustre:manual, AUTHOR = {J. A. Plaice and N. Halbwachs }, TITLE = {\lustre-{\sc V2} User's guide and reference manual}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L2}, INSTITUTION = {IMAG}, ADDRESS = {Grenoble}, MONTH = oct , YEAR = 1987 } @UNPUBLISHED{oc, AUTHOR = {J. A. Plaice and J-B. Saint}, TITLE = {The \lustre-\esterel\ portable format} , NOTE = {\unpublishedreport, INRIA, Sophia Antipolis}, YEAR = 1987 } @UNPUBLISHED{ic, AUTHOR = {J-B. Saint and J-P. Paris}, TITLE = {Les instructions du code interm\'{e}diaire, description syntaxique} , NOTE = {\unpublishedreport, INRIA, Sophia Antipolis}, YEAR = 1990 } @TECHREPORT{paris:these, AUTHOR={J-P. Paris}, TITLE={Ex\'ecution de t\^aches asynchrones depuis {Esterel}}, TYPE={\Thesis}, INSTITUTION={\Universityof\ Nice}, ADDRESS={Nice, France}, YEAR= 1992 } @TECHREPORT{costemaniere, AUTHOR={E. Coste-Mani\`ere}, TITLE={Synchronisme et asynchronisme dans la programmation des syst\`emes robotiques: apport du langage {Esterel} et de concepts objets}, TYPE={\Thesis}, INSTITUTION={Ecole Nationale Sup\'erieure des Mines de Paris}, YEAR=1991 } @TECHREPORT{plaice:these, AUTHOR = {J. A. Plaice}, TITLE = {S\'{e}mantique et compilation de \lustre, un langage d\'{e}claratif synchrone}, TYPE = {\Thesis}, INSTITUTION = {Institut National Polytechnique de Grenoble}, YEAR = 1988 } @TECHREPORT{plotkin81, AUTHOR = {G. D. Plotkin }, TITLE = {A structural approach to operational semantics}, TYPE = {Lecture Notes}, INSTITUTION = {Aarhus University}, YEAR = 1981 } @INPROCEEDINGS{pnueli77, AUTHOR = {A. Pnueli }, TITLE = {The temporal logic of programs}, BOOKTITLE = {18th Symp. on the Foundations of Computer Science}, PUBLISHER = {IEEE}, ADDRESS = {Providence R.I.}, YEAR = 1977 } @ARTICLE{prywes83, AUTHOR= {N.S. Prywes and A. Pnueli}, TITLE={Compilation of nonprocedural specifications into computer programs}, JOURNAL={IEEE Transactions on Software Engineering}, VOLUME={SE-9}, NUMBER={3}, MONTH=may , YEAR=1983 } @INPROCEEDINGS{pnueli85, AUTHOR = {O. Lichtenstein and A. Pnueli and L. Zuck}, TITLE = {The glory of the past}, BOOKTITLE = {Conference on Logics of Programs}, PUBLISHER = {LNCS 194, Springer Verlag}, YEAR = 1985 } @INPROCEEDINGS{pnueli85a, AUTHOR = {O. Lichtenstein and A. Pnueli}, TITLE = {Checking that finite state concurrent programs satisfy their linear specifications}, BOOKTITLE = {12th ACM Symposium on Principles of Programming Languages, POPL'85}, ADDRESS = {New-Orleans}, MONTH = jan , YEAR = 1985 } @INPROCEEDINGS{pnueli89, AUTHOR = {A. Pnueli and R. Rosner}, TITLE = {On the synthesis of a reactive module}, BOOKTITLE = {16th ACM Symposium on Principles of Programming Languages, POPL'89}, YEAR = 1989 } @INPROCEEDINGS{pnueli89b, AUTHOR = {A. Pnueli and R. Rosner}, TITLE = {On the synthesis of an asynchronous reactive module}, BOOKTITLE = {16th ICALP}, EDITOR={G. Ausiello and M. Dezani-Ciancaglini and S. Ronchi Della Rocca}, PUBLISHER = {LNCS 372, Springer Verlag}, MONTH = jul , YEAR = {1989} } @INPROCEEDINGS{cesar1, AUTHOR = {J. P. Queille and J. Sifakis }, TITLE = {Specification and verification of concurrent systems in {C}esar}, BOOKTITLE = {International Symposium on Programming}, PUBLISHER = {LNCS 137, Springer Verlag}, MONTH = apr , YEAR = 1982 } @INPROCEEDINGS{caesar, AUTHOR = {Hubert Garavel and Joseph Sifakis}, TITLE = {Compilation and Verification of {\sc Lotos} Specifications}, BOOKTITLE = {Proceedings of the 10th IFIP International Symposium on Protocol Specification, Testing and Verification (Ottawa)}, YEAR = {1990}, EDITOR = {L. Logrippo and R. L. Probert and H. Ural}, PUBLISHER = {North Holland}, MONTH = jun } @inproceedings{Garavel89c, author = {Hubert Garavel}, title = {Compilation of {L}OTOS Abstract Data Types}, booktitle = {Proceedings of the 2nd International Conference on Formal Description Techniques {FORTE}'89 (Vancouver B.C., Canada)}, year = {1989}, editor = {Son T. Vuong}, publisher = {North Holland}, address = {Amsterdam}, month = dec, annote = {presentation de CAESAR.ADT} } @techreport{garavel89b, author = {Hubert Garavel}, INSTITUTION = {Universite' Joseph~Fourier, Grenoble}, title = {Compilation et ve'rification de programmes Lotos}, TYPE = {\Thesis}, year = {1989}, month = nov } @article{siftcs82, author= {J. Sifakis}, title= {A unified approach for studying the properties of transition systems}, journal={TCS}, volume= {3}, year= {1982} } @TECHREPORT{rasse:dea, AUTHOR = {A. Rasse }, TITLE = {\cleo, interpr\'{e}tation de la non correction de programmes sur un mod\`{e}le}, TYPE = {\techreport\ }, NUMBER = {SPECTRE C10}, INSTITUTION = {IMAG}, ADDRESS = {Grenoble}, MONTH = jun, YEAR = 1988 } @TECHREPORT{ratel:dea, AUTHOR = {C. Ratel }, TITLE = {Etude de la conformit\'{e} d'un programme \lustre\ et de ses sp\'ecifications en logique temporelle arborescente}, TYPE = {\DEA}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH = jun , YEAR = 1988 } @TECHREPORT{raymond, AUTHOR = {P. Raymond}, TITLE = { Compilation s\'{e}par\'{e}e de programmes \lustre}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L5}, INSTITUTION = {IMAG}, ADDRESS = {Grenoble}, MONTH = jun , YEAR = 1988 } @INPROCEEDINGS{cesar2, AUTHOR = {J. L. Richier and C. Rodriguez and J. Sifakis and J. Voiron }, TITLE = {Verification in {\sc Xesar} of the sliding window protocol}, BOOKTITLE = {IFIP WG-6.1 7th. International Conference on Protocol Specification, Testing and Verification}, PUBLISHER = {North Holland}, ADDRESS = {Zurich}, YEAR = 1987 } @TECHREPORT{cesar:manual, AUTHOR = {J. L. Richier and C. Rodriguez and J. Sifakis and J. Voiron }, TITLE = {\xesar\ user's guide}, TYPE = {\techreport\ }, NUMBER = {SPECTRE C??}, INSTITUTION = {IMAG}, ADDRESS = {Grenoble}, MONTH = sep, YEAR = 1987 } @TECHREPORT{dea:rocheteau, AUTHOR = {F. Rocheteau}, TITLE = {Programmation d'un circuit massivement parall\`{e}le \`{a} l'aide d'un langage d\'{e}claratif synchrone }, TYPE = {\techreport\ }, NUMBER = {SPECTRE L10}, INSTITUTION = {IMAG, Grenoble}, MONTH = jun , YEAR = 1989 } @INPROCEEDINGS{lustre:pam, AUTHOR={F. Rocheteau and N. Halbwachs}, TITLE={Implementing reactive programs on circuits, a hardware implementation of \lustre}, BOOKTITLE ={{\sc Rex} Workshop on Real-Time: Theory in Practice, DePlasmolen (Netherlands)}, PUBLISHER={LNCS 600, Springer Verlag}, PAGES={195--208}, MONTH = jun , YEAR= {1991} } @BOOK{rex91, KEY={REX91}, TITLE={{\sc Rex} Workshop on Real-Time: Theory in Practice, DePlasmolen (Netherlands)}, editor={J.W. de Bakker and C. Huizing and W. P. de Roever and G. Rozenberg}, PUBLISHER={LNCS 600, Springer Verlag}, MONTH = jun , YEAR= {1991} } @INPROCEEDINGS{pollux:bonas, AUTHOR={F. Rocheteau and N. Halbwachs}, TITLE={{\sc Pollux}, A {\sc Lustre}-based hardware design environment}, BOOKTITLE={Conference on Algorithms and Parallel {VLSI} Architectures {II}, Chateau de Bonas}, EDITOR = {P. Quinton and Y. Robert}, MONTH = jun , YEAR= {1991} } @TECHREPORT{raymond91, AUTHOR = {P. Raymond}, TITLE = {Compilation efficace d'un langage d\'eclaratif synchrone~: Le g\'en\'erateur de code \lustre-V3}, TYPE = {\Thesis}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH=nov , YEAR = {1991} } @TECHREPORT{Roy89, AUTHOR = {V. Roy and {R. de} Simone}, TITLE = {An {\sc Autograph} Primer}, TYPE = {\techreport\ }, INSTITUTION = {INRIA}, ADDRESS = {Sophia-Antipolis}, MONTH = may , YEAR = 1989 } @TECHREPORT{Roy90, AUTHOR={V. Roy}, TITLE={\autograph, Un outil de visualisation pour les calculs de processus}, TYPE={\Thesis}, INSTITUTION={\Universityof\ Nice}, YEAR= 1990 } @TECHREPORT{fctools, AUTHOR={A. Bouali and A. Ressouche and V. Roy and R. {de Simone}}, TITLE = {The FC2Tools User Manual (Version v1.0)}, TYPE = {\techreport\ }, INSTITUTION = {INRIA}, ADDRESS = {Sophia-Antipolis}, YEAR = 1996 } @INPROCEEDINGS{auto, AUTHOR = {G. Boudol and V. Roy and R. de Simone and D. Vergamini}, TITLE = {Process Calculi, from Theory to Practice: Verification Tools}, BOOKTITLE = {International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, YEAR = {1989} } @INPROCEEDINGS{Auto:Cav90, AUTHOR= {V. Roy and R. de Simone}, TITLE= {{Auto} and {Autograph}}, BOOKTITLE= {International Workshop on Computer Aided Verification}, ADDRESS={Rutgers (N.J.)}, INSTITUTION= {AMS-DIMACS}, EDITOR= {R.~Kurshan}, MONTH= jun , YEAR= 1990} @TECHREPORT{schwartz83, AUTHOR = {R. L. Schwartz and P. M. Melliar-Smith and F. H. Vogt }, TITLE = {An interval logic for higher-level temporal reasonning: language definition and examples}, TYPE = {\researchreport\ }, NUMBER = {CSL-138}, INSTITUTION = {Computer Science Lab. , SRI International}, MONTH = feb , YEAR = 1983 } @INPROCEEDINGS{sheran84, AUTHOR = {M. Sheeran }, TITLE = {$\mu$-{sc FP}, a language for {sc VLSI} design}, BOOKTITLE = {ACM Symposium on Lisp and Functional Programming}, ADDRESS = {Austin}, YEAR = 1984 } @PHDTHESIS{sistla83, AUTHOR = {A. P. Sistla}, TITLE = {Theoretical issues in the design and verification of distributed systems}, SCHOOL = {Harvard University}, YEAR = 1983 } @INPROCEEDINGS{vardi86, AUTHOR = {M. Y. Vardi and P. Wolper}, TITLE = {An automata-theoretic approach to automatic program verification}, BOOKTITLE = {Symposium on Logic in Computer Science}, MONTH = jun , YEAR = {1986} } @INPROCEEDINGS{wolper94, AUTHOR={O. Bernholtz and M. Vardi and P. Wolper}, TITLE = {An automata-theoretic approach to branching-time model checking}, BOOKTITLE ={6th International Conference on Computer Aided Verification, CAV'94}, ADDRESS = {Stanford}, EDITOR = {D. Dill}, MONTH = jun , YEAR = 1994 } @TECHREPORT{auto1, AUTHOR = {D. Vergamini }, TITLE = {Verification by means of observational equivalence on automata}, INSTITUTION = {INRIA}, NUMBER = 501, YEAR = 1986 } @TECHREPORT{these:fernandez, AUTHOR = {J.-C. Fernandez}, TITLE = {Aldebaran~: un syst\`{e}me de v\'{e}rification par r\'{e}duction de processus communicants}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Joseph Fourier, Grenoble}, YEAR = 1988 } @INPROCEEDINGS{harel85, AUTHOR = {D. Harel and A. Pnueli}, TITLE = {On the Development of Reactive Systems}, BOOKTITLE = {Logic and Models of Concurrent Systems, {\sc NATO} Advanced Study Institute on Logics and Models for Verification and Specification of Concurrent Systems}, PUBLISHER = {Springer Verlag}, YEAR = 1985 } @INPROCEEDINGS{harel86, AUTHOR = {D. Harel and A. Pnueli and J. P. Schmidt and R. Sherman}, TITLE = {On the formal semantics of {Statecharts}}, BOOKTITLE = {Logic in Computer Science}, YEAR = 1986 } @ARTICLE{lustre:clocks, AUTHOR = {P. Caspi}, TITLE = {Clocks in Dataflow languages}, JOURNAL = {Theoretical Computer Science}, VOLUME = {94}, PAGES = {125--140}, YEAR = {1992} } @ARTICLE{lustre:tsi, AUTHOR = {N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud }, TITLE = {Programmation et v\'{e}rification des syst\`{e}mes r\'{e}actifs \`{a} l'aide du langage flot de donn\'{e}es synchrone \lustre}, JOURNAL = {Technique et Science Informatique}, VOLUME={10}, NUMBER={2}, YEAR = 1991 } @INPROCEEDINGS{wolper90, AUTHOR = {P. Wolper and V. Lovinfosse}, TITLE = {Verifying properties of large sets of processes with network invariants}, BOOKTITLE = {International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, YEAR = {1989} } @TECHREPORT{c2a:1, AUTHOR = {A. Benveniste}, TITLE = {Les langages synchrones: des noyaux logiciels pour la sp\'{e}cification et la conception des syst\`{e}mes de contro^le commande}, TYPE = {Rapport ``Collaboration CAO Automatiqu\'{e}'}, NUMBER = {\mynumber~1}, MONTH = feb, YEAR = 1989 } @TECHREPORT{c2a:2, AUTHOR = {N. Halbwachs and Th. Gauthier}, TITLE = {Programmation graphique de syst\'{e}mes temps r\'{e}el \`{a} l'aide de langages d\'{e}claratifs synchrones}, TYPE = {Rapport ``Collaboration CAO Automatiqu\'{e}'}, NUMBER = {\mynumber~2}, MONTH = mar , YEAR = 1989 } @TECHREPORT{c2a:3, AUTHOR = {V. Lecompte and F. Boussinot}, TITLE = {Une application de la programmation synchrone: le modem du minitel en \esterel}, TYPE = {Rapport ``Collaboration CAO Automatiqu\'{e}'}, NUMBER = {\mynumber~3}, MONTH = feb , YEAR = 1989 } @TECHREPORT{Billon87, AUTHOR = {J.P. Billon}, TITLE = {Perfect Normal Forms For Discrete functions}, TYPE ={\researchreport\ }, INSTITUTION={BULL}, NUMBER = {\mynumber~87019}, MONTH = jun , YEAR = 1987 } @INPROCEEDINGS{Billon88, AUTHOR = {J.P. Billon and J.C. Madre}, TITLE = {Original Concepts of {PRIAM}, an industrial tool for efficient formal verification of combinational circuits}, BOOKTITLE ={IFIP WG 10.2 Int Working Conference on the Fusion of Hardware Design and Verification}, ADDRESS={Glasgow, Scotland}, MONTH =jul , YEAR ={1988}, EDITOR={G. Milne}, PUBLISHER={North Holland} } @INPROCEEDINGS{Madre88, AUTHOR = {J.C. Madre and J.P. Billon}, TITLE ={Proving Circuit Correctness by Formally Comparing their Expected and Extracted Behavior}, BOOKTITLE = {25th Design Automation Conference}, ADDRESS = {Anaheim}, MONTH = jun , YEAR = 1988 } @ARTICLE{Madre89a, AUTHOR = {J.C. Madre and F. Anceau and J.P. Billon}, TITLE = {Formal Verification in an Industrial Environment}, JOURNAL = {International Journal of Computer Aided VLSI Design}, YEAR = {1989} } @INPROCEEDINGS{Madre89b, AUTHOR = {J.C. Madre and O. Coudert and J.P. Billon and C. Berthet}, TITLE ={Formal Verification and Diagnosis of Digital Circuits Using a Propositional Theorem Prover}, BOOKTITLE = {Working Conference on the CAD Systems Using AI Techniques}, MONTH = jun , ADDRESS = {Tokyo}, YEAR = 1989 } @UNPUBLISHED{Madre89c, AUTHOR={J.C. Madre and O. Coudert and J.P. Billon}, TITLE ={Automating the Diagnosis and the Rectification of Design Errors with {PRIAM}}, NOTE = {submitted to ICCAD 89} } @INPROCEEDINGS{borrione87c, AUTHOR={D. Borrione and J.L. Paillet }, TITLE ={An approach to the formal verification of VHDL descriptions}, BOOKTITLE={VHDL User's Workshop Charlottesville, Va}, MONTH = apr , YEAR = 1988 } @INPROCEEDINGS{borrione88a, AUTHOR={D. Borrione and J.L. Paillet and L. Pierre}, TITLE ={Formal Verification of CASCADE Descriptions}, BOOKTITLE ={IFIP WG 10.2 International Working Conference on the Fusion of Hardware Design and Verification}, ADDRESS = {Glasgow}, EDITOR={G.Milne}, PUBLISHER={North Holland}, MONTH = jul , YEAR = 1988 } @INPROCEEDINGS{borrione88b, AUTHOR={D. Borrione and P. Camurati and J.L. Paillet and P. Prinetto}, TITLE ={A functional approach to formal hardware verification: the MTI experience}, BOOKTITLE={IEEE international conference on computer design ICCD'88}, ADDRESS={Port Chester, New York}, MONTH = oct , YEAR = 1988 } @TECHREPORT{collavizza89a, AUTHOR={H. Collavizza}, TITLE ={Premi\`{e}re \'{e}valuation du logiciel OBJ3 pour la preuve formelle des circuits digitaux}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~89-01}, MONTH=jan , YEAR = 1989 } @TECHREPORT{paillet85, AUTHOR={J.L. Paillet}, TITLE ={Un mod\`{e}le de fonctions s\'{e}quentielles pour la v\'{e}rification formelle de syst\`{e}mes digitaux}, TYPE={\researchreport\ }, INSTITUTION={IMAG-ARTEMIS}, NUMBER={\mynumber~546}, ADDRESS={Grenoble}, MONTH=jun , YEAR = 1985 } @TECHREPORT{paillet86a, AUTHOR={J.L. Paillet}, TITLE ={Formes fonctionnelles pour l'expression de sp\'{e}cifications temporelles}, TYPE={\researchreport\ }, INSTITUTION={IMAG-ARTEMIS}, NUMBER={\mynumber~593}, ADDRESS={Grenoble}, MONTH=jan , YEAR = 1986 } @INPROCEEDINGS{paillet86b, AUTHOR={J.L. Paillet}, TITLE ={A functional Model for Descriptions and Specifications of Digital Devices}, BOOKTITLE={IFIP Int. Working Conf. ``From HDL Descriptions to Guaranteed Correct Circuit Designs'' }, ADDRESS={Grenoble}, MONT=sep , YEAR = 1986 } @INPROCEEDINGS{paillet89, AUTHOR={J.L. Paillet}, TITLE ={Functional Semantics of Microprocessors at the Machine Instruction Level}, BOOKTITLE={IFIP WG 10.2 9th Int. Symposium on Computer Hardware Description Languages ``CHDL'89''}, ADDRESS={Washington}, PUBLISHER={North-Holland}, MONTH=jun , YEAR = 1989 } @TECHREPORT{pierre86, AUTHOR={L. Pierre}, TITLE ={Algorithme d'\'{e}limination par substitution des variables internes d'un syst\`{e}me de modules interconnect\'{e}s et application \`{a} des descriptions CASCADE}, \TYPE={\DEA\ }, INSTITUTION={Universit\'{e} de Provence}, MONTH=jul , YEAR = 1986 } @TECHREPORT{pierre89a, AUTHOR={L. Pierre}, TITLE ={Mod\'{e}lisation de plusieurs types de circuits s\'{e}quentiels et preuve au moyen du d\'{e}monstrateur de Boyer et Moore}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~89-05}, MONTH=apr , YEAR = 1989 } @TECHREPORT{gthuau90, AUTHOR={G. Thuau and D. Pilaud}, TITLE={Using the declarative language \lustre\ for circuit verification}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L11}, INSTITUTION = {IMAG, Grenoble}, MONTH = feb , YEAR = 1990 } @INPROCEEDINGS{thuau90, AUTHOR={G. Thuau and D. Pilaud}, TITLE={Using the declarative language \lustre\ for circuit verification}, BOOKTITLE={Workshop on Designing Correct Circuits}, address={Oxford}, MONTH = sep, YEAR = 1990 } @TECHREPORT{bayol89a, AUTHOR={C. Bayol and J.L. Paillet}, TITLE={TACHE : a TAutology CHEcker for the P$-$Calculus}, TYPE={\researchreport\ }, NUMBER={89-07}, INSTITUTION={Univerist\'{e} de Provence}, MONTH=jun , YEAR= 1989 } @INPROCEEDINGS{bayol89b, AUTHOR={C. Bayol and J.L. Paillet}, TITLE={Using TACHE for proving circuits}, BOOKTITLE={ IMEC-IFIP Internation Workshop ``Applied Formal Methods for Correct VLSI Designs''}, ADDRESS={Leuven}, MONTH=nov , YEAR= 1989 } @INPROCEEDINGS{borrione87b, AUTHOR={D. Borrione and J.L. Paillet }, TITLE={Preuve formelle et simulation \`{a} partir d'une description {CASCADE}: Techniques compl\'{e}mentaires pour la validation de circuits}, BOOKTITLE={16th IASTED International Conference: Identification, Modelling and Simulation}, ADDRESS={Paris}, MONTH=jun , YEAR= 1987 } @INPROCEEDINGS{borrione89, AUTHOR={D. Borrione and A. Salem}, TITLE={Proving an on-line multiplier with {OBJ3} and {TACHE}: a practical experience}, BOOKTITLE={IMEC-IFIP Internation Workshop ``Applied Formal Methods for Correct VLSI Designs''}, ADDRESS={Leuven}, MONTH=nov , YEAR= 1989 } @TECHREPORT{collavizza87, AUTHOR={H. Collavizza}, TITLE={Etude de la v\'{e}rification logico-temporelle des circuits digitaux synchrones et r\'{e}alisation d'un logiciel en {Prolog II}}, TYPE={M\'{e}moire de DEA de math\'{e}matiques appliqu\'{e}es}, INSTITUTION={Universit\'{e} de Provence}, MONTH=jun , YEAR=1987 } @TECHREPORT{collavizza88a, AUTHOR={H. Collavizza}, TITLE={Evaluation des techniques de r\'{e}\'{e}criture pour la preuve formelle des circuits digitaux : exp\'{e}rimentation du logiciel {REVE}}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~88-01}, MONTH=may , YEAR = 1988 } @TECHREPORT{collavizza88b, AUTHOR={H. Collavizza and L. Pierre}, TITLE={Formal Verification of Hardware using {OBJ} and the {Boyer \& Moore} Theorem Prover : a practical Comparison}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~88-04}, MONTH=oct , YEAR = 1988 } @TECHREPORT{collavizza89b, AUTHOR={H. Collavizza}, TITLE={Mod\'{e}lisation du microprocesseur MTI : le niveau microprogramme}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~89-06}, MONTH=may , YEAR = 1989 } @TECHREPORT{paillet90, AUTHOR={J.L. Paillet}, TITLE={Alg\`{e}bres de fonctions: propri\'{e}t\'{e}s logiques et preuves de circuits digitaux}, TYPE={ M\'{e}moire d'Habilitation \`{a} diriger des recherches}, INSTITUTION={Universit\'{e} de Provence}, MONTH=feb, YEAR=1990 } @TECHREPORT{pierre88, AUTHOR={L. Pierre}, TITLE={Pr\'{e}sentation du d\'{e}monstrateur de th\'{e}or\`{e}mes de {Boyer \& Moore} et \'{e}valuation pr\'{e}liminaire en vue de la preuve de circuits}, TYPE={\researchreport\ }, INSTITUTION={MAIUP}, NUMBER={\mynumber~88-03}, MONTH=sep , YEAR = 1988 } @INPROCEEDINGS{pierre89b, AUTHOR={L. Pierre}, TITLE={An Evaluation of the {Boyer \& Moore} Theorem Prover for the Formal Proof of Sequential Circuits}, BOOKTITLE={17th IASTED International Conference on Simulation and Modelling}, MONTH=jun , ADDRESS={Lugano, Suisse}, YEAR=1989 } @INPROCEEDINGS{pierre89c, AUTHOR={L. Pierre}, TITLE={The Formal Proof of Sequential Circuits described in {CASCADE} using the {Boyer-Moore} Theorem Prover}, BOOKTITLE={IMEC-IFIP Internation Workshop ``Applied Formal Methods for Correct VLSI Designs''}, ADDRESS={Leuven}, MONTH=nov , YEAR= 1989 } @INPROCEEDINGS{salem90, AUTHOR={A. Salem and D. Borrione}, TITLE={Automatic Proof of bit-level {VHDL} Descriptions with {TACHE}}, BOOKTITLE={VHDL Forum for CAD in Europe, Spring'90 meeting}, ADDRESS={Munich}, MONTH=may , YEAR= 1990 } @TECHREPORT{L15, AUTHOR = {N. Halbwachs and F. Lagnier}, TITLE = {S\'{e}mantique statique du langage Lustre - Version 3}, TYPE = {\techreport\ }, NUMBER = {SPECTRE L15}, INSTITUTION = {IMAG, Grenoble}, MONTH = feb , YEAR = 1991 } @TECHREPORT{maraninchi90, AUTHOR={F. Maraninchi}, TITLE={Argos, un langage graphique pour la conception, la description et la validation des syst\`{e}mes r\'{e}actifs}, TYPE = {\Thesis}, INSTITUTION = {Universit\'{e} Joseph Fourier, Grenoble}, YEAR = 1990 } @INPROCEEDINGS{maraninchi89, AUTHOR={F. Maraninchi}, TITLE={Argonaute: graphical description, semantics and verification of reactive systems by using a process algebra}, BOOKTITLE = {International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, YEAR = {1989} } @TECHREPORT{sorel, AUTHOR ={N. Ghezal and S. Matiatos and P. Piovezan and Y. Sorel and M. Sorine}, TITLE= {{\sc Syndex}, un environnement de programmation pour multi-processeur de traitement du signal. {M}\'{e}canismes de communication}, TYPE = {\techreport\ }, INSTITUTION={INRIA Rocquencourt, France}, NUMBER={1236}, YEAR = 1990 } @INPROCEEDINGS{kurshan89, AUTHOR={R. P. Kurshan and K McMillan}, TITLE={A structural induction theorem for processes}, BOOKTITLE={8th ACM Symposium on Principles of Distributed Computing}, ADDRESS={Edmonton (Alberta)}, MONTH=aug , YEAR={1989}, PAGES={239--247} } @INPROCEEDINGS{sistla87, AUTHOR={A. P. Sistla and S. M. German}, TITLE={Reasoning with many processes}, BOOKTITLE={Symp. on Logic in Computer Science, Ithaca}, MONTH=jun , YEAR={1987}, PAGES={138--152} } @INPROCEEDINGS{clarke86a, AUTHOR={E. M. Clarke and O. Grumberg and M. C. Browne}, TITLE={Reasonning about networks with many identical finite-state processes}, BOOKTITLE={5th ACM Symposium on Principles of Distributed Computing, Calgary (Alberta)}, MONTH=aug , YEAR={1986}, PAGES={240--248} } @inproceedings{henzinger92, Author = { T. Henzinger and X. Nicollin and J. Sifakis and S. Yovine } , title = { Symbolic Model-Checking for Real-Time Systems } , booktitle = { {LICS}'92 }, year = { 1992 } , month = jun } } @TECHREPORT{fernandez88, AUTHOR = {J.-C. Fernandez}, TITLE={Alde'baran, un syste`me de ve'rification par re'duction de processus communicants}, TYPE = {\Thesis}, INSTITUTION = {Universite' Joseph Fourier, Grenoble}, MONTH = may , YEAR = {1988} } @INPROCEEDINGS{fernandez85a, AUTHOR = {J.-C. Fernandez and J.L. Richier and J. Voiron}, TITLE ={Verification of Protocols Specifications using the \cesar\ system}, BOOKTITLE = {IFIP Workshop on protocols}, ADDRESS = {Toulouse}, MONTH = jun , YEAR = {1985} } @TECHREPORT{rasse90, AUTHOR = {A. Rasse}, TITLE={CLEO : diagnostic des erreurs en Xesar}, TYPE = {These}, INSTITUTION= {Institut National Polytechnique, Grenoble}, MONTH = jun , YEAR = {1990} } @TECHREPORT{richier87a, AUTHOR = {J.L. Richier and C Rodriguez and J. Sifakis and J. Voiron}, TITLE={\xesar\ User's Guide }, TYPE = {Rapport Technique Spectre C6}, INSTITUTION= {LGI/IMAG, Grenoble}, MONTH = sep , YEAR = {1987} } @TECHREPORT{rodriguez88a, AUTHOR = {C. Rodriguez}, TITLE={Sp\'ecification et validation de syst\`emes en \xesar}, TYPE = {\Thesis}, INSTITUTION = {Institut National Polytechnique, Grenoble}, MONTH = may , YEAR = {1988} } @INPROCEEDINGS{berthet90, AUTHOR = {C. Berthet and O. Coudert and J. C. Madre}, TITLE={ New ideas on symbolic manipulations of finite state machines}, BOOKTITLE={International Conference on Computer Design (ICCD), Cambridge}, MONTH=sep , YEAR= 1990 } @ARTICLE{brayton90, AUTHOR={R. K. Brayton and G. D. Hachtel and A. L. Sangiovanni-{V}incentelli}, TITLE={Multilevel Logic Synthesis}, JOURNAL={Proceedings of the IEEE}, VOLUME= 78, NUMBER = 2, MONT= feb , YEAR = 1990 } @INPROCEEDINGS{coudert90a, AUTHOR={O. Coudert and J. C. Madre}, TITLE={A unified framework for the formal verification of sequential circuits}, BOOKTITLE={International Conference on Computer Aided Design (ICCAD), Santa Clara}, YEAR= 1990 } @INPROCEEDINGS{touati90, AUTHOR={H. Touati and H. Savoj and B. Lin and R. K. Brayton and A. Sangiovanni-Vincentelli}, TITLE={Implicit state enumeration of finite state machines using {BDD}s}, BOOKTITLE={International Conference on Computer Aided Design (ICCAD)}, MONTH=nov , YEAR= 1990 } @INPROCEEDINGS{savoj91, AUTHOR={H. Savoj and H. Touati and R. K. Brayton}, TITLE={The use of image computation techniques in extracting local don't cares and network optimization}, BOOKTITLE={International Conference on Computer Aided Design (ICCAD)}, MONTH=nov , YEAR= 1991 } @ARTICLE{apt86, AUTHOR={K. R. Apt and D. C. Kozen}, TITLE={Limits for automatic verification of finite-state concurrent systems}, JOURNAL={Information Processing Letters}, VOLUME= 22, YEAR=1986, PAGES={307--309} } @ARTICLE{suzuki88, AUTHOR={I. Suzuki}, TITLE={Proving properties of a ring of finite-state machines}, JOURNAL={Information Processing Letters}, VOLUME= 28, YEAR=1988, PAGES={213--214} } @TECHREPORT{rocheteau:these, AUTHOR = {F. Rocheteau}, TITLE = {Extension du langage {Lustre} et application \`a la conception de circuits: Le langage {Lustre-V4} et le syst\`eme {Pollux}}, TYPE = {\Thesis}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH=jun , YEAR = {1992} } @TECHREPORT{ratel:these, AUTHOR = {C. Ratel}, TITLE = {D\'efinition et r\'ealisation d'un outil de v\'erification formelle de programmes {Lustre}: Le syst\`eme {Lesar}}, TYPE = {\Thesis}, INSTITUTION = {Universit\'e Joseph Fourier, Grenoble}, MONTH=jun , YEAR = {1992} } @INPROCEEDINGS{thuau:verif, AUTHOR ={G. Thuau and B. Berkane}, TITLE ={Using the language \lustre\ for Sequential Circuit Verification}, BOOKTITLE = {International Workshop on Designing Correct Circuits, Lingby (Denmark)}, MONTH = jan , YEAR = {1992}, } @INPROCEEDINGS{girault92, AUTHOR = {A. Girault and P. Caspi }, TITLE = {An algorithm for distributing a finite transition system on a shared/distributed memory system}, BOOKTITLE = {PARLE'92, Paris}, MONTH = { July}, YEAR = {1992} } @ARTICLE{cousot92, AUTHOR={P. Cousot and R. Cousot}, TITLE={Abstract interpretation and application to logic programs}, JOURNAL={Journal of Logic Programming}, VOLUME={13}, NUMBER={1--4}, PAGES={103--179}, YEAR=1992, NOTE={(Also, \researchreport\ LIX/RR/92/08, Ecole Polytechnique)} } @INPROCEEDINGS{cousot92b, AUTHOR={P. Cousot and R. Cousot}, TITLE={Comparing the {G}alois connection and widening/narrowing approaches to abstract interpretation}, BOOKTITLE = {PLILP'92}, PUBLISHER = {LNCS 631, Springer Verlag}, EDITOR={M. Bruynooghe and M. Wirsing}, ADDRESS = {Leuven (Belgium)}, MONTH=jan, YEAR=1992 } @INPROCEEDINGS{cousot95, AUTHOR={ P. Cousot and R. Cousot}, TITLE={Formal languages, grammar and set-constraint-based program analysis by abstract interpretation}, BOOKTITLE = {ACM Conference on Functional Programming and Computer Architecture, FPCA'95}, ADDRESS = {La Jolla (Cal)}, MONTH = jun, YEAR= 1995 } @ARTICLE{cherni68, AUTHOR={N. V. Chernikova}, TITLE={Algorithm for discovering the set of all solutions of a linear programming problem}, JOURNAL={U.S.S.R. Computational Mathematics and Mathematical Physics}, VOLUME= 8, NUMBER= 6, PAGES={282--293}, YEAR= 1968 } @TECHREPORT{leverge, AUTHOR={H. {LeVerge}}, TITLE={A note on {C}hernikova's Algorithm}, TYPE={\researchreport\ }, NUMBER = 635, INSTITUTION={IRISA}, MONTH= feb , YEAR=1992 } @TECHREPORT{wilde93, AUTHOR={D. K. Wilde}, TITLE={A library for doing polyhedral operations}, TYPE={\researchreport\ }, NUMBER = 785, INSTITUTION={IRISA}, MONTH= dec , YEAR=1993 } @TECHREPORT{berkane92, AUTHOR = {B. Berkane}, TITLE={V\'erification des syst\`emes mat\'eriels num\'eriques s\'equentiels synchrones~: Application du langage \lustre\ et de l'outil de v\'erification {Lesar}}, Institution = {Institut Polytechnique de Grenoble}, TYPE = {\Thesis }, MONTH = oct , YEAR = {1992} } @BOOK{mybook, AUTHOR={N. Halbwachs}, TITLE={Synchronous programming of reactive systems}, PUBLISHER={Kluwer Academic Pub.}, YEAR={1993} } @article{peterson77, author={J. L. Peterson}, title={Petri nets}, journal={ACM Computing Surveys}, volume={9}, number={3}, year=1977, pages={223--252} } @article{chaochen91, author={Z. Chaochen and C.A.R. Hoare and A.P. Ravn}, title={A calculus of durations}, journal={Information Processing Letters}, volume={40}, pages={269--276}, year=1991 } @inproceedings{vdbeek94, author = {M. von der Beeck}, title = {A Comparison of {S}tatecharts Variants}, booktitle = {FTRTFT}, publisher = {LNCS 863, Springer Verlag}, year = 1994 } @INPROCEEDINGS{hoffman92, AUTHOR={G. Hoffmann and H. Wong-Toi}, TITLE={Symbolic Synthesis of supervisory controllers}, BOOKTITLE={American Control Conference, Chicago}, MONTH=jun , YEAR= 1992 } @ARTICLE{ramadge89, AUTHOR={P. J. Ramadge and W. M. Wonham}, TITLE={The control of discrete event systems}, JOURNAL={Proceedings of the IEEE}, VOLUME = {77}, NUMBER= {1}, MONTH= jan , YEAR= 1989 } @ARTICLE{ramadge87, AUTHOR={P. J. Ramadge and W. M. Wonham}, TITLE={Supervisory control of a class of discrete event processes}, JOURNAL={SIAM J. Control and Optimization}, VOLUME={25}, NUMBER={1}, MONTH=jan , YEAR= 1987 } @INPROCEEDINGS{pnueli92, AUTHOR={A. Pnueli}, TITLE={How vItal is liveness? {V}erifying timing properties of reactive and hybrid systems}, BOOKTITLE={CONCUR'92, Stony Brook}, PUBLISHER={LNCS 630, Springer Verlag}, MONTH=aug , YEAR= 1992 } @INPROCEEDINGS{polys, AUTHOR={N. Halbwachs}, TITLE={Delay analysis in synchronous programs}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @INPROCEEDINGS{islip93, AUTHOR={N. Halbwachs and J.-C. Fernandez and A. Bouajjanni}, TITLE={An executable temporal logic to express safety properties and its connection with the language \lustre}, BOOKTITLE={Sixth International Symp. on Lucid and Intensional Programming, ISLIP'93, Quebec}, MONTH=apr , YEAR= 1993 } @INPROCEEDINGS{amast93, AUTHOR={N. Halbwachs and F. Lagnier and P. Raymond}, TITLE={Synchronous observers and the verification of reactive systems}, BOOKTITLE={Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93}, ADDRESS={Twente}, MONTH=jun , EDITOR={M. Nivat and C. Rattray and T. Rus and G. Scollo}, PUBLISHER={Workshops in Computing, Springer Verlag}, YEAR=1993 } @ARTICLE{bartlett88, AUTHOR={K. A. Bartlett and R. K. Brayton and G. D. Hachtel and R. M. Jacoby and R. Rudell and A. Sangiovanni-Vincentelli and A. Wang}, TITLE={Multilevel Logic Minimization using implicit don't cares}, JOURNAL={IEEE Transactions on CAD/ICAS}, VOLUME={CAD-7}, NUMBER= 6, PAGES={723--739}, MONTH=jun , YEAR= 1988 } @TECHREPORT{damiani92, AUTHOR={M. Damiani and G. DeMicheli}, TITLE={Don't care set specifications in combinational and synchronous logic circuits}, TYPE={\techreport\ }, INSTITUTION={Computer Systems Laboratory, Stanford University}, NUMBER={CSL-TR-92-531}, YEAR=1992 } @ARTICLE{josephs92, AUTHOR={M. B. Josephs}, TITLE={Receptive Process Theory}, JOURNAL={Acta Informatica}, VOLUME= 29, MONTH=feb , YEAR= 1992 } @PHDTHESIS{corbett92a, AUTHOR={J. C. Corbett}, TITLE={Automated formal analysis methods for concurrent and real-time software}, SCHOOL={Univ. of Massachusetts at Amherst}, YEAR=1992 } @INPROCEEDINGS{corbett92, AUTHOR={J. C. Corbett}, TITLE={Verifying general safety and liveness properties with integer programming}, BOOKTITLE={4th Int. Workshop on Computer Aided Verification, Montreal}, EDITOR={G. Bochmann}, YEAR=1992 } @INPROCEEDINGS{irigoin91, AUTHOR={F. Irigoin and P. Jouvelot and R. Triolet}, TITLE={Semantical Interprocedural parallelization: An overview of the {PIPS} Project}, BOOKTITLE={ACM Int. Conf. on Supercomputing, ICS'91, K\"oln}, YEAR= 1991 } @INPROCEEDINGS{macii92, AUTHOR={E. Macii and B. Plessier and F. Somenzi}, TITLE={Verification of systems containing counters}, BOOKTITLE={ICCAD'92}, YEAR= 1992 } @INPROCEEDINGS{devadas91, AUTHOR={S. Devadas and K. Kreutzer and A. S. Krishnakumar}, TITLE={Design verification ansd reachability analysis using algebraic manipulation}, BOOKTITLE={ICCD'91}, YEAR= 1991, } @INPROCEEDINGS{jourdan93, AUTHOR={M. Jourdan and F. Maraninchi and A. Olivero}, TITLE={Verifying quantitative real-time properties of synchronous programs}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @INPROCEEDINGS{maraninchi92, AUTHOR={F. Maraninchi}, TITLE={Operational and compositional semantics of synchronous automaton compositions}, BOOKTITLE={CONCUR'92}, ADDRESS={Stony Brook}, PUBLISHER={LNCS 630, Springer Verlag}, MONTH=aug , YEAR= 1992 } @INPROCEEDINGS{murphi, AUTHOR={D. Dill and A. J. Drexler and A. J. Hu and C. H. Yang}, TITLE={Protocol verification as a hardware design aid}, BOOKTITLE= {1992 IEEE Int. Conference on Computer Design: VLSI in Computers and Processors}, YEAR= 1992 } @INPROCEEDINGS{kurshan93, AUTHOR={R. P. Kurshan and L. Lamport}, TITLE={Verification of a multiplier: 64 bits and beyond}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @INPROCEEDINGS{kurshan90, AUTHOR={R. P. Kurshan}, TITLE={Analysis of discrete event coordination}, BOOKTITLE= {REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness}, EDITOR={J.W. de Bakker and W.-P. de Roever and G. Rozemberg}, PUBLISHER={LNCS 430, Springer Verlag}, MONTH=may , YEAR=1989 } @INPROCEEDINGS{abadi89a, AUTHOR={M. Abadi and L. Lamport}, TITLE={Composing specifications}, BOOKTITLE= {REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness}, EDITOR={J.W. de Bakker and W.-P. de Roever and G. Rozemberg}, PUBLISHER={LNCS 430, Springer Verlag}, MONTH=may , YEAR=1989 } @INPROCEEDINGS{josko87, AUTHOR = {B. Josko}, TITLE = {{MCTL - An extension of CTL for modular verification of concurrent systems}}, BOOKTITLE = {Workshop on Temporal Logic in Specification, Manchester}, PUBLISHER = {LNCS 398, Springer Verlag}, YEAR = 1987 } @INPROCEEDINGS{hu93, AUTHOR={A. J. Hu and D. L. Dill}, TITLE={Efficient verification with {BDD}s using implicitly conjuncted invariants}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @ARTICLE{karr76, AUTHOR={M. Karr}, TITLE={Affine relationships among variables of a program}, JOURNAL={Acta Informatica}, VOLUME= 6, PAGES={133--151}, YEAR=1976 } @ARTICLE{McNaughton66, AUTHOR={R. McNaughton}, TITLE={Testing and generating infinite sequences by a finite automaton}, JOURNAL={Information and Control}, VOLUME= 9, PAGES = {521--530}, YEAR = 1966 } @ARTICLE{Choueka74, AUTHOR={Y. Choueka}, TITLE={Theories of Automata on $\omega$-tapes: A simplified approach}, JOURNAL={J. Computer and System Sciences}, VOLUME= 8, PAGES = {117--141}, YEAR=1974 } @ARTICLE{Sistla87a, AUTHOR={A. P. Sistla and M. Y. Vardi and P. Wolper}, TITLE={The complementation problem for B\"uchi automata with applications to temporal logic}, JOURNAL={Theoretical Computer Science}, VOLUME = 49, PAGES = {217--237}, YEAR = 1987 } @INPROCEEDINGS{Safra88, AUTHOR={S. Safra}, TITLE={On the complexity of $\omega$-automata}, BOOKTITLE={29th IEEE Symp. on Foundations of Computer Science}, PAGES={319--327}, YEAR=1988 } @BOOK{arnold92, AUTHOR={A. Arnold}, TITLE={Syst\`emes de transitions finis et s\'emantique des processus communicants}, PUBLISHER={Masson}, YEAR=1992 } @INBOOK{thomas90, AUTHOR={W. Thomas}, TITLE={Automatas on infinite objects}, BOOKTITLE={Handbook of theoretical computer science}, PUBLISHER={Elsevier Science Pub.}, PAGES={134--191}, YEAR=1990 } @TECHREPORT{perrin91, AUTHOR={D. Perrin and J.-E. Pin}, TITLE={Mots infinis}, Institution={LITP}, TYPE={\researchreport\}, NUMBER={91.06}, MONTH=jan , YEAR=1991 } @ARTICLE{alpern85, AUTHOR={B. Alpern and F. B. Schneider}, TITLE={Defining Liveness}, JOURNAL={Information Processing Letters}, VOLUME= 21, PAGES={181--185}, YEAR=1985 } @TECHREPORT{alpern86, AUTHOR={B. Alpern}, TITLE={Constructing proof obligations}, TYPE={PhD. Thesis}, Institution={Cornell University}, YEAR=1986 } @ARTICLE{graf86b, AUTHOR = {S. Graf and J. Sifakis}, TITLE = {A Modal Characterization of Observational Congruence on Finite Terms of {CCS}}, JOURNAL = {Information and Control}, VOLUME = {68}, PAGE = {1--3}, YEAR = {1986} } @INPROCEEDINGS{bouajjani91, AUTHOR = {A. Bouajjani and J.-C. Fernandez and S. Graf and C. Rodriguez and J. Sifakis}, TITLE = {Safety for Branching Time Semantics}, BOOKTITLE = {18th ICALP}, PUBLISHER = {LNCS 510, Springer Verlag}, MONTH = jul , YEAR = {1991} } @ARTICLE{lamport77, AUTHOR={L. Lamport}, TITLE={Proving the correctness of multiprocess programs}, JOURNAL={IEEE Transactions on Software Engineering}, VOLUME={SE-3}, NUMBER=2, PAGES={125--143}, YEAR=1977 } @ARTICLE{alpern87, AUTHOR={B. Alpern and F. B. Schneider}, TITLE={Recognizing safety and liveness}, JOURNAL={Distributed Computing}, VOLUME=2, PAGES={117--126}, YEAR=1987 } @INPROCEEDINGS{abadi88, AUTHOR={M. Abadi and L. Lamport}, TITLE={The existence of refinement mappings}, BOOKTITLE={3rd Symp. on Logics in Computer Science}, YEAR=1988 } @INPROCEEDINGS{floyd87, AUTHOR={R. W. Floyd}, TITLE={Assigning meaning to programs}, BOOKTITLE={Symp. on Applied Mathematics, American Matematical Society, nr. 19}, YEAR=1967 } @ARTICLE{dijkstra75, AUTHOR={E. W. Dijkstra}, TITLE={Guarded commands, non determinacy and formal derivation of programs}, JOURNAL={CACM}, VOLUME=18, NUMBER=8, Month=aug, YEAR=1975 } @BOOK{dijkstra76, AUTHOR={E. W. Dijkstra}, TITLE={A Discipline of Programming}, PUBLISHER={Prentice-Hall Series in Automatic Computation}, YEAR=1976 } @ARTICLE{hoare69, AUTHOR={C.A.R. Hoare}, TITLE={An axiomatic approach to computer programming}, JOURNAL={CACM}, VOLUME=12, NUMBER=10, MONTH=oct , YEAR=1969 } @ARTICLE{owicki76, AUTHOR={S. Owicki and D. Gries}, TITLE={An axiomatic proof technique for parallel programs}, JOURNAL={Acta Informatica}, VOLUME=6, PAGES={319--340}, YEAR=1976 } @ARTICLE{lamport80, AUTHOR={L. Lamport}, TITLE={The ``{H}oare Logic'' of concurrent programs}, JOURNAL={Acta Informatica}, VOLUME=14, PAGES={21--37}, YEAR=1980 } @TECHREPORT{synchrone, AUTHOR={J.-P. Paris and G. Berry and F. Mignard and Ph. Couronn\'e and P. Caspi and N. Halbwachs and Y. Sorel and A. Benveniste and Th. Gautier and P. Le~Guernic and F. Dupont and C. Le~Maire}, TITLE={Projet {SYNCHRONE}, Les formats communs des langages synchrones}, TYPE={Rapport Technique}, INSTITUTION={INRIA}, NUMBER=157, MONTH=jun , YEAR = 1993 } @TECHREPORT{synchron, AUTHOR={J.-P. Paris and G. Berry and F. Mignard and Ph. Couronn\'e and P. Caspi and N. Halbwachs and Y. Sorel and A. Benveniste and Th. Gautier and P. Le~Guernic and F. Dupont and C. Le~Maire}, TITLE={{SYNCHRON} project, Common formats of synchronous languages}, TYPE={Technical Report}, MONTH={July }, YEAR = 1993 } @INPROCEEDINGS{benveniste93, AUTHOR={A. Benveniste and P. Caspi and P. Le~Guernic and N. Halbwachs}, TITLE={Data-flow synchronous languages}, BOOKTITLE={{\sc Rex} Symposium ``Ten Years of Concurrency, Reflections and Perspectives''}, PUBLISHER={LNCS 803, Springer-Verlag}, MONTH=jun , YEAR=1993 } @INPROCEEDINGS{caspi93, AUTHOR={P. Caspi}, TITLE={Lucid {S}ynchrone}, BOOKTITLE={International Workshop on Principles of Parallel Computing (OPOPAC)}, MONTH=nov , YEAR=1993 } @inproceedings{fernandez93, author = {J.-C. Fernandez and A. Kerbrat and L. Mounier}, title = {Symbolic Equivalence Checking}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @INPROCEEDINGS{fernandez93a, AUTHOR={J. Cl. Fernandez}, TITLE={Abstract Interpretation and Verification of Reactive Systems}, BOOKTITLE = {Static Analysis}, MONTH = sep , PUBLISHER={LNCS 724, Springer Verlag}, YEAR = {1993} } @INPROCEEDINGS{graf93, author = {S. Graf and C. Loiseaux}, title = {A tool for symbolic program verification and abstraction}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @TECHREPORT{sergio:these, AUTHOR = {S. Yovine}, TITLE = {M\'ethodes et outils pour la v\'erification symbolique de syst\`emes temporis\'es}, TYPE = {Th\`ese}, INSTITUTION = {Institut National Polytechnique de Grenoble}, MONTH = may , YEAR = {1993} } @INPROCEEDINGS{emerson86, AUTHOR={E. A. Emerson and C.-L. Lei}, TITLE={Efficient model checking in fragments of the propositional $\mu$-calculus}, BOOKTITLE={Symp. on Logic in Computer Science}, PAGES={276--278}, YEAR=1986 } @INPROCEEDINGS{cleaveland91, AUTHOR={R. Cleaveland and B. Steffen}, TITLE={Computing behavioural relations, logically}, BOOKTITLE={18th ICALP}, PUBLISHER = {LNCS 510, Springer Verlag}, PAGES={127--138}, YEAR=1991 } @INPROCEEDINGS{coudert89a, AUTHOR={O. Coudert and C. Berthet and J. C. Madre}, TITLE={Verification of sequential machines using Boolean functional vectors}, BOOKTITLE={Formal VLSI Correctness Verification}, EDITOR={L. J. M. Claesen}, PUBLISHER={North-Holland}, MONTH=nov , YEAR=1989 } @article{lamport87, AUTHOR={L. Lamport}, TITLE={A fast mutual exclusion algorithm}, JOURNAL={ACM Transactions on Computer Systems}, VOLUME=5, NUMBER=1, PAGES={1--11}, YEAR=1987 } @inproceedings{yanakakis93, author={M. Yanakakis and D. Lee}, title={An efficient algorithm for minimizing real-time transition systems}, BOOKTITLE= {Fifth Conference on Computer-Aided Verification, CAV'93}, address={Elounda (Greece)}, PUBLISHER = {LNCS 697, Springer Verlag}, MONTH=jul , YEAR=1993 } @UNPUBLISHED{approx, author={N. Halbwachs and D. Dill and A. Hu}, title={On the use of approximation in symbolic model-checking}, note={\inpreparation} } @TECHREPORT{tiger, author={O. Coudert and J.-C. Madre and H. Touati}, title={{TiGeR} Version 1.0 User Guide}, institution={Digital Paris Research Laboratory}, month=nov , year=1993 } @TECHREPORT{blif, key={Blif90}, title={{Blif-MV}: An Interchange Format for Design Verification and Synthesis}, Institution={Berkeley~Logic~Synthesis~Group}, year=1990 } @ARTICLE{harel89, TITLE={Using {S}tatecharts for hardware description and synthesis}, AUTHOR={D. Drusinsky and D. Harel}, JOURNAL={IEEE Trans. on Computer-Aided Design}, VOLUME= 8, NUMBER= 7, MONTH=jul , YEAR= 1989, PAGES={798--807} } @INPROCEEDINGS{malik93, author={S. Malik}, title={Analysis of cyclic combinational circuits}, booktitle={ICCAD'93}, address={Santa Clara (Ca)}, year= 1993 } @TECHREPORT{Hui91, AUTHOR = {C. Huizing}, TITLE={Semantics of reactive systems: comparison and full abstraction}, INSTITUTION= {Eindhoven University}, TYPE = {\thesis\ }, YEAR = {1991} } @BOOK{brown, Author={F. M. Brown}, Title={Boolean Reasoning: The logic of Boolean Equations}, Publisher={Kluwer Academic Publishers}, year= 1990 } @Article{kautz, Author={W. H. Kautz}, Title={The necessity of closed loops in minimal combinatorial circuits}, Journal={IEEE Trans. on Computers}, Pages={162--164}, Year= 1970 } @inproceedings{stok, author={L. Stok}, title={False loops through resource sharing}, booktitle={ICCAD'92}, address={Santa Clara (Ca)}, year= 1992 } @inproceedings{achh93, author={R. Alur and C. Courcoubetis and T. A. Henzinger and Pei-Hsin Ho}, title={Hybrid automata: an algorithmic approach to the specification and analysis of hybrid systems}, booktitle={Workshop on Theory of Hybrid Systems}, publisher={LNCS 736, Springer Verlag}, address={Lyngby, Denmark}, month=oct, year=1993 } @inproceedings{ahh93, author={R. Alur and T. A. Henzinger and Pei-Hsin Ho}, title={Automatic symbolic verification of embedded systems}, booktitle={RTTS93}, year=1993} @inproceedings{kpsy93, author={Y. Kesten and A. Pnueli and J. Sifakis and S. Yovine}, title={Integration graphs: a class of decidable hybrid systems}, booktitle={Workshop on Theory of Hybrid Systems}, publisher={LNCS 736, Springer Verlag}, year=1993, address={Lyngby, Denmark}, month=oct } @inproceedings{nosy92, author={X. Nicollin and A. Olivero and J. Sifakis and S. Yovine}, title={An approach to the description and analysis of hybrid systems}, booktitle={Workshop on Theory of Hybrid Systems}, publisher={LNCS 736, Springer Verlag}, year=1993, address={Lyngby, Denmark}, month=oct } @inproceedings{mmp91, author={O. Maler and Z. Manna and A. Pnueli}, title={From timed to hybrid systems}, booktitle={{\sc Rex} Workshop on Real-Time: Theory in Practice}, address={DePlasmolen (Netherlands)}, PUBLISHER={LNCS 600, Springer Verlag}, MONTH = jun , YEAR= {1991} } @inproceedings{henzinger94, author={T. A. Henzinger and P.-H. Ho}, title={Model checking strategies for hybrid systems}, booktitle={Conference on Industrial Applications of Artificial Intelligence and Expert Systems}, year=1994 } @inproceedings{dill93, author={H. Wong-Toi and D. Dill}, title={Using iterative approximations for timing verification}, booktitle={First AMAST International Workshop on Real-Time Systems}, address={Iowa City (Iowa)}, month=nov , year=1993 } @inproceedings{halbwachs94a, author={N. Halbwachs and F. Maraninchi}, title={On the symbolic analysis of combinational loops in circuits and synchronous programs}, booktitle={Euromicro'95}, address={Como (Italy)}, month=sep , year= 1995 } @inproceedings{halbwachs94b, author={N. Halbwachs and Y.-E. Proy and P. Raymond}, title={Verification of linear hybrid systems by means of convex approximations}, booktitle={International Symposium on Static Analysis, SAS'94}, editor = {B. {LeCharlier}}, publisher = {LNCS 864, Springer Verlag}, address = {Namur (Belgium)}, month = sep , year= 1994 } @inproceedings{halbwachs94c, author={N. Halbwachs}, title={About synchronous programming and abstract interpretation}, booktitle={International Symposium on Static Analysis, SAS'94}, editor = {B. {LeCharlier}}, publisher = {LNCS 864, Springer Verlag}, address = {Namur (Belgium)}, month = sep , year= 1994 } @article{halbwachs98, author={N. Halbwachs}, title={About synchronous programming and abstract interpretation}, journal={Science of Computer Programming,Special Issue on SAS'94}, editor={P. Cousot and B. Le Charlier}, volume= 31, number= 1, month= may , year=1998 } @inproceedings{masdupuy93, author={F. Masdupuy}, title={Semantic analysis of interval congruences}, booktitle={Int. Conf. on Formal Methods in Programming and their Applications}, publisher={LNCS, Springer Verlag}, month=jul , year=1993 } @article{wegbreit75, author={B. Wegbreit}, title={Property extraction in well-founded property sets}, journal={IEEE Trans. on Software Engineering}, volume={SE-1}, number=3, pages={270--285}, month=sep , year=1975 } @article{granger89, author={P. Granger}, title={Static analysis of arithmetical congruences}, journal={International Journal on Computer Mathematics}, volume=30, pages={165--190}, year=1989 } @inproceedings{cousot76, author={P. Cousot and R. Cousot}, title={Static determination of dynamic properties of programs}, booktitle={2nd Int. Symp. on Programming}, publisher={Dunod, Paris}, year=1976 } @unpublished{gas:amir, author = {A. Pnueli}, title={Case study: Generalized gas burner}, note={REACT common case studies, unpublished}, month=jun , year=1994 } @article{tcs95, author={R.~Alur and C.~Courcoubetis and N.~Halbwachs and T.~Henzinger and P.~Ho and X.~Nicollin and A.~Olivero and J.~Sifakis and S.~Yovine}, title={The Algorithmic Analysis of Hybrid Systems}, journal={Theoretical Computer Science B}, volume=138, pages={3--34}, month=jan , year=1995 } @techreport{dret94, author={F. Lagnier and P. Raymond and Ch. Dubois}, title={V\'erification de propri\'et\'es de programmes {SAGA/LUSTRE}}, type={Rapport final du contrat n$^0$ 92~34~463~00~470~7501}, institution={DRET}, month=jul , year=1994 } @techreport{dea:lesens, title={Synth\`ese de programmes r\'eactifs}, author={D. Lesens}, type = {\DEA}, institution = {Ecole Polytechnique}, month = jul , year=1994 } @inproceedings{lesar:rts95, author={Ch. Dubois and P. Ghaleb and F. Lagnier and P. Raymond}, title={V\'erification de propri\'et\'es de programmes \'ecrits en {Lustre}}, booktitle={RTS'95}, address={Paris}, month=jan , year= 1995 } @ARTICLE{graf84, author={S. Graf}, title={On {L}amport's comparison between linear and branching time temporal logic}, journal={R.A.I.R.O. Informatique Th\'eorique}, volume=18, number=4, year=1984, pages={345--353} } @ARTICLE{emerson86a, author={E. A. Emerson and J. Y. Halpern}, title={``{S}ometimes'' and ``{N}ot {N}ever'' revisited: on branching versus linear time temporal logic}, journal={JACM}, volume=33, number=1, month=jan , year=1986, pages={151--178} } @techreport{bac, author={N. Halbwachs}, title={{BAC}, A {B}oolean Automaton Checker}, type={Technical Report}, institution={Verimag Laboratory}, month=feb , year=1994 } @techreport{HR96, author={N. Halbwachs and P. Raymond}, title={On the use of approximation in symbolic model-checking}, type={Technical Report}, institution={Verimag Laboratory}, month=jan , year=1996 } @INPROCEEDINGS{causalesterel, author={T. R. Shiple and G. Berry and H. Touati}, title={Constructive Analysis of Cyclic Circuits}, booktitle={International Design and Testing Conference IDTC'96}, address={Paris, France}, year=1996 } @INPROCEEDINGS{ArgosLustre-ICCL94, AUTHOR = {M. Jourdan and F. Lagnier and P. Raymond and F. Maraninchi}, TITLE = {A Multiparadigm Language for Reactive Systems}, BOOKTITLE = {5th IEEE International Conference on Computer Languages }, ADDRESS = {Toulouse}, PUBLISHER = {IEEE Computer Society Press}, MONTH = may , YEAR = {1994} } @unpublished{irisagc1, author={P. Aubry and T. Gautier and P. {Le Guernic}}, title={Proposals for the evolution of the {GC} format}, note={Working Document}, month={January}, year=1995 } @INPROCEEDINGS{courcoubetis91, AUTHOR = {C. Courcoubetis and S. Graf and J. Sifakis}, TITLE={An Algebra for Boolean Processes}, BOOKTITLE = {Workshop on Computer-Aided Verification 91, Aalborg}, MONTH = jun , YEAR = {1991}, PUBLISHER = {LNCS Vol. 575} } @TECHREPORT{Lynch89b, AUTHOR = {N. A. Lynch and M. R. Tuttle}, TITLE={An Introduction to Input/Output Automata}, TYPE = {CWI-Quaterly}, INSTITUTION = {CWI, Amsterdam}, VOLUME = {2}, NUMBER = {3}, YEAR = {1989} } @INPROCEEDINGS{Caspi94, AUTHOR = {P. Caspi and A. Girault and D. Pilaud}, BOOKTITLE = {Seventh International Conference on Parallel and Distributed Computing Systems, PDCS'94}, PUBLISHER = {ISCA}, TITLE = {Distributing Reactive Systems}, ADDRESS = {Las Vegas, USA}, MONTH = oct , YEAR = {1994} } @INPROCEEDINGS{bergerand88, AUTHOR={J.~L. Bergerand and E. Pilaud}, TITLE={{\sc Saga}, a software environment for dependable automatic control}, BOOKTITLE={IFAC SAFECOMP'88}, ADDRESS={Fulda}, YEAR= 1988 } @INPROCEEDINGS{sayet90, AUTHOR={C. Sayet and E. Pilaud}, TITLE={An experience of a critical software development}, BOOKTITLE={Fault Tolerant Computing Symposium 20}, ADDRESS={Newcastle}, YEAR=1990 } @INPROCEEDINGS{lagnier95, AUTHOR={F. Lagnier and P. Raymond and C. Dubois}, TITLE={Formal verification of a critical system written in {\sc Saga/Lustre}}, BOOKTITLE={Workshop on Formal Methods, Modelling and Simulation for System Engineering}, ADDRESS={St Quentin en Yvelines (France)}, MONTH=feb , YEAR=1995 } @INPROCEEDINGS{nervia, AUTHOR={A. Boue and G. Clerc}, TITLE={{Nervia}: A local network for safety}, BOOKTITLE={IAEA Specialist Meeting on Communication and data transfer in Nuclear Power Plants}, ADDRESS={Lyon (France)}, EDITOR={CEA/EDF/Framatome}, MONTH=apr , YEAR={1990} } @inproceedings{sigali, author={M. {Le Borgne} and Bruno Dutertre and Albert Benveniste and Paul {Le Guernic}}, title={Dynamical Systems over {Galois} Fields}, booktitle={European Control Conference}, address={Groningen}, year=1993, pages={2191--2196} } @article{cacm:fundations, author={P. Caspi and A. Benveniste and P. {Le Guernic} and F. Maraninchi}, title={The fundamentals of reactive system synchronous programming}, journal={Communications of the ACM}, volume={\toappear\ }, year=1995 } @article{cacm:users, author={Y. Auffray and Th. Bravier and E. Ledinot and J.-L. Bergerand and Ch. Dubois and Ph. Beaufreton and A. Janvier}, title={Synchronous languages in the industry: Three experience reports}, journal={Communications of the ACM}, volume={\toappear\ }, year=1995 } @article{cacm:ssii, author={Ch. Bodennec and F. Dupont and C. {Le Maire} and A. Benveniste and G. Berry and R. {De Simone} and T. Gautier and N. Halbwachs}, title={Synchronous languages and reactive system design}, journal={Communications of the ACM}, volume={\toappear\ }, year=1995 } @article{cacm:ongoing, author={C2A-SYNCHRON}, title={Synchronous technology: a short term perspective}, journal={Communications of the ACM}, volume={\toappear\ }, year=1995 } @INPROCEEDINGS{Esterel:TouatiBerry, AUTHOR={H. Touati and G. Berry}, TITLE={Optimized Controlleur Synthesis Using {E}sterel}, BOOKTITLE={Proc. International Workshop on Logic Synthesis IWLS'93, Lake Tahoe}, YEAR={1993} } @INPROCEEDINGS{Esterel:Berry:Preemption, AUTHOR={G. Berry}, TITLE={Preemption and Concurrency}, BOOKTITLE={Proc. FSTTCS 93}, PUBLISHER={Springer-Verlag}, SERIES= {Lecture Notes in Computer Science 761}, PAGES={72-93}, YEAR=1993 } @INPROCEEDINGS{Esterel:CRP, AUTHOR={G. Berry and R. K. Shyamasundar and S. Ramesh}, TITLE={Communicating Reactive Processes}, BOOKTITLE={Proc. 20th ACM Conf. on Principles of Programming Languages, POPL'93}, ADDRESS={Charleston, Virginia}, YEAR=1993 } @UNPUBLISHED{baufreton94, author={ P. Baufreton and C. Olivier}, title={Exp\'erience de v\'erification de propri\'et\'es sur des sp\'ecifications syst\'emes de r\'egulation de moteur d'avion avec SILDEX}, note={Invited Talk at C2A Group, Paris}, month=jan , year=1994 } @TECHREPORT{horlacher, author={S. Horlacher}, title={Preuve de propri\'et\'es de {Grafcet} avec le langage {Signal}}, type={\DEA}, institution={SNECMA}, month=sep , year=1993 } @BOOK{tni, author={TNI}, title= {Manuel de r\'ef\'erence {SILDEX}}, year=1994 } @BOOK{jones93, author={N. D. Jones and C. Gomard and P. Sestoft}, title={Partial Evaluation and Automatic Program Generation}, publisher={Prentice Hall International}, year=1993 } @INPROCEEDINGS{wadler84, author={Ph. Wadler}, title={Listlessness in Better than Laziness}, booktitle={ACM Symp. on Lisp and Functional Programming}, address={Austin}, month=aug , year=1984 } @INPROCEEDINGS{caspi95, author={P. Caspi and M. Pouzet}, title={A functional extension to \lustre}, booktitle={Eighth International Symp. on Languages for Intensional Programming, ISLIP'95}, address={Sidney}, month=may , year=1995 } @INPROCEEDINGS{maffeis94, author={O. Maffeis and P. {Le Guernic}}, title={Distributed implementation of {\sc Signal}: scheduling and graph clustering}, booktitle={3rd Internationl Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems}, publisher={LNCS 863, Springer Verlag}, month=sep , year=1994 } @article{berthomieu91, author={B. Berthomieu and M. Diaz}, title={Modeling and verification of time dependent systems using {T}ime {P}etri{N}ets}, journal={IEEE Trans. on Software Engineering}, volume=17, number=3, month=mar , year=1991 } @article{electre, author={F. Cassez and O. Roux}, title={Compilation of the {\sc Electre} reactive language into finite transition systems}, journal={Theoretical Computer Science}, volume=144, month=jun , year=1995 } @inproceedings{augeraud94, author={M. Augeraud and F. Bertrand}, title={Asynchronous reactive objects}, booktitle={OOPSLA'94}, address={Portland (Oregon)}, month=oct , year=1994 } @techreport{boulanger93, author={F. Boulanger}, title={Int\'egration de modules synchrones dans la programmation par objet}, type={\thesis\ }, institution={Universit\'e Paris Sud}, month=dec , year=1993 } @techreport{dc, author={C2A-SYNCHRON}, title={The common format of synchronous languages -- {T}he declarative code {DC}}, Institution={Eureka-SYNCHRON Project}, month=oct , year= 1995 } @inproceedings{oracle, author={F. Maraninchi and N. Halbwachs}, title={Compositional semantics of non deterministic synchronous languages}, booktitle={European Symposium on Programming, ESOP'96}, address={Link\"{o}ping}, month=apr , year= 1996 } @inproceedings{rutten95, author={E. Rutten and F. Martinez}, title={{\sc SignalGTI}, implementing task preemption and time interval in the synchronous data-flow language {\sc Signal}}, booktitle={7th Euromicro Workshop on Real Time Systems}, address={Odense (Denmark)}, month=jun , year=1995 } @inproceedings{rushby94, author={J. Rushby}, title={A formally verified algorithm for clock synchronization under a hybrid fault model}, booktitle={13th ACM Symp. on Principles of Distributed Computing, PODC'94}, address={Los Angeles}, month=aug , year=1994 } @inproceedings{lamport91, author={M. Abadi and L. Lamport}, title={An old-fashioned recipe for real time}, booktitle={{\sc Rex} Workshop on Real-Time: Theory in Practice, DePlasmolen (Netherlands)}, editor={J.W. de Bakker and C. Huizing and W. P. de Roever and G. Rozenberg}, PUBLISHER={LNCS 600, Springer Verlag}, MONTH = jun , YEAR= {1991} } @incollection{dill94, author={H. Wong-Toi and D. Dill}, title={Aproximations for verifying timing properties}, chapter={7}, booktitle={Theories and Experiences for Real-Time System Development}, publisher={World Scientific}, year=1995 } @inproceedings{dill95, author={D. DiIl and H. Wong-Toi}, title={Verification of real-time systems by successive over- and under-approximations}, booktitle={7th International Conference on Computer Aided Verification, CAV'95}, editor={P. Wolper}, publisher={LNCS 939, Springer Verlag}, address={Liege (Belgium)}, month=jul , year={1995} } @article{bergeron95, author={A. Bergeron}, title={Sharing out control in distributed processes}, journal={TCS}, volume=139, year=1995, pages={163--186} } @inproceedings{clarke95, author={E. M. Clarke and O. Grumberg and S. Jha}, title={Verifying parameterized networks using abstraction and regular languages}, booktitle={CONCUR'95}, publisher={LNCS 962, Springer Verlag}, month=aug , year= 1995 } @book{eilenberg74, author={S. Eilenberg}, title={Automata, Languages, and Machines}, publisher={Academic Press}, year=1974 } @inproceedings{grumberg89, author={Z. Shtadler and O. Grumberg}, title={Network grammars, communication behaviors and automatic verification}, BOOKTITLE= {Workshop on Automatic Verification Methods for Finite State Systems, Grenoble}, PUBLISHER = {LNCS 407, Springer Verlag}, MONTH = jun , YEAR = 1989 } @unpublished{hu94, author={A. J. Hu}, title={}, note={Private communication}, year=1994 } @inproceedings{mauborgne94, author={L. Mauborgne}, title={Abstract interpretation using {TDG}s}, booktitle={International Symposium on Static Analysis, SAS'94}, editor = {B. {LeCharlier}}, publisher = {LNCS 864, Springer Verlag}, address = {Namur (Belgium)}, month = sep , year= 1994 } @inproceedings{GPVW95, author = {R. Gerth and D. Peled and M. Y. Vardi and P. Wolper}, title = {Simple On-the-fly Automatic Verification of Linear Temporal Logic}, month = jun, year = {1995}, booktitle = {Proc. 15th Work. Protocol Specification, Testing, and Verification}, address = {Warsaw}, publisher = {North-Holland} } @TECHREPORT{Nadjm:Tehrani95, author={M. Westhead and S. Nadjm-Tehrani}, title={A Study of Decompositional Verification of Hybrid Systems}, type={Technical Report}, number={LiTH-IDA-R-95-30}, year=1995 } @unpublished{cattel96, author={T. Cattel and G. Duval}, title={The steam boiler problem in {L}ustre}, note={ Available by FTP at {\tt ltidec1.epfl.ch:/pub/lustre/steamboiler\_lustre.ps.gz}}, year=1996 } @inproceedings{Mauto:cav:94, author={R. {De Simone} and A. Ressouche}, title={Compositional semantics of {\sc Esterel} and verification by compositional reductions}, booktitle={6th International Conference on Computer Aided Verification, CAV'94}, editor={D. Dill}, publisher={LNCS 818, Springer Verlag}, address={Stanford}, month=jun , year={1994} } @inproceedings{tempest:cav:95, author={L. J. Jagadeesan and C. Puchol and J. E. {Von Olnhausen}}, title={Safety property verification of {\sc Esterel} programs and applications to telecommunication software}, booktitle={7th International Conference on Computer Aided Verification, CAV'95}, editor={P. Wolper}, publisher={LNCS 939, Springer Verlag}, address={Liege (Belgium)}, month=jul , year={1995} } @inproceedings{xeve:cav:98, author={A. Bouali}, title={Xeve: an {E}sterel Verification Environment}, BOOKTITLE={Tenth International Conference on Computer-Aided Verification, CAV'98}, address={Vancouver (B.C.)}, PUBLISHER = {LNCS 1427, Springer Verlag}, month = jun , year = 1998 } @inproceedings{production:cell, author={L. Holenderski}, title={Production cell in {\sc Lustre}}, booktitle={Case Study ``Production Cell'': a Comparative Study in Formal Software Development}, editor={C. Lewerentz and Th. Lindner}, publisher={FZI-Publikation 940001, ISSN 0944-3037}, address={Forschungszentrum Informatik, Karlsruhe}, year=1994 } @book{productioncell, author={C. Lewerentz and Th. Lindner (eds.)}, title={Case Study ``Production Cell'': a Comparative Study in Formal Software Development}, publisher={FZI-Publikation 940001, ISSN 0944-3037}, address={Forschungszentrum Informatik, Karlsruhe}, year=1994 } @inproceedings{parissis94, author={F. Ouabdesselam and I. Parissis}, title={Testing Synchronous Critical Software}, booktitle={5th International Symposium on Software Reliability Engineering (ISSRE'94)}, address={Monterey, USA}, month=nov, year=1994 } @inproceedings{lutess98, author={{L. du} Bousquet and F. Ouabdesselam and J.-L. Richier and N. Zuanon}, title={Lutess: testing environment for synchronous software}, booktitle={Tool support for System Specification Development and Verification}, publisher={Advances in Computing Science, Springer}, year= 1998 } @inproceedings{mazuet94, author={P. {Thevenod-Fosse} and C. Mazuet and Y. Crouzet}, title={On Statistical Testing of Synchronous Data Flow Programs}, booktitle={1st European Dependable Computing Conference (EDCC-1)}, address={Berlin, Germany}, pages={250--67}, year=1994 } @INPROCEEDINGS{FernandezJardJeronViho-96a, AUTHOR = {J.-C. Fernandez and C. Jard and T. J\'{e}ron and C. Viho}, TITLE = {Using on-the-fly verification techniques for the generation of test suites}, EDITOR={R. Alur and T. Henzinger}, BOOKTITLE={8th International Conference on Computer Aided Verification, CAV'96}, ADDRESS={Rutgers (N.J.)}, YEAR = {1996} } @INPROCEEDINGS{emerson96, AUTHOR = {E. A. Emerson and K. S. Namjoshi}, TITLE= {Automatic verification of parameterized synchronous systems}, EDITOR={R. Alur and T. Henzinger}, BOOKTITLE={8th International Conference on Computer Aided Verification, CAV'96}, ADDRESS={Rutgers (N.J.)}, YEAR = {1996} } @INPROCEEDINGS{lesens96, AUTHOR = {D. Lesens and N. Halbwachs and P. Raymond}, TITLE={Automatic Construction of Network Invariants}, BOOKTITLE={International Workshop on Verification of Infinite State Systems (INFINITY) }, ADDRESS={Pisa}, MONTH=aug , year={1996} } @INPROCEEDINGS{lesens:popl, AUTHOR = {D. Lesens and N. Halbwachs and P. Raymond}, TITLE={Automatic Verification of Parameterized Linear Networks of Processes}, BOOKTITLE={24th ACM Symposium on Principles of Programming Languages, POPL'97}, ADDRESS={Paris}, MONTH=jan , year= 1997 } @article{tcs99, author={D. Lesens and N. Halbwachs and P. Raymond}, title={Automatic Verification of Parameterized Networks of Processes}, journal={Theoretical Computer Science}, volume = {256}, year=2001, pages={113--144} } @inproceedings{emerson95, author={E. A. Emerson and K. S. Namjoshi}, title={Reasoning about rings}, BOOKTITLE={Proc. 22th ACM Conf. on Principles of Programming Languages, POPL'95}, MONTH=jan , address={San Francisco}, year= 1995 } @INPROCEEDINGS{ArgosDC-FTRTFT96, AUTHOR = {F. Maraninchi and N. Halbwachs}, TITLE = {Compiling {Argos} into Boolean equations}, BOOKTITLE = {Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT)}, PUBLISHER = {LNCS 1135, Springer Verlag}, ADDRESS = {Uppsala (Sweden)}, MONTH = sep , YEAR = 1996 } @INPROCEEDINGS{reglo:icalp96, AUTHOR = {P. Raymond}, TITLE = {Recognizing Regular Expressions by means of Dataflows Networks}, BOOKTITLE = {23rd International Colloquium on Automata, Languages, and Programming, (ICALP'96) {\em Paderborn, Germany}}, MONTH = jul , PUBLISHER = {LNCS 1099, Springer Verlag}, YEAR = 1996 } @InProceedings{afcet96, author = {B. Caillaud and P. Caspi and A.Girault and C. Jard}, title = {Un mod\`ele pour la distribution d'automates r\'eactifs sur r\'eseau asynchrone de processeurs}, booktitle = {Conf\'erence Afcet sur la Mod\'elisation des syst\`emes r\'eactifs}, address = {Brest}, month = mar , year = 1996 } @InProceedings{parle95, author = {P. Caspi and A. Girault}, title = {Execution of reactive distributed systems}, booktitle = {EURO--PAR'95 Stockholm}, series = {LNCS}, volume = {966}, year = 1995, publisher = {Springer Verlag}, month = aug , } @phdthesis{alain:these, AUTHOR = {A. Girault}, TITLE = {Sur la r\'epartition de programmes synchrones}, SCHOOL = {Institut national Polytechnique de Grenoble}, MONTH = jan , YEAR = {1994} } @InProceedings{CFG95, author = {P. Caspi and J.C. Fernandez and A. Girault}, title = {An algorithm for reducing binary branchings}, booktitle = {FST~\&~TCS Bangalore}, series = {LNCS}, volume = {1026}, year = 1995, publisher = {Springer Verlag}, month = dec } @INPROCEEDINGS{caspi94b, AUTHOR={P. Caspi}, TITLE={Towards recursive block diagrams}, BOOKTITLE={19th IFAC Workshop on Real Time Program ming WRTP'94}, PUBLISHER = {IFAC}, PAGES = {81--86}, MONTH= jun , YEAR=1994 } @InProceedings{islip95, author = {P. Caspi and M. Pouzet}, title = {A functional extension to {\sc Lustre}}, editor = {M. A. Orgun and E. A. Ashcroft}, booktitle = {8th Int. Symp. on Languages for Intensional Programming, Sydney}, year = 1995, publisher = {World Scientific}, month = may } @InProceedings{jfla96, author = {P. Caspi and M. Pouzet}, title = {R\'eseaux de {K}ahn synchrones}, booktitle = {Journ\'ees Francophones des langages applicatifs, Val Morin, Quebec}, year = 1996, publisher = {INRIA}, month = jan } @InProceedings{icfp96, author = {P. Caspi and M. Pouzet}, title = {Synchronous {K}ahn networks}, booktitle = {Int. Conf. on Functional Programming, Philadelphia}, year = 1996, publisher = {ACM SIGPLAN}, month = may } @InProceedings{Argos+Polka-hybrid95, author = {N. Halbwachs and F. Maraninchi and Y. E. Proy}, title = {The railroad crossing problem, modeling with {H}ybrid {A}rgos - {A}nalysis with {P}olka}, booktitle = {Second European Workshop on Real-Time and Hybrid Systems}, year = {1995}, address = {Grenoble (France)}, month = jun } @inproceedings{kronos:cav96, author={S.~Tripakis and S.~Yovine}, title={Analysis of timed systems based on time--abstracting bisimulations}, booktitle={Proc. 8th Conference Computer-Aided Verification, CAV'96}, publisher= {Springer-Verlag}, pages={232--243}, organization={Lecture Notes in Computer Science 1102}, address={Rutgers, NJ}, month=jul , year=1996} @inproceedings{kronos:rtss96, author={C.~Daws and S.~Yovine}, title={Reducing the number of clock variables of timed automata}, booktitle={Proc. 1996 IEEE Real-Time Systems Symposium, RTSS'96}, publisher={IEEE Computer Society Press}, address={Washington, DC, USA}, month=dec , year=1996} @article{atp:ieee, author={X. Nicollin and J. Sifakis and S. Yovine}, title={Compiling real-time specifications into extended automata}, journal={{IEEE TSE} {S}pecial {I}ssue on {R}eal-{T}ime {S}ystems}, month=sep , year=1992, volume=18, number=9, pages={794--804}} @inproceedings{kronos:forte94, author={C.~Daws and A.~Olivero and S.~Yovine}, title={Verifying {ET-LOTOS} programs with {KRONOS}}, booktitle={Proc. 7th. IFIP WG G.1 International Conference of Formal Description Techniques, FORTE'94}, pages={227--242}, organization={Formal Description Techniques VII}, publisher={Chapman \& Hall}, editor={D. Hogrefe and S. Leue}, address={Bern, Switzerland}, month=oct , year=1994} @inproceedings{kronos:hybsys96, author={C.~Daws and A.~Olivero and S.~Tripakis and S.~Yovine}, title={The tool {KRONOS}}, booktitle={Hybrid Systems III, Verification and Control}, publisher= {Springer-Verlag}, pages={208--219}, organization={Lecture Notes in Computer Science 1066}, year=1996} @inproceedings{kronos:rtss95, author={C.~Daws and S.~Yovine}, title={Two examples of verification of multirate timed automata with {KRONOS}}, booktitle={Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95}, publisher={IEEE Computer Society Press}, address={Pisa, Italy}, month=dec , year=1995} @unpublished{multiclock:esterel, author={G. Berry and S. Ramesh and R. K. Shyamasundar}, title={Multi-clock {E}sterel}, note={Manuscript}, year=1995 } @inproceedings{coudert92, author={O. Coudert and J. C. Madre}, title={A new method to compute prime and essential prime implicants of {B}oolean functions}, booktitle={MIT VLSI Conference}, address={Cambridghe (MA)}, month=mar , year=1992 } @article{king76, author={J. C. King}, title={Symbolic execution and program testing}, journal={CACM}, volume=19, number=7, month=jul , year=1976 } @inproceedings{coudert93, author={O. Coudert and J. C. Madre and H. Fraiss\'{e}}, title={A new viewpoint on two-level logic minimization}, booktitle={30th IEEE/ACM Design Automation Conference}, address={Dallas (Texas)}, month=jun , year= 1993 } @TechReport{grumberg91, author = {R. Marelly and O. Grumberg}, title = {GORMEL-Grammar ORiented ModEL checker.}, institution = {The Technion}, year = {1991}, number = {697}, month = oct, } @INPROCEEDINGS{pnueli97, AUTHOR = {Y. Kesten and O. Maler and M. Marcus and A. Pnueli and E. Shahar}, TITLE = {Symbolic Model Checking with Rich Assertional Languages}, BOOKTITLE = {9th Conference on Computer Aided Verification, CAV'97}, MONTH = jul , YEAR = {1997} } @inproceedings{fribourg97, title = {Reachability sets of parameterized rings as regular languages}, author = {L. Fribourg and H. Ols\'{e}n}, booktitle = {International Workshop on Verification of Infinite State Systems (INFINITY) }, address = {Bologna}, month = jul , year = {1997} } @BOOK{ullman84, author={J. D. Ullman}, title={Computational Aspects of {VLSI}}, publisher={Computer Science Press}, year=1984, } @article{martin85, author = {A. J. Martin}, title = {Distributed Mutual Exclusion on a Ring of Processes}, journal = {Science of Computer Programming}, year = {1985}, volume = {5}, pages = {265-276}, publisher = {North-Holland Publisher} } @article{polka:fmsd:97, author={N. Halbwachs and Y.E. Proy and P. Roumanoff}, title={Verification of real-time systems using linear relation analysis}, journal={Formal Methods in System Design}, year={1997}, month=aug , volume={11}, number={2}, pages={157--185}, publisher={Kluwer}, } @Inproceedings{lesens:amast, author = {D. Lesens}, title = {Invariants of Parameterized Binary Tree Networks as Greatest Fixpoints}, booktitle = {Sixth International Conference on Algebraic Methodology and Software Technology, AMAST'97}, address = {Sydney}, month = dec , year = {1997} } @techreport{mrlustre, key={Ver96}, title={{SAO+/SAOCG} - {L}angage {L}ustre, Manuel de r\'ef\'erence}, institution={V\'erilog S.A.}, year=1996 } @inproceedings{demillo80, author={R. A. {DeMillo}}, title={Mutation analysis as a tool for software quality assurance}, booktitle={COMPSAC'80}, address={Chicago}, month=oct , year= 1980 } @PhdThesis{these:lesens, author = {D. Lesens}, title = {V\'{e}rification et synth\`{e}se de syst\`{e}mes r\'{e}actifs}, school = {Institut National Polytechnique de Grenoble}, month = sep , year = {1997} } @article{reactiveC, author={F. Boussinot}, title={Reactive {C}: An Extension of {C} to Program Reactive Systems}, journal={Software Practice and Experience}, volume= 21, number= 4, pages={401--428}, year= 1991 } @article{sl, author={F. Boussinot and R. de Simone}, title={The {SL} Synchronous Language}, journal={IEEE Transactions on Software Engineering}, volume=22, number= 4, pages= {256--266}, month= apr , year= 1996 } @inproceedings{boniol95, author={F. Boniol}, title={Synchronous communicating reactive processes}, booktitle={2nd AMAST Workshop on Real-Time Systems}, address={Bordeaux}, month=jun , year= 1995 } @techreport{herylaleuf, title={Stabilit\'e de la r\'ealisation des {DFL}}, author={{J.-F.} H\'ery and {J.-C.} Laleuf}, type={\techreport\ }, institution = {Electricit\'e de France}, year= 1997 } @inproceedings{stable, title={Stability of discrete sampled systems}, author={N. Halbwachs and {J.-F.} H\'ery and {J.-C.} Laleuf and X. Nicollin}, booktitle={FTRTFT'2000}, publisher={LNCS 1926}, address={Pune, India}, month=sep, year=2000 } @techreport{weber98, title={Un g\'en\'erateur automatique de jeux de test de programmes {Lustre}}, author={D. Weber}, type={M\'emoire d'Ing\'enieur}, institution = {Conservatoire National de Arts et M\'etiers}, month=mar , year=1998 } @InProceedings{Modes-COMPOS97, author={F. Maraninchi and Y. R\'{e}mond}, title={Compositionality Criteria for Defining Mixed-Styles Synchronous Languages}, booktitle={International Symposium: Compositionality - The Significant Difference}, address={Malente (Holstein, Germany)}, publisher = {Springer Verlag}, month= sep , year=1997 } @InProceedings{Modes-ESOP98, author={F. Maraninchi and Y. R\'{e}mond}, title={Mode-Automata: About Modes and States for Reactive Systems}, booktitle={European Symposium On Programming}, address={Lisbon (Portugal)}, publisher = {Springer Verlag}, month= mar, year=1998 } @inproceedings{marce93, author={P. {LeParc} and L. Marc\'e}, title={Synchronous definition of {G}rafcet with {S}ignal}, booktitle={IEEE SMC'93}, year=1993 } @unpublished{strlbook, author={G. Berry}, title={The Constructive Semantics of {E}sterel}, note={Draft book available by ftp at {\tt ftp://ftp-sop.inria.fr/meije/esterel/papers/cons\-tructi\-veness.ps.gz}}, year = 1995 } @inproceedings{syndex, author={C. Lavarenne and O. Seghrouchni and Y. Sorel and M. Sorine}, title={The {SynDEx} software environment for real-time distributed systems design and implementation}, booktitle={European Control Conference, ECC'91}, month=jul , year= 1991 } @inproceedings{toma96, author={E. Sentovich and H. Toma and G. Berry}, title={Latch optimization in circuits generated from high-level descriptions}, booktitle={ICCAD'96}, month=nov , year= 1996 } @inproceedings{toma97, author={E. Sentovich and H. Toma and G. Berry}, title={Efficient latch optimization using incompatible sets}, booktitle={34th Design Automatio Conference}, month=jun , year= 1997 } @techreport{sis, author={E. Sentovich and K. J. Singh and L. Lavagno and C. Moon and R. Murgai and A. Aldanha and H. Savoj and P. R. Stephan and R. K. Brayton and A. L. Sangiovanni-Vincentelli}, title={{SIS}: a system for sequential circuit synthesis}, type={Technical Report Memorandum nr. UCB/ERL M92/41}, institution = {University of California at Berkeley}, year= 1992 } @inproceedings{strlauto, author={R. de Simone and Annie Ressouche}, title={Compositional semantics of \esterel\ and verification by compositional reductions}, booktitle={CAV'94}, address={Stanford}, month=jun , year=1994 } @inproceedings{modes, author={F. Maraninchi and Y. R\'{e}mond}, title={Mode-Automata: About Modes and States for Reactive Systems}, booktitle={European Symposium on Programming, ESOP'98}, address={Lisbon}, month=apr , year=1998 } @unpublished{modes:pldi, author={F. Maraninchi and Y. R\'{e}mond}, title={Running Modes in a Dta-Flow Language: Mode-Automata and their Implementation}, note={Submitted for Publication}, year = 1998 } @article{mullerburg95, author={M. M\"ullerburg and L. Holenderski and O. Maffeis and M. Morley}, title={Systematic testing and formal verification to validate reactive programs}, journal={Software Quality Journal}, volume= 4, number = 4, pages={287--307}, year=1995 } @inproceedings{marre98, author={B. Marre}, title={Test data selection for reactive synchronous software}, booktitle={Dagstuhl-Seminar-Report 223: Test Automation for Reactive Systems - Theory and Practice}, month=sep, year=1998 } @inproceedings{westhead96, author={M. Westhead and S. Nadjm-Tehrani}, title={Verification of Embedded Systems using Synchronous Observers}, booktitle={FTRTFT'96}, publisher={LNCS 1135}, address={Uppsala}, month=sep , year= 1996 } @incollection{strlfoundations, author={G. Berry}, title={The Foundations of {E}sterel}, booktitle={Proof, Language and Interaction: Essays in Honour of Robin Milner}, editor={G. Plotkin, C. Stirling and M. Tofte}, publisher={MIT Press}, year=1998 } @inproceedings{syncchart96, author={C. Andr\'e}, title={Representation and analysis of reactive behaviors: a synchronous approach}, booktitle={IEEE-SMC'96, Computational Engineering in Systems Applications}, address={Lille, France}, month=jul , year=1996 } @inproceedings{andre96b, author={C. Andr\'e and D. Gaff\'e}, title={Proving Properties of {\sc Grafcet} with Synchronous Tools}, booktitle={IEEE-SMC'96, Computational Engineering in Systems Applications}, address={Lille, France}, month=jul , year=1996 } @unpublished{lurette, author={X. Nicollin and P. Raymond and D. Weber}, title={Automatic testing of reactive programs}, note={\inpreparation\ }, year = 1998 } @techreport{manuel:lustre, author={N. Halbwachs}, title={Lustre Language Reference Manual --- Versions 3, 3+, 4, 5}, type={\techreport\ }, number={97-09}, institution={V\'erimag}, month=sep , year=1997 } @INPROCEEDINGS{cav:tutorial, AUTHOR = {N. Halbwachs}, TITLE={Synchronous programming of reactive systems, a tutorial and commented bibliography}, BOOKTITLE={Tenth International Conference on Computer-Aided Verification, CAV'98}, address={Vancouver (B.C.)}, PUBLISHER = {LNCS 1427, Springer Verlag}, month = jun , year = 1998 } @INPROCEEDINGS{lurette:movep, AUTHOR = {N. Halbwachs and X. Nicollin and P. Raymond and D. Weber}, TITLE={Test automatique de syst\`emes r\'eactifs}, BOOKTITLE={Ecole d'\'et\'e ``Mod\'elisation et V\'erification des Processus Paralle\`eles, MOVEP'98}, address = {Nantes}, month=jul , year=1998 } @INPROCEEDINGS{lurette:rtss, AUTHOR = {P. Raymond and D. Weber and X. Nicollin and N. Halbwachs}, TITLE={Automatic Testing of Reactive Systems}, BOOKTITLE={19th IEEE Real-Time Systems Symposium}, address = {Madrid, Spain}, month=dec , year = 1998 } @techreport{zampunieris97, author={Denis Zampuni\'eris}, title={The Sharing Tree Data Structure}, type={PhD Thesis}, institution={Facult\'es Universitaires Notre-Dame de la Paix, Namur (Belgium)}, month=may , year= 1997 } @TECHREPORT{Habilitation-Florence97, AUTHOR={F. Maraninchi}, TITLE={Mod\'elisation et validation des syst\`emes r\'eactifs : un langage synchrone \`a base d'automates}, TYPE ={Document d'Habilitation \`a Diriger des Recherches}, INSTITUTION ={Universit\'{e} Joseph Fourier, Grenoble}, ADDRESS = {Grenoble}, MONTH = may, YEAR = {1997} } @article{tarjanSCC, author={R. E. Tarjan}, title={Depth-first search and linear graph algorithms}, journal={SIAM Journal on Computing}, volume = 1, year = 1972, pages={146--160} } @techreport{bourdoncle:these, author={F. Bourdoncle}, title={S\'emantique des langages imp\'eratifs d'ordre sup\'erieur et interpr\'etation abstraite}, type = {\thesis\ }, institution={Ecole Polytechnique, Paris}, year= 1992 } @inproceedings{mauras:yoyo:wsp, author={Ch. Mauras}, title={Symbolic Simulation of Interpreted Automata}, booktitle={3rd Workshop on Synchronous Programming}, address={Dagstuhl (Germany)}, month=dec, year=1996 } @inproceedings{bourdoncle90, author={F. Bourdoncle}, title={Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity}, booktitle={PLILP'90}, publisher={LNCS 456, Springer Verlag}, year=1990 } @INPROCEEDINGS{bultan97, AUTHOR = {T. Bultan and R. Gerber and W. Pugh}, TITLE = {Symbolic model checking of infinite state systems using {P}resburger arithmetic}, BOOKTITLE = {Computer Aided Verification, CAV'97}, publisher={LNCS 1254, Springer Verlag}, month = jun, year = {1997} } @article{bultan-TOPLAS, AUTHOR = {T. Bultan and R. Gerber and W. Pugh}, title={Model-Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations, and Experimental Results}, journal={ACM Transactions on Programming Languages and Systems (TOPLAS)}, volume=21, number=4, pages={747--789}, month= jul, year=1999 } @TechReport{bultan99, type = {Technical Report}, number = {TRCS99-02}, institution = {University of California, Santa Barbara}, title = {Composite Model Checking: Verification with Type-Specific Symbolic Representations}, month = jan, year = {1999}, url = {ftp://ftp.cs.ucsb.edu/pub/techreports/TRCS99-02.ps}, author = {T. Bultan and R. Gerber and C. League} } @article{bourdoncle92b, author={F. Bourdoncle}, title={Abstract Interpretation By Dynamic Partitionning}, journal={Journal of Functional Programming}, volume = 2, number = 4, year = 1992 } @ARTICLE{cousot92c, AUTHOR={P. Cousot and R. Cousot}, TITLE={Abstract Interpretation Frameworks}, journal={Journal of Logic and Computation}, year=1992 } @inproceedings{BCDP99, author = {S. Bensalem and P. Caspi and C. Dumas and C. {Parent-Vigouroux}}, title = {A methodology for proving control programs with {L}ustre and {P}{V}{S}.}, booktitle = {Dependable Computing for Critical Applications, DCCA-7, San Jose}, year = 1999, month = jan, publisher = {IEEE Computer Society} } @inproceedings{asian99, author = {N. Halbwachs and P. Raymond}, title = {Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing}, booktitle = {ASIAN'99, Asian Computing Science Conference}, address={Phuket (Thailand)}, year = 1999, month = dec } @inproceedings{sas99, author = {B. Jeannet and N. Halbwachs and P. Raymond}, title = {Dynamic Partitioning in Analyses of Numerical Properties}, booktitle = {Static Analysis Symposium, SAS'99}, publisher={LNCS 1694, Springer Verlag}, editor={A. Cortesi and G. Fil\'e}, address={Venice (Italy)}, month = sep, year=1999 } @article{harel96, author={D. Harel and A. Naamad}, title={The {S}tatemate semantics of {S}tatecharts}, journal={ACM Transactions on Software Engineering and Methodology}, volume = 5, number= 4, month = oct, year = 1996 } @techreport{iec1131, author={IEC}, title={International Standard for Programmable Controllers: Programming Languages}, type={Technical Report IEC1131, part 3}, institution={International Electrotecnical Commission}, year=1993 } @inproceedings{kurshan99, author={K. S. Namjoshi and R. P. Kurshan}, title={Efficient Analysis of Cyclic Definitions}, booktitle={11th International Conference on Computer Aided Verification, CAV'99}, address={Trento (Italy)}, month = jul, year= 1999 } @InProceedings{pvs, author = {S. Owre and J. Rushby and N. Shankar}, title = {P{V}{S}: a prototype verification system}, volume = 607, series = {Lecture Notes in Computer Science}, pages = {748--752}, booktitle = {11th Conf. on Automated Deduction}, year = 1992, publisher = {Springer Verlag} } @Book{boyermoore, author = {R.S. Boyer and J.S.Moore}, title = {A Computational Logic}, publisher = {Academic Press}, year = 1979 } @Article{coq1, author = {T. Coquand and G. Huet}, title = {The calculus of construction}, journal = {Information and Computation}, year = 1988, volume = 76, number = 2 } @Article{coq2, author = {C. Paulin-Mohring and B. Werner}, title = {Synthesis of ML programs in the system Coq}, journal = {Journal of Symbolic Computation}, year = 1993, volume = 15, pages = {607--640} } @Book{hol, author = {M. J. Gordon and T. F. Melham}, title = {Introduction to {HOL} : A Theorem Proving Environment for Higher-Order Logic}, publisher = {Cambridge University Press}, year = {1993}, address = {Cambridge, UK}, } @Book{abrial, author = {J.-R. Abrial}, title = {The B-Book}, publisher = {Cambridge University Press}, year = 1995 } @book{Rogers, title={Theory of Recursive Functions and Effective Computability}, author={H. Rogers}, publisher={The MIT Press}, year=1987 } @inproceedings{peled98, author={D. Peled}, title={Ten years of partial order reduction}, BOOKTITLE={Tenth International Conference on Computer-Aided Verification, CAV'98}, address={Vancouver (B.C.)}, PUBLISHER = {LNCS 1427, Springer Verlag}, month = jun , year = 1998 } @unpublished{autographweb, author={Autograph}, title={\website{http://www-sop.inria.fr/meije/verification/}}, note={} } @inproceedings{bouali92, author={A. Bouali and {R. de} Simone}, title={Symbolic bisimulation minimization}, BOOKTITLE={4th Int. Workshop on Computer Aided Verification}, address={Montreal}, EDITOR={G. Bochmann}, YEAR=1992 } @techreport{VanGlabbeek-Weijland-89, author = {R. J. van Glabbeek and W. P. Weijland}, title = {Branching-Time and Abstraction in Bisimulation Semantics (extended abstract)}, institution = cwi, year = {1989}, type = {CS}, number = {R8911}, address = {Amsterdam}, note = {Also in proc. IFIP 11th World Computer Congress, San Francisco, 1989}, } @TECHREPORT{jeannet:these, AUTHOR = {B. Jeannet}, TITLE={Partitionnement dynamique dans l'analyse de relations lin\'eaires et application \`a la v\'erification de programmes synchrones}, TYPE = {These}, INSTITUTION= {Institut National Polytechnique, Grenoble}, MONTH = sep , YEAR = {2000} } @article{clarke94, author={E. M. Clarke and O. Grumberg and D. E. Long}, title={Model checking and abstraction}, journal={ACM TOPLAS}, pages={1512--1542}, number=5, volume=16, year=1994 } @ARTICLE{Modes-SCP, AUTHOR = {F. Maraninchi and Y. R\'emond}, TITLE = {Mode-Automata: a New Domain-Specific Construct for the Development of Safe Critical Systems}, JOURNAL = {Science of Computer Programming}, VOLUME={to appear}, NUMBER={}, YEAR={} } @inproceedings{fmics, title={Counter-example generation in symbolic abstract model-checking}, author={G. Pace and N. Halbwachs and P. Raymond}, booktitle={6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS'2001}, publisher={Inria}, address={Paris}, month=jul, year=2001 } @article{fmics-sttt, title={Counter-example generation in symbolic abstract model-checking}, author={G. Pace and N. Halbwachs and P. Raymond}, journal={Software Tools for Technology Transfer}, volume=5, number={2---3}, month=mar, year=2004 } @inproceedings{holenderski00, title={Compositional verification of synchronous networks}, author={L. Holenderski}, booktitle={FTRTFT'2000}, publisher={LNCS 1926}, address={Pune, India}, month=sep, year=2000 } @techreport{deamorel, author = {L. Murasorel}, title = {Compilation efficace d'itérateurs de tableaux {LUSTRE}}, type={M\'emoire de {DEA}}, institution = {Université Joseph Fourier, Grenoble}, MONTH = jun , year = 2001 } @book{nielson99, author = {F. Nielson and H. R. Nielson and C. Hankin}, title={Principles of Program Analysis}, publisher={Springer-Verlag}, year=1999 } @article{alur99, author = {R. Alur and T. A. Henzinger}, title={Reactive modules}, journal= {Formal Methods in System Design}, volume= 15, pages={7-48}, year=1999 } @inproceedings{benveniste-concur99, author= {A. Benveniste and B. Caillaud and P. Le Guernic}, title={From synchrony to asynchrony}, editor={J.C.M. Baeten and S. Mauw}, booktitle={CONCUR'99}, publisher={LNCS 1664, Springer Verlag}, year= 1999 } @inproceedings{berry-sentovich98, author={ G. Berry and E. Sentovich}, title={Embedding Synchronous Circuits in {GALS}-based Systems}, booktitle={Sophia-Antipolis conference on Micro-Electronics (SAME 98)}, month= oct, year=1998 } @inproceedings{multiclock-esterel01, author={G. Berry and E. Sentovich}, title={Multiclock {E}sterel}, booktitle={Correct Hardware Design and Verification Methods, CHARME'01}, address={Livingston (Scotland)}, publisher={LNCS 2144, Springer Verlag}, month=sep, year= 2001 } @book{balarin_kluwer_97, author = {F. Balarin and M. Chiodo and P. Giusto and H. Hsieh and A. Jurecska and L. Lavagno and C. Passerone and A. Sangiovanni-Vincentelli and E. Sentovich and K. Suzuki and B. Tabbara}, title = {Hardware-Software Co-Design of Embedded Systems: The Polis Approach}, publisher = {Kluwer Academic Publishers}, year = 1997 } @techreport{benveniste-caspi-tripakis, author={A. Benveniste and P. Caspi and S. Tripakis}, title={Distributing synchronous programs on a loosely synchronous, distributed architecture}, type={Research Report}, institution={Irisa}, number=1289, month=dec, year=1999 } @book{sdl, author={{ITU-T}}, title={Recommendation Z-100. Specification and description language (SDL)}, year=1994 } @book{kopetz97, author={H. Kopetz}, title={Real-Time Systems: Design Pronciples for Distributed Embedded Applications}, publisher={Kluwer Academic Publisher}, year=1997 } @inproceedings{rushby-tta, author={J. Rushby}, title={Bus architectures for safety-critical embedded systems}, booktitle={1st International Workshop on Embedded Software, EMSOFT2001}, address={Lake Tahoe}, publisher={LNCS 2211}, month=oct, year=2001 } @inproceedings{caspi-emsoft, author={P. Caspi}, title={Embedded Control: From Asynchrony to Synchrony and Back}, booktitle={1st International Workshop on Embedded Software, EMSOFT2001}, address={Lake Tahoe}, publisher={LNCS 2211}, month=oct, year=2001 } @inproceedings{caspi-safecomp01, author={P. Caspi and C. Mazuet and N. {Reynaud Paligot}}, title={About the design of distributed control systems, the quasi-synchronous approach}, booktitle={SAFECOMP'01}, publisher={LNCS 2187}, year = 2001 } @inproceedings{caspi-pune, author={P. Caspi and R. Salem}, title={Threshold and Bounded-Delay Voting in Critical Control Systems}, booktitle={FTRTFT'2000}, publisher={LNCS 1926}, address={Pune, India}, month=sep, year=2000 } @inproceedings{desimone-iwls, author={R. de Simone and A. Bouali}, title={A symbolic representation of asynchronous networks of synchronous processes}, booktitle={Tenth International Workshop on Logic Synthesis, IWLS'98}, address={Lake Tahoe}, month=jun, year= 1998 } @inproceedings{lutin-slap, author={P. Raymond and Y. Roux}, title={Describing non-deterministic reactive systems by means of regular expressions}, booktitle={First Workshop on Synchronous Languages, Applications and Programming, SLAP'02}, address={Grenoble}, month = apr, year=2002 } @inproceedings{shyam, author={B. Rajan and R. K. Shyamasundar}, title={A fault tolerant distributed system in {M}ulticlock {E}sterel}, booktitle={FORTE/PSTV}, publisher={North Holland}, pages={301--316}, month=oct, year=2000 } @inproceedings{emsoft02, author={N. Halbwachs and S. Baghdadi}, title={Synchronous modeling of asynchronous systems}, booktitle={EMSOFT'02}, publisher={LNCS 2491, Springer Verlag}, month=oct, year= 2002 } @article{edwards02, author={S. A. Edwards}, title={An {E}sterel compiler for large control-dominated systems}, journal={IEEE Transactions on Computer-Aided Design of Integrated Circuits ans Systems}, volume=21, year=2002 } @inproceedings{saxo00, author={D. Weil and V. Bertin and E. Closse and M. Poisse and P. Venier and J. Pulou}, title={Efficient compilation of {E}sterel for real-time embedded systems}, booktitle={International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES)}, address={San Jose}, year=2000 } @inproceedings{cvt98, author={A. Pnueli and M. Siegel and O. Shtrichman}, title={Translation Validation for Synchronous Languages}, editor={K.G. Larsen and S. Skyum and G. Winskel}, booktitle={25th International Colloquium on Automata, Languages, and Programming (ICALP 1998)}, publisher={LNCS 1443}, year=1998 } @inproceedings{tta, author={H. Kopetz}, title={The Time-Triggered Architecture}, booktitle={ISORC'98}, address={Kyoto, Japan}, month=apr, year=1998 } @inproceedings{morel:slap:02, author={L. Morel}, title={Efficient Compilation of Array Iterators for {L}ustre}, booktitle={First Workshop on Synchronous Languages, Applications, and Programming, SLAP02}, address={Grenoble}, month=apr, year=2002 } @article{step:tutorial, author={N. Bjorner and A. Browne and M. Colon and B. Finkbeiner and Z. Manna and H. Sipma and T. Uribe}, title={Verifying Temporal Properties of Reactive Systems: A {STeP} Tutorial}, journal={Formal Methods in System Design}, volume= 16, pages={227--270}, year=2000 } @article{step:lra, author={N. Bjorner and I. Anca Browne and Z. Manna}, title={Automatic Generation of Invariants and Intermediate Assertions}, journal={Theoretical Computer Science}, volume= 173, number=1, pages={49--87}, month=feb, year=1997 } @article{hytech, author={T. A. Henzinger and P.-H. Ho and H. Wong-Toi}, title={HyTech: A model checker for hybrid systems}, journal={Software Tools for Technology Transfer}, volume= 1, pages={110--122}, year=1997 } @inproceedings{sagiv:sas01, author={N. Dor and M. Rodeh and M. Sagiv}, title={Cleanness Checking of String Manipulations in {C} Programs via Integer Analysis}, booktitle={SAS'01}, address={Paris}, publisher={LNCS 2126}, editor={P. Cousot}, month=jul, year=2001 } @unpublished{dor:pldi03, author={N. Dor and M. Rodeh and M. Sagiv}, title={{CCSV}: towards a realistic tool for statically detecting all buffer overflows in {C}}, note={to appear in PLDI03}, year=2003 } @incollection{motskin53, author={T. S. Motzkin and H. Raiffa and G. L. Thompson and R. M. Thrall}, title={The double description method}, booktitle={Contribution to the Theory of Games -- Volume II}, editor={H. W. Kuhn and A. W. Tucker}, publisher={Annals of Mathematic Studies, nr 28, Princeton University Press}, year=1953 } @article{tip95, author={F. Tip}, title={A survey of program slicing techniques}, journal={Journal of Programming Languages}, volume=3, number=3, pages={121--189}, month=sep, year=1995 } @inproceedings{parma:sas:02, author={R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill}, title={Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library}, booktitle={9th International Symposium on Static Analysis, SAS'02}, address={Madrid, Spain}, publisher={LNCS 2477}, editor={ M. V. Hermenegildo and G. Puebla}, month=sep, year=2002 } @Inproceedings{ Bagnara03, AUTHOR = {R. Bagnara and P. M. Hill and E. Ricci and E. Zaffanella}, TITLE = {Precise Widening Operators for Convex Polyhedra}, BOOKTITLE = {Static Analysis: Proceedings of the 10th International Symposium}, ADDRESS = {San Diego, California, USA}, EDITOR = {R. Cousot}, PUBLISHER = {Springer-Verlag, Berlin}, SERIES = {Lecture Notes in Computer Science}, VOLUME = 2694, YEAR = 2003, PAGES = {337--354}, URL = {http://www.cs.unipr.it/ppl/Documentation/BagnaraHRZ03.pdf} } @article{clauss98, author={Ph. Clauss and V. Loechner}, title={Parametric analysis of polyhedral iteration spaces}, journal={Journal of VLSI Signal Processing}, volume=19, number=2, publisher={Kluwer Academic Pub.}, month=jul, year=1998 } @inproceedings{sas03, author = {N. Halbwachs and D. and C. Parent-Vigouroux}, title = {Cartesian factoring of polyhedra in linear relation analysis}, booktitle = {Static Analysis Symposium, SAS'03}, address={San Diego}, month = jun, year=2003 } @article{ieee03, author={A. Benveniste and P. Caspi and S.A. Edwards and N. Halbwachs and P. {Le Guernic} and R. {de Simone}}, title={The synchronous languages 12 years later}, journal={Proceedings of the IEEE}, volume=91, number=1, month=jan, year=2003 } @inproceedings{pandya01, author={P.K. Pandya}, title={Specifying and Deciding Quantified Discrete-time Duration Calculus formulae using DCVALID}, booktitle={Real-Time Tools, RTTOOLS'2001}, address={Aalborg}, month=aug, year=2001 } @inproceedings{pandya02, author={P.K. Pandya}, title={Interval Duration Logic: Expressiveness and Decidability}, booktitle={Workshop on Theory and Practice of Timed Systems TPTS'2002}, address={Grenoble}, month=apr, year=2002 } @inproceedings{pandya03, author={G. Chakravarty and P.K. Pandya}, title={Digitizing interval duration logic}, booktitle={CAV 2003}, address={Boulder, Colorado}, month=jul, year=2003 } @inproceedings{pnueli-popl87, author={Z. Manna and A. Pnueli}, title={Specification and verification of concurrent programs by $\forall$-automata}, booktitle= {14th ACM Symposium on Principles of Programming Languages, POPL'87}, address={Munchen}, month = jan , year = 1987 } @article{hoare-CSP, author={C. A. R. Hoare}, title={Communicating Sequential Processes}, journal={CACM}, month=aug, year=1978 } @article{hoare-monitors, author={C. A. R. Hoare}, title={Monitors, an operating system structuring concept}, journal={CACM}, month=oct, year=1974 } @article{event-structures, author={M. Nielsen and G. D. Plotkin and G. Winskel}, title={Petri Nets, Event Structures and Domains, Part I} , journal={TCS}, volume=13, year=1981 } @inproceedings{valmari91, author={A. Valmari}, title={Stubborn Sets for Reduced State Space Generation}, booktitle={Advances in Petri Nets 1990}, publisher={LNCS 483, Springer-Verlag }, year=1991 } @Article{pi-calcul, author = {Robin Milner and Joachim Parrow and David Walker}, title = {A Calculus of Mobile Processes, Part {I/II}}, journal = {Journal of Information and Computation}, year = 1992, volume = 100, pages = {1--77}, month = sep } @inproceedings{havelund02, title={ Synthesizing Monitors for Safety Properties}, author={K. Havelund and G. Rosu}, booktitle={International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02)}, address={Grenoble, France}, month=apr, year=2002 } @article{durationcalculus, author={Z. Chaochen and C.A.R. Hoare and A.P. Ravn}, title={A calculus of durations}, journal={Information Processing Letters}, volume= 40, number = 5, year= 1991 } @inproceedings{boigelot94, author={B. Boigelot and P. Wolper}, title={Symbolic Verification with Periodic Sets}, booktitle={CAV'94}, publisher={LNCS 818, Springer Verlag}, address={Stanford (Ca.)}, year=1994 } @inproceedings{jurski98, author={H. Comon and Y. Jurski}, title={Multiple Counters Automata, Safety Analysis and {P}resburger Arithmetic}, booktitle={CAV'98}, publisher={LNCS 1427, Springer Verlag}, address={Vancouver (B.C.)}, year=1998 } @inproceedings{finkel00, author={A. Finkel and G. Sutre}, title={An algorithm constructing the semilinear post* for 2-dim Reset/Transfer VASS}, booktitle={25th Int. Symp. Math. Found. Comp. Sci. (MFCS'2000)}, publisher={LNCS 1893, Springer Verlag}, address={Bratislava, Slovakia}, month= aug, year=2000 } @article{clauss02, author={ V. Loechner and B. Meister and Ph. Clauss}, title={Precise data locality optimization of nested loops}, journal={The Journal of Supercomputing}, Volume= 21, Number= 1, pages={37--76}, month=jan, year= 2002, ipublisher={Kluwer Academic Pub.} } @inproceedings{irigoin01, author={N. V. Nguyen and F. Irigoin and C. Ancourt and R. Keryell}, title={Efficient Intraprocedural Array Bound Checking}, booktitle={Second International Workshop on Automated Program Analysis, Testing and Verification, WAPATV'01}, month=may, year=2001, address={Toronto, Canada} } @article{irigoin97, title={A Linear Algebra Framework for Static HPF Code Distribution}, author={C. Ancourt and F. Coelho and F. Irigoin and R. Keryell}, journal={Scientific Programming}, Volume= 6, pages={3--27}, year=1997 } @INPROCEEDINGS{ball:2000, author = {T. Ball and S. K. Rajamani}, title = {Checking Temporal Properties of Software with Boolean Programs}, booktitle = {Workshop on Advances in Verification (with CAV 2000)}, day = {20}, month=jul, address={Chicago}, year = 2000 } @ARTICLE{clarke:2000, author = {E. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith}, title = {Counterexample-guided abstraction refinement}, note={Preliminary version in CAV'2000, LNCS 1855, Springer-Verlag}, journal={JACM}, pages={752--794}, volume=50, number=5, month=sep, year=2003 } @INPROCEEDINGS{lakhnech:2001, author = {Y. Lakhnech and S. Bensalem and S. Berezin and S. Owre}, title = {Incremental Verification by Abstraction}, series = {LNCS 2031}, publisher = {Springer-Verlag}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, address={Genova}, day={2--6}, month=apr, year = 2001 } @InProceedings{bensalem:1999, author = {S. Bensalem and P. Caspi and C. Dumas and C. Parent-Vigouroux}, title = {A methodology for proving control programs with {L}ustre and {P}{V}{S}.}, booktitle = {Proceedings of Dependable Computing for Critical Applications, DCCA-7, San Jose}, year = 1999, month = jan, publisher = {IEEE Computer Society} } @INPROCEEDINGS{pasareanu:2001, AUTHOR = {C. S. P\u{a}s\u{a}reanu and M. B. Dwyer and W. Visser}, TITLE ={Finding Feasible Counter-examples when Model Checking {J}ava Programs}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, series = {LNCS}, volume = {2031}, publisher = {Springer-Verlag}, address={Genova}, day={2--6}, month=apr, YEAR = 2001 } @INPROCEEDINGS{rusu:1999, author = {V. Rusu and E. Singerman}, title = {On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction}, series = {Lecture Notes in Computer Science}, volume = {1579}, publisher = {Springer-Verlag}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = 1999 } @INPROCEEDINGS{nbac-lurette, AUTHOR = {E. Jahier and B. Jeannet and F. Gaucher and F. Maraninchi}, TITLE = {Automatic State Reaching for Debugging Reactive Programs}, BOOKTITLE = {AADEBUG'2003 -- Fifth International Workshop on Automated Debugging}, MONTH=sep, YEAR=2003, ADDRESS={Ghent} } @InProceedings{Saraswat90, author = {Vijay A. Saraswat}, title = {The Paradigm of Concurrent Constraint Programming}, pages = {777--778}, ISBN = {0-262-73090-1}, editor = {Peter {Warren, David H.D.; Szerdei}}, booktitle = {Proceedings of the 7th International Conference on Logic Programming ({ICLP} '90)}, address = {Jerusalem}, month = jun, year = {1990}, publisher = {MIT Press} } @InProceedings{clarke-fmcad02, author={P. Chauhan and E.M. Clarke and J. Kukula and S. Sapra and H. Veith and D. Wang}, title={Automated abstraction refinement for model checking large state spaces using {SAT} based conflict analysis}, booktitle ={Formal Methods in Computer Aided Design (FMCAD)}, address={Portland}, day={6--8}, month= nov, year=2002 } @InProceedings{clarke-cav02, author={E.M. Clarke and A.~Gupta and J.~Kukula and O.~Strichman}, title={{SAT} based abstraction-refinement using {ILP} and machine learning techniques}, booktitle={CAV'02}, address={Copenhagen}, day={27--31}, month=jul, year=2002 } @techreport{spl, author={C. Pichler and M. Siegler and D. Stra{\ss}er and K. Winkelmann and B. Josko and H. Wittke and M. Segelken}, title={D2.1, Specifying Design Properties: The Languages (Version 1.1)}, institution={Safeair Project, IST-1999-10913}, type={Deliverable}, month=sep, year=2001 } @techreport{safeair-d11, author={E. Jahier and N. Halbwachs}, title={D1.1, Test tool specification}, institution={Safeair-II Project, IST-2001-34363}, type={Deliverable}, month=dec, year=2002 } @inproceedings{wolinski97, author={A. Kountouris and C. Wolinski}, title={A Method for the Generation of HDL Code at the RTL level form a High-Level Formal Specification Language}, booktitle={Proceedings of MWSCAS'97}, publisher={IEEE Computer Society Press}, address={Sacramento}, month=aug, year=1997 } @techreport{dea-laure, author={L. Danthony-Gonnord}, title={Du calcul des dur\'ees aux automates symboliques}, type={Master Thesis}, institution={Universit\'es Paris VI/VII}, month=jun, year=2003, note={\verb'www-verimag.imag.fr/~danthony/papers/rapport_dea.ps'} } @TECHREPORT{merchat:these, AUTHOR = {D. Merchat}, TITLE={Réduction du nombre de variables en analyse de relations linéaires}, TYPE = {These}, INSTITUTION= {Université Joseph Fourier}, MONTH= may, YEAR= 2005 } @article{jeannet-fmsd, author={B. Jeannet}, title={Dynamic Partitioning in Linear Relation Analysis, Application to the Verification of Synchronous Programs}, journal={Formal Methods in System Design}, volume= 23, number= 1, pages={5--37}, month=jul, year=2003 } @inproceedings{slap04, author = {L. Gonnord and N. Halbwachs and P. Raymond}, title = {From Discrete Duration Calculus to Symbolic Automata}, booktitle={3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04}, address={Barcelona, Spain}, month=mar, year=2004 } @inproceedings{lamport80a, author = {L. Lamport}, title={``{S}ometime'' is Sometimes ``{N}ot {N}ever'''}, booktitle={Seventh ACM Symposium on Principles of Programming Languages}, month=jan, year=1980 } @techreport{granger:these, author={Ph. Granger}, title={Analyses sémantiques de congruence}, type={PhD Thesis}, institution={Ecole Polytechnique}, month=jul, year=1991 } @inproceedings{cortadella:dcc04, author={R. C. Clarisó and J. Cortadella}, title={Verification of parametric timed circuits using octahedra}, booktitle={Designing correct circuits, DCC'04}, address={Barcelona}, month=mar, year=2004 } @inproceedings{mine:ast01, author ={A. Min\'e}, title = {The Octagon Abstract Domain}, booktitle = {AST 2001 in WCRE 2001}, series = {IEEE}, year = {2001}, month = {October}, pages = {310--319}, publisher = {IEEE CS Press}, } @inproceedings{invest98, author={ S. Bensalem and Y. Lakhnech and S. Owre}, title={ InVeSt : A Tool for the Verification of Invariants}, editor={Alan Hu, Moshe Vardi}, booktitle={International Conference on Computer-Aided Verification , CAV'98}, address={Vancouver, Canada}, publisher={ LNCS vol. 1427 Springer-Verlag}, month= jun, year= 1998 } @inproceedings{mercouroff91, author={N. Mercouroff}, title={An Algorithm for Analyzing Communicating Processes}, booktitle={Mathematical Foundations of Programming Semantics, MFPS'91}, pages={312--325}, year=1991 } @inproceedings{podelski04, author={A. Podelski}, title={ A Complete Method for Synthesis of Linear Ranking Functions}, booktitle={ Verification, Model Checking and Abstract Interpretation, VMCAI'04}, address={Venice, Italy}, month=jan, year=2004 } @article{motzkin, AUTHOR = {Motzkin, Raiffa, Thompson and Thrall}, TITLE = {The double description method}, YEAR = {1953}, JOURNAL = {Theodore S. Motzkin: Selected Papers}, } @techreport{Sunder2000, AUTHOR = {Nookala, Sunder Phani Kumar and Risset, Tanguy}, INSTITUTION = {Irisa}, NUMBER = {1330}, TITLE = {A Library for {Z}-polyhedral Operations}, YEAR = {2000}, MONTH = {Mai}, PAGES = {29}, URL = {http://www.irisa.fr/bibli/publi/pi/2000/1330/1330.html} } @inproceedings{ Fukuda95, AUTHOR = {Komei Fukuda and Alain Prodon}, TITLE = {Double Description Method Revisited}, BOOKTITLE = {Combinatorics and Computer Science}, PAGES = {91-111}, YEAR = {1995}, URL = {citeseer.nj.nec.com/fukuda96double.html} } @INPROCEEDINGS{ Avis98, AUTHOR = {D. Avis}, TITLE = {Computational experience with the reverse search vertex enumeration algorithm}, BOOKTITLE = {Optimization Methods and Software}, YEAR = {1998}, URL = {http://cgm.cs.mcgill.ca/%7Eavis/doc/avis/Av98b.ps} } @misc{ GNU, NOTE = {The GNU Project. http://www.gnu.org}, KEY = {gnu} } @misc{PPL, NOTE = {The Parma Polyhedra Library. http://www.cs.unipr.it/ppl/}, KEY = {PPL} } @techreport{leroux:these, author={J. Leroux}, title={Algorithmique de la vérification des systèmes à compteurs -- Approximation et accélération -- Implémentation dans l'outil {Fast}}, type={PhD Thesis}, institution={Ecole Normale Supérieure de Cachan}, month=dec, year=2003 } @inproceedings{cousot-pldi03, author={B. Blanchet and P. Cousot and R. Cousot and J. Feret and L. Mauborgne and A. Min\'{e} and D. Monniaux and X. Rival}, title={A Static Analyzer for Large Safety-Critical Software}, booktitle={PLDI 2003, ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation}, address={San Diego (Ca.)}, month=jun, year=2003, pages={196--207} } @inproceedings{feautrier96, author={P. Feautrier}, title={Automatic parallelization in the polytope model}, booktitle={The Data Parallel Programming Model: Foundations, HPF Realization, and Scientific Applications}, PUBLISHER = {LNCS 1132, Springer Verlag}, Pages={79--103}, year=1996 } @article{alpha91, author={H. LeVerge and Ch. Mauras and P. Quinton}, title={The ALPHA language and its use for the design of systolic arrays}, journal={Journal of VLSI Signal Processing Systems}, volume=3, number=3, pages={173--182}, month=sep, year=1991 } @inproceedings{mongenet95, author={V. Loechner and C. Mongenet}, title={A toolbox for affine recurrence equations parallelization}, booktitle={International Conference and Exhibition on High-Performance Computing and Networking}, pages={263--268}, month=may, year=1995 } @article{quillere00, author={F. Quiller\'e and S. Rajopadhye}, title={Optimizing Memory Usage in the Polyhedral Model}, journal={ACM TOPLAS}, Volume= 22 , Number= 5 , month=sep, year=2000 } @book{muchnick97, title={Advanced Compiler Design Implementation}, author={S. S. Muchnick}, publisher={Morgan Kaufmann Pub.}, year=1997 } @inproceedings{reps04, author={D. Gopan and F. DiMaio and N. Dor and T. Reps and M. Sagiv}, title={Numeric domains with summarized dimensions}, booktitle={TACAS'04}, address={Barcelona}, year=2004, pages={512--529} } @misc{benchmarkduong, author={F. Irigoin and D. Nguyen}, title={Private communication}, institution={CRI/ENSMP}, year=2004 } @inproceedings{sankaranarayanan05, author={S. Sankaranarayanan and H. Sipma and Z. Manna}, title={Scalable analysis of linear systems using mathematical programming}, booktitle={6th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'05}, editor={R. Cousot}, address={Paris}, publisher={LNCS 3385, Springer Verlag}, month=jan, year=2005 } @inproceedings{sankaranarayanan06, author={S. Sankaranarayanan and M. A. Col\'{o}n and H. Sipma and Z. Manna}, title={Efficient strongly relational polyhedral analysis}, booktitle={7th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'06}, editor={E. A. Emerson, K. S. Namjoshi}, address={Charleston (SC)}, publisher={LNCS 3855,Springer Verlag}, month=jan, year=2006 } @article{allen83, author={J. F. Allen}, title={Maintaining knowledge about temporal intervals}, journal={CACM}, volume=26, number=11, year=1983 } @inproceedings{grafcet:baker:johnson87, author= {A.D. Baker and T.L. Johnson and D.I. Kerpelman and H.A. Sutherland}, title={Grafcet and {SFC} as factory automation standards}, booktitle={American Control Conference}, pages={1725--1730}, year=1987 } @book{grafcet:David:Alla92, author={R. David and H. Alla}, title={Petri nets and {G}rafcet: tools for modelling discrete event systems}, publisher={Prentice Hall}, address={New York}, year=1992 } @inproceedings{val:duquenne, author={N. Duquenne}, title={Maintening safety in automated transit, the {Val} experience}, booktitle={APM Conference}, address={San Francisco}, mont=jul, year=2001 } @inproceedings{val:ferbeck, author={D. Ferbeck}, title={The {VAL} product line}, booktitle={APM'91 Conference}, address={Yokohama}, mont=oct, year=1991 } @inproceedings{jahier:isola04, author={E. Jahier and P. Raymond and P. Baufreton}, title={Case Studies with {L}urette {V}2}, booktitle={First International Symposium on Leveraging Applications of Formal Method, ISoLa 2004}, month=oct, year=2004, address={Paphos, Cyprus} } @inproceedings{scaife:ecrts04, author={N. Scaife and P. Caspi}, title={Integrating model-based design and preemptive scheduling in mixed time- and event-triggered systems}, booktitle={Euromicro conference on Real-Time Systems (ECRTS'04)}, address={Catania, Italy}, month=jun, year=2004 } @book{coq-art, author={Y. Bertot and P. Cast\'eran}, title={Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions}, publisher={Texts in Theoretical Computer Science. An EATCS Series, Springer Verlag}, year=2004 } @INPROCEEDINGS{lucy:cmcs98, AUTHOR = {Paul Caspi and Marc Pouzet}, TITLE = {{A Co-iterative Characterization of Synchronous Stream Functions}}, BOOKTITLE = {Coalgebraic Methods in Computer Science (CMCS'98)}, SERIES = {Electronic Notes in Theoretical Computer Science}, YEAR = 1998, MONTH = {28-29 March}, } @INPROCEEDINGS{maraninchi-morel-acsd04, AUTHOR = {F. Maraninchi and L. Morel}, TITLE = {Arrays and Contracts for the Specification and Analysis of Regular Systems}, BOOKTITLE = {Fourth International Conference on Application of Concurrency to System Design (ACSD)}, MONTH=jun, ADDRESS={Hamilton, Ontario, Canada}, YEAR = 2004 } @inproceedings{caspi:lctes03, author={P. Caspi and A. Curic and A. Maignan and C. Sofronis and S. Tripakis and P. Niebert}, title={From {S}imulink to {S}CADE/{L}ustre to {TTA}: A Layered Approach for Distributed Embedded Applications}, booktitle={LCTES 2003}, address={San Diego, CA}, month=jun, year=2003 } @inproceedings{slam:popl02, author={T. Ball and S. Rajamani}, title={The {SLAM} Project: Debugging System Software via Static Analysis}, booktitle={POPL 2002}, month=jan, year=2002 } @inproceedings{blast:spin03, title={Software Verification with {Blast}}, author={T. A. Henzinger and R. Jhala and R. Majumdar and G. Sutre}, booktitle={10th SPIN Workshop on Model Checking Software}, publisher={LNCS 2648, Springer-Verlag}, year=2003 } @inproceedings{morel02efficient, author = {Lionel Morel}, title = {Efficient Compilation of Array Iterators for {Lustre}}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {65}, issue = {5}, publisher = {Elsevier}, editor = {Florence Maraninchi and Alain Girault and \'Eric Rutten}, year = {2002}} @inproceedings{wolper-boigelot98, author={P. Wolper and B. Boigelot}, title={Verifying Systems with Infinite but Regular State Spaces}, booktitle={CAV'98}, address={Vancouver}, month=jun, year=1998, publisher={LNCS 1427, Springer-Verlag}, pages={88--97} } @PHDTHESIS{boigelot:these, AUTHOR = {B. Boigelot}, TITLE={ Symbolic Methods for Exploring Infinite State Spaces}, SCHOOL= {Université de Li\`ege}, YEAR = 1999 } @inproceedings{fast03, author={S. Bardin and A. Finkel and J. Leroux and L. Petrucci}, title={FAST: Fast Acceleration of Symbolic Transition Systems}, booktitle={CAV'03}, address={Boulder (Colorado)}, month=jul, year=2003, publisher={LNCS 2725, Springer-Verlag}, pages={118--121} } @INPROCEEDINGS{leroux02, AUTHOR = {A. Finkel and J. Leroux}, TITLE = {How to compose {P}resburger-accelerations: Applications to broadcast protocols}, BOOKTITLE = { Proceedings of the 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FSTTCS'2002)}, pages={145--156}, address = {Kanpur, India}, MONTH = Dec , YEAR = 2002, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2556}, } @techreport{halava97decidable, author = {Vesa Halava}, title = {Decidable and Undecidable Problems in Matrix Theory}, number = {TUCS-TR-127}, month = {30,}, year = {1997}, institution = {University of Turku}, url = {citeseer.ist.psu.edu/halava97decidable.html} } @techreport{irigoin2005, author={F. Irigoin}, title={Detecting affine loop invariants using modular static analysis}, number={A/367/CRI}, institution={Centre de Recherche en Informatique, Ecole des Mines de Paris}, month=jul, year=2005 } @inproceedings{wagner04, author={Z. Su and D. Wagner}, title={A class of polynomially solvable range constraints for interval analysis without widenings and narrowings}, booktitle={TACAS'04}, address={Barcelona}, year=2004, pages={280--295} } @article{KarpMiller69, author = {Richard M. Karp and Raymond E. Miller}, title = {Parallel Program Schemata.}, journal = {J. Comput. Syst. Sci.}, volume = {3}, number = {2}, year = {1969}, pages = {147-195}, } @article{Meyer:contracts, author={Bertrand Meyer}, title={Applying``design by contract''}, journal={Computer}, volume=25, number=10, pages={40--51}, month=oct, year=1992 } @inproceedings{henzingerICCAD00, author={T. A. Henzinger and S. Qadeer and S. K. Rajamani}, title={Decomposing refinement proofs using assume-guarantee reasoning}, booktitle={International Conference on Computer-Aided Design (ICCAD)}, publisher={IEEE Computer Society Press}, year=2000, pages={245--252} } @inproceedings{henzingerCAV98, author={T. A. Henzinger and S. Qadeer and S. K. Rajamani}, title={You assume, we guarantee: Methodology and case studies}, booktitle={Tenth International Conference on Computer-Aided Verification (CAV)}, publisher={LNCS 1427, Springer-Verlag}, year=1998, pages={440--451} } @inproceedings{stalmarck-sheeran99, author={M. Sheeran and G. St\aa lmarck}, title={A tutorial on St\aa lmarck's proof procedure for propositional logic}, booktitle={FMCAD'98}, publisher={LNCS 1522, Springer-Verlag}, year=1998 } @inproceedings{clarke-SAT-99, author={A. Biere and A. Cimatti and E. M. Clarke and M. Fujita and Y. Zhu}, title={Symbolic model checking using {SAT} procedures instead of {BDDs}}, booktitle={DAC'99}, pages={317--320}, publisher={IEEE}, year=1999 } @inproceedings{ssm-sas04, author={Sriram Sankaranarayanan and Henny Sipma and Zohar Manna}, title={Constraint-based Linear Relations Analysis}, booktitle={International Symposium on Static Analysis, SAS'2004}, publisher = {LNCS 3148, Springer Verlag}, pages={53--68}, year= 2004 } @inproceedings{avery06, title={Size-change Termination and Bound Analysis}, author={J. Avery}, booktitle={Eighth International Symposium on Functional and Logic Programming, FLOPS 2006}, month=apr, year=2006, address= {Fuji Susono (Japan)} } @article{boussinot98, author={F. Boussinot and J.-F. Susini}, title={ The {S}ugar{C}ubes tool box - a reactive {J}ava framework}, journal={Software Practice and Experience}, volume=28, number=14, pages={1531--1550}, year=1998 } @article{boussinot00, author={F. Boussinot and J.-F. Susini}, title={Java Threads and {S}ugar{C}ubes}, journal={Software Practice and Experience}, volume=30, number=14, pages={545--566}, year=2000 } @article{poigne98, author={A. Poign\'e and M. Morley and O. Maffeis and L. Hoelenderski and R. Budde}, title={The synchronous approach to design reactive systems}, journal={Formal Methods in System Design}, volume=12, pages={163--187}, year=1998 } @inproceedings{pouzet06, author={A. Cohen and M. Duranton and C. Eisenbeis and C. Pagetti and F. Plateau and M. Pouzet}, title={N-{S}ynchronous {K}ahn {N}etworks: a Relaxed Model of Synchrony for Real-Time Systems}, booktitle={ACM International Conference on Principles of Programming Languages (POPL'06)}, address={Charleston (N.C.)}, month=jan, year=2006 } @inproceedings{rml, author={L. Mandel and M. Pouzet}, title={Reactive{ML}, a Reactive Extension to {ML}}, booktitle={ACM International Conference on Principles and Practice of Declarative Programming (PPDP)}, address={Lisboa}, month=jul, year=2005 } @inproceedings{moy05, author={M. Moy and F. Maraninchi and L. Maillet-Contoz}, title={{LusSy}: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level}, booktitle={Fifth International Conference on Application of Concurrency to System Design (ACSD)}, year= 2005 } @article{metropolis:ieee, author={ F. Balarin and Y. Watanabe and H. Hsieh and L. Lavagno and C. Passerone and A. Sangiovanni-Vincentelli}, title={Metropolis: An Integrated Electronic System Design Environment}, journal={Computer --- IEEE Computer Society,}, volume=36, number=4, pages={45--52}, year=2003 } @inproceedings{potop05, author={D. Potop-Butucaru and B. Caillaud}, title={Correct-by-construction asynchronous implementation of modular synchronous specifications}, booktitle={5th Int. Conf. on Applications of Concurrency in System Design, ACSD'05}, address={Saint-Malo (France)}, year=2005 } @inproceedings{benveniste-emsoft04, author={A. Benveniste and B. Caillaud and L. P. Carloni and P. Caspi and A. L. Sangiovanni-Vincentelli}, title={Heterogeneous reactive systems modeling: capturing causality and the correctness of the loosely time-triggered architectures}, booktitle={4th Int. Conf. on Embedded Software, EMSOFT'04}, editor={G. Buttazzo and S. Edwards}, month=sep, year=2004 } @inproceedings{benveniste-tag, author={A. Benveniste and B. Caillaud and L. Carloni and A. Sangiovanni-Vincentelli}, title={Tag Machines}, booktitle={EMSOFT'2005}, month=sep, year=2005 } @inproceedings{baufreton04, author={P. Baufreton}, booktitle={CCCT'04 Computing, Communications and Control Technologies}, address={Austin (Texas)}, month=aug, year=2004, title={Visual notations based on synchronous languages for dynamic validation of GALS systems} } @inproceedings{baufreton-sacres, author={P. Baufreton}, title={{SACRES}: A Step Ahead in the Development of Critical Avionics Applications}, booktitle={Hybrid Systems: Computation and Control: Second International Workshop, HSCC'99}, editor={F.W. Vaandrager and J.H. van Schuppen}, publisher={LNCS 1569, Springer-Verlag}, year=1999 } @inproceedings{gamatie-arinc, author={A. Gamati\'e and T. Gautier}, title={Synchronous Modeling of Avionics Applications using the SIGNAL Language}, booktitle={9th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'2003)}, address={Toronto} , month=may, year= 2003, pages={144--151} } @inproceedings{gamatie-03, author={A. Gamati\'e and T. Gautier}, title={The SIGNAL Approach to the Design of System Architectures}, booktitle={10th IEEE Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2003)}, address={Huntsville (Alabama)}, month=apr, year=2003, pages={80--88} } @article{polychrony, author={P. {Le Guernic} and J.-P. Talpin and J.-C. {Le Lann}}, title={Polychrony for system design}, journal={Journal for Circuits, Systems and Computers, Special Issue on Application Specific Hardware Design}, month=apr, year= 2003 } @techreport{gals, author={D. Chapiro}, title={Globally-Asynchronous Locally-Synchronous Systems}, type={PhD Thesis}, institution={Stanford University}, year=1984 } @inproceedings{talpin-gals05, author={F. Doucet and M. Menarini and I. H. Kr\"uger and R. Gupta and J.-P. Talpin}, title={A verification approach for {GALS} integration of synchronous components}, booktitle={FMGALS'2005}, address={Verona (Italy)}, month=jul, year=2005 } @inproceedings{memocode05, author={N. Halbwachs}, title={A synchronous language at work: the story of {L}ustre}, booktitle={Third ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE'2005}, address={Verona, Italy}, month=jul, year=2005 } @inproceedings{reps06, author={D. Gopan and T. Reps}, title={Lookahead widening}, booktitle={CAV'06}, address={Seattle}, year=2006 } @inproceedings{Tiwari04:CAV, TITLE = {Termination of linear programs}, AUTHOR = {Tiwari, A.}, BOOKTITLE = {Computer-Aided Verification, CAV}, EDITOR = {Alur, R. and Peled, D.}, PAGES = {70--82}, PUBLISHER = {Springer}, SERIES = {LNCS}, VOLUME = {3114}, MONTH = jul, YEAR = 2004 } @article{merchat-fmsd, author={N. Halbwachs and D. Merchat and L. Gonnord}, title={Some ways to reduce the space dimension in polyhedra computations}, journal={Formal Methods in System Design}, volume={29}, number=1, month=jul, year=2006, pages={79--95} } @inproceedings{gonnord-sas, author={L. Gonnord and N. Halbwachs}, title={Combining Widening and Acceleration in Linear Relation Analysis}, booktitle={ 13th International Static Analysis Symposium, SAS'06}, editor={Kwangkeun Yi}, publisher={LNCS 4134, Springer Verlag}, address={Seoul, Korea}, month=aug, year=2006 } @inproceedings{mauborgne-esop05, author={L. Mauborgne and X. Rival}, title={Trace partitioning in abstract interpretation based static analyzers}, booktitle={14th European Symposium on Programming, ESOP 2005}, address={Edinburgh}, month=apr, year=2005 } @inproceedings{sriram-sas06, author={S. Sankaranarayanan and F. Ivan\v{c}i\'c and I. Shlyakhter and A. Gupta}, title={Static analysis in disjunctive numerical domains}, booktitle={ 13th International Static Analysis Symposium, SAS'06}, address={Seoul, Korea}, month=aug, year=2006 } @inproceedings{halbwachs-acsd06, author={N. Halbwachs and L. Mandel}, title={Simulation and verification of asynchronous systems by means of a synchronous model}, booktitle={ Sixth International Conference on Application of Concurrency to System Design, ACSD 2006}, address={Turku, Finland}, month=jun, year=2006 } @inproceedings{peron-vmcai, author={M. P\'eron and N. Halbwachs}, title={An abstract domain extending {D}ifference-{B}ound {M}atrices with disequality constraints}, booktitle={8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07}, editor={B. Cook and A. Podelski}, address= {Nice, France}, month=jan, year=2007 } @inproceedings{EK99, author = {J. Esparza and J. Knoop}, booktitle = {Proceedings von FOSSACS'99}, editor = {W. Thomas}, number = {1578}, pages = {14--30}, series = {Lecture Notes in Computer Science}, title = {An Automata-theoretic Approach to Interprocedural Dataflow Analysis}, year = {1999} } @inproceedings{EP00, author = {J. Esparza and A. Podelski}, booktitle = {Proc. of POPL'2000}, pages = {1--11}, publisher = {ACM Press}, title = {Efficient Algorithms for {\it pre}$^*$ and {\it post}$^*$ on Interprocedural Parallel Flow Graphs}, year = {2000} } @techreport{aadl, author={P. H. Feiler and D. P. Gluch and J. J. Hudak and B. A. Lewis}, title={Embedded System Architecture Analysis Using {SAE} {AADL}}, type={Technical Note CMU/SEI-2004-TN-005}, institution={Carnegie Mellon University}, year=2004 } @article{liulayland, author={C. L. Liu and J. Layland}, title={ Scheduling algorithms for multiprogramming in a hard real-time environment}, journal={JACM}, volume=20, number=1, pages={46--61}, year=1973 } @inproceedings{reps:popl05, title={A framework for numeric analysis of array operations}, author={D. Gopan and T. Reps and M. Sagiv}, booktitle = {Proc. of POPL'2005}, address={Long Beach, CA}, pages={338 -- 350}, year=2005 } @phdthesis{gopan:thesis, author={D. Gopan}, title={Numeric program analysis techniques with applications to array analysis and library summarization}, school={Computer Science Department, University of Wisconsin}, address={Madison, WI}, month=aug, year=2007 } @inproceedings{reps:tacas04, author={D. Gopan and F. Di~Maio and N. Dor and T. Reps and M. Sagiv}, title={Numeric domains with summarized dimensions}, booktitle={TACAS'04}, address={Barcelona}, year=2004, pages={512--529} } @inproceedings{ptolemy, author={J. T. Buck and S. Ha and E. A. Lee and D. G. Messerschmitt}, title={Ptolemy: A Mixed-Paradigm Simulation/Prototyping Platform in C++}, booktitle={C++ At Work Conference}, address={Santa Clara, CA}, mont=nov, year=1991 } @inproceedings{aadl-emsoft, author={E. Jahier and N. Halbwachs and P. Raymond and X. Nicollin and D. Lesens}, title={Virtual Execution of {AADL} Models via a Translation into Synchronous Programs}, booktitle={EMSOFT 2007}, address= {Salzburg, Austria}, mont=oct, year=2007 } @article{cadp, author={H. Garavel and F. Lang and R. Mateescu}, title={An overview of {CADP}2001}, journal={EASST Newsletter}, volume=4, pages={13--24}, month=aug, year=2002, note={Also available as INRIA technical report RT-0254 (December 2001)} } @inproceedings{dill-fmcad96, title={Validity Checking for Combinations of Theories with Equality}, author={C. Barrett and D. Dill and J. Levitt}, booktitle={First International Conference on Formal Methods in Computer-Aided Design, FMCAD}, address={Palo Alto, CA}, year=1996 } @inproceedings{dill-uninterpretedfunctions, author={J. Burch and D. Dill}, title={Automatic verification of microprocessor control}, booktitle={Computer Aided Verification, CAV'94}, address={Stanford, CA}, month=jul, year=1994 } @techreport{gonnord:these, author={L. Gonnord}, title={Accélération abstraite pour l'amélioration de la précision en analyse de relations linéaires}, type={PhD Thesis}, institution={Universit\'e Joseph Fourier (Grenoble 1)}, month=oct, year=2007 } @inproceedings{masdupuy-arrays, author = {F. Masdupuy}, title = {Array abstractions using semantic analysis of trapezoid congruences}, booktitle = {ICS '92: Proceedings of the 6th international conference on Supercomputing}, year = {1992}, isbn = {0-89791-485-6}, pages = {226--235}, location = {Washington, D. C., United States}, doi = {http://doi.acm.org/10.1145/143369.143414}, publisher = {ACM}, address = {New York, NY, USA}, } @InProceedings{Cousot03-ZM, author = {P{.} Cousot}, title = {Verification by Abstract Interpretation}, booktitle = {Proc{.} Int{.} Symp{.} on Verification -- Theory \& Practice -- Honoring Zohar Manna's 64th Birthday}, editor = {N{.} Dershowitz}, address = {Taormina, Italy}, publisher = {\copyright{} Springer-Verlag, Berlin, Germany}, pages = {243--268}, month = {June 29 -- July 4}, year = 2003, } @inproceedings{Iosif-Cav06, author={A. Bouajjani and M. Bozga and P. Habermehl and R. Iosif and P. Moro and T. Vojnar}, title={Programs with Lists are Counter Automata}, booktitle={Computer Aided Verification (CAV 2006)}, publisher={LNCS 4144, Springer Verlag}, pages={517--531}, month=jul, year=2006 } @article{hoare:find, author={C. A. R. Hoare}, title={Proof of a program: FIND}, journal={CACM}, volume=14, number=1, pages={39--45}, year=1971 } @inproceedings{fast06, author={S. Bardin and J. Leroux and G. Point}, title={Tool Presentation: FAST Extended Release}, booktitle={18th Conf. Computer Aided Verification (CAV'2006)}, address={Seattle (Washington)}, publisher={LNCS 4144, Springer-Verlag}, pages={63--66}, year=2006 } @inproceedings{DBLP:conf/pldi/BeyerHMR07, author = {D. Beyer and T. A. Henzinger and R. Majumdar and A. Rybalchenko}, title = {Path invariants}, booktitle = {PLDI 2007}, publisher = {ACM}, editor = {J. Ferrante and K. S. McKinley}, year = {2007}, pages = {300-309}, } @inproceedings{DBLP:conf/pldi/LinP00, author = {Y. Lin and D. A. Padua}, title = {Compiler analysis of irregular memory accesses}, booktitle = {PLDI 2000}, year = {2000}, pages = {157-168}, } @inproceedings{DBLP:conf/popl/GulwaniMT08, author = {S. Gulwani and B. McCloskey and A. Tiwari}, title = {Lifting abstract interpreters to quantified logical domains}, booktitle = {POPL 2008}, year = {2008}, pages = {235-246}, editor = {G. C. Necula and P. Wadler}, publisher = {ACM}, } @inproceedings{DBLP:conf/cav/JhalaM07, author = {R. Jhala and K. L. McMillan}, title = {Array Abstractions from Proofs}, booktitle = {CAV 2007}, year = {2007}, pages = {193-206}, editor = {W. Damm and H. Hermanns}, publisher = {LNCS 4590, Springer Verlag} } @inproceedings{DBLP:conf/cav/LahiriB04, author = {S. K. Lahiri and R. E. Bryant}, title = {Indexed Predicate Discovery for Unbounded System Verification}, booktitle = {CAV 2004}, year = {2004}, pages = {135-147}, editor = {R. Alur and D. Peled}, publisher = {LNCS 3114, Springer Verlag} } @inproceedings{DBLP:conf/cav/LahiriBC03, author = {S. K. Lahiri and R. E. Bryant and B. Cook}, title = {A Symbolic Approach to Predicate Abstraction}, booktitle = {CAV 2003}, year = {2003}, pages = {141-153}, editor = {W. A. Hunt Jr. and F. Somenzi}, publisher = {LNCS 2725, Springer Verlag} } @inproceedings{DBLP:conf/popl/FlanaganQ02, author = {C. Flanagan and S. Qadeer}, title = {Predicate abstraction for software verification}, booktitle = {POPL 2002}, year = {2002}, pages = {191-202}, publisher = {ACM} } @inproceedings{DBLP:conf/vmcai/BradleyMS06, author = {A. R. Bradley and Z. Manna and H. B. Sipma}, title = {What's Decidable About Arrays?}, booktitle = {VMCAI 06}, year = {2006}, pages = {427-442}, editor = {E. A. Emerson and K. S. Namjoshi}, publisher = {LNCS 3855, Springer Verlag} } @inproceedings{whatelse, author={R. Iosif and P. Habermehl and T. Vojnar}, title={What else is decidable about arrays?}, editor = {R. Amadio}, publisher = {LNCS, Springer Verlag}, booktitle = {FOSSACS 2008}, year=2008 } @Misc{ analyseur, author = {{ANALYSER}}, note = {\url{http://pop-art.inrialpes.fr/people/bjeannet/analyzer/}} }