Nicolas Halbwachs - Main Publications

Back to N. H. Home Page

Books

  • Synchronous programming of reactive systems. N. Halbwachs. Kluwer Academic Pub., 1993 [Abstract and pdf]

  • Détermination automatique de relations linéaires vérifiées par les variables d'un programme. N. Halbwachs. Thèse de 3e cycle, Université Scientifique et Médicale de Grenoble, March 1979. [pdf]

  • Modélisation et analyse du comportement des systèmes informatiques temporisés. N. Halbwachs. Thèse d'Etat, Institut National Polytechnique de Grenoble, June 1984. [pdf]

    Articles

  • Improving WCET Evaluation using Linear Relation Analysis. P. Raymond, C. Maiza, C. Parent-Vigouroux, E. Jahier, N. Halbwachs, F. Carrier, M. Asavoae, and R. Boutonnet. LITES, Leibniz International Transactions on Embedded Systems, vol. 6, nr. 1, pages 02:1, 02:28, 2019. [pdf]

  • Improving the results of program analysis by abstract interpretation beyond the decreasing sequence. R. Boutonnet and N. Halbwachs. Formal Methods in System Design, vol. 53, nr. 3, pp.384--406. December 2018. [doi] [pdf]

  • Specification and Validation of Embedded Systems: A Case Study of a Fault-Tolerant Data Acquisition System with Lustre Programming environment. F. Maraninchi, N. Halbwachs, P. Raymond, C. Parent, and R. K. Shyamasundar. CSI Journal of Computing, Vol 1, nr. 4, pp. 69-85. 2013. [PDF]

  • Some ways to reduce the space dimension in polyhedra computations. N. Halbwachs, D. Merchat and L. Gonnord. Formal Methods in System Design, Vol 29, nr. . July 2006. [Abstract and pdf]

  • Counter-Example Generation in Symbolic Abstract Model-Checking. G. Pace, N. Halbwachs, and P. Raymond. Software Tools for Technology Transfer, Vol.5, nr. 2-3 March 2004 [Abstract and pdf]

  • The synchronous languages 12 years later A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. Proceedings of the IEEE, Vol. 91, Nr. 1, January 2003 [PDF]

  • Automatic Verification of Parameterized Networks of Processes. D. Lesens, N. Halbwachs and P. Raymond. Theoretical Computer Science, Vol. 256, pp. 113-144. 2001 [Abstract and pdf]

  • Verification of Real-Time Systems using Linear Relation Analysis. N. Halbwachs and Y.E. Proy and P. Roumanoff. Formal Methods in System Design, Vol. 11, nr. 2, pp.157-185. August 1997 [Abstract and Postscript]

  • The Algorithmic Analysis of Hybrid Systems. 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. Theoretical Computer Science B, Vol. 138, pp.3-34. January 1995. Postscript

  • Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre. N. Halbwachs, F. Lagnier and C. Ratel. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems. September 1992. [Abstract and Postscript]

  • Minimal state graph generation. A. Bouajjani, J. C. Fernandez, N. Halbwachs, P. Raymond and C. Ratel. Science of Computer Programming, vol. 18, pp. 247--269. 1992 [Abstract and Postscript]

  • An experience in proving regular networks of processes by modular model checking. N. Halbwachs, F. Lagnier and Ch. Ratel. Acta Informatica, vol. 29, nr. 6/7, pp. 523-543, 1992 [Abstract]

  • The synchronous dataflow programming language Lustre. N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud. Proceedings of the IEEE, vol. 79, nr. 9. September 1991. [Abstract and Postscript]

  • A functional model for describing and reasoning about time behaviour of computing systems. P. Caspi and N. Halbwachs. Acta Informatica, vol. 22, pp. 595-697, 1986

  • Describing and reasoning about circuits behaviour by means of time functions. P. Amblard, P. Caspi and N. Halbwachs. IEE Proceedings-E, vol. 133, nr. 5, pp. 271-275. September 1986.

    Conference Papers

  • Disjunctive relational abstract interpretation for interprocedural program analysis. R. Boutonnet and N. Halbwachs. VMCAI 2019, 20th International Conference on Verification, Model Checking, and Abstract Interpretation. Cascais/Lisbon, Portugal, January 2019. [pdf]

  • When the worst-case execution time estimation gains from the application semantics. A. Bonenfant, F. Carrier, H. Cassé, P. Cuenot, D. Claraz, N. Halbwachs, H. Li, C. Maiza, M. De Michiel, V. Mussot, C. Parent-Vigouroux, I. Puaut, P. Raymond, E. Rohou, P. Sotin. 8th European Congress on Embedded Real-Time Software and Systems, ERTS2 2016. Toulouse, France, January 2016. [Abstract and PDF]

  • Engineering Functional Requirements of Reactive Systems using Synchronous Languages. E. Jahier, N. Halbwachs, P. Raymond. International Symposium on Industrial Embedded Systems, SIES'13. Porto, Portugal, June 2013 [Abstract and PDF]

  • When the decreasing sequence fails N. Halbwachs and J. Henry. SAS 2012. Deauville, France, September 2012 [Abstract and PDF]

  • An analysis of permutations in arrays V. Perrelle and N. Halbwachs. VMCAI 2010 Madrid, Spain, January 2010 [Abstract and PDF]

  • Synchronous Modeling and Validation of Priority Inheritance Schedulers E. Jahier, N. Halbwachs and P. Raymond FASE'09 York, U.K., March 2009 [Abstract  and PDF]

  • Discovering Properties about Arrays in Simple Programs N. Halbwachs and M. Péron PLDI 2008 Tucson (Az.), June 2008 [Abstract  and PDF]

  • On the timed automata-based verification of Ravenscar systems I. Ober and N. Halbwachs 13th International Conference on Reliable Software Technologies - Ada-Europe 2008 Venice, June 2008 [Abstract and PDF]

  • Virtual Execution of AADL Models via a Translation into Synchronous Programs E. Jahier, N. Halbwachs, P. Raymond, X. Nicollin and D. Lesens 7th ACM & IEEE international conference on Embedded software - EMSOFT 2007 Salzburg, Austria, October 2007. [Abstract and PDF]

  • An abstract domain extending Difference-Bound Matrices with disequality constraints M. Péron and N. Halbwachs {8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07 Nice, France, January 2007. [Abstract and PDF]

  • Combining Widening and Acceleration in Linear Relation Analysis. L. Gonnord and N. Halbwachs. 13th International Static Analysis Symposium, SAS'06. Seoul, Korea, August 2006. [Abstract and PDF]

  • Simulation and verification of asynchronous systems by means of a synchronous model. N. Halbwachs and L. Mandel. Sixth International Conference on Application of Concurrency to System Design, ACSD 2006. Turku, Finland, June 2006 [Abstract and PDF]

  • A Synchronous Language at Work: the Story of Lustre. N. Halbwachs. Third ACM-IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE'2005 , Verona, Italy, July 2005 . [Abstract and PDF]

  • From Discrete Duration Calculus to Symbolic Automata L. Gonnord, N. Halbwachs, and P. Raymond 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04 Barcelona, Spain, March 2003. [Abstract and PDF]

  • Cartesian factoring of polyhedra in linear relation analysis N. Halbwachs, D. Merchat, and C. Parent-Vigouroux Static Analysis Symposium, SAS'03 LNCS 2694, Springer Verlag, June 2003. [Abstract and PDF]

  • Synchronous modeling of asynchronous systems N. Halbwachs and S. Baghdadi EMSOFT'02, LNCS 2491, Springer Verlag, October 2002. [Abstract and Postscript]

  • Counter-example generation in symbolic abstract model-checking. G. Pace, N. Halbwachs, and P. Raymond. 6th International Workshop on Formal Me thods for Industrial Critical Systems, FMICS'2001, Paris, July 2001, Inria. [Abstract and Postscript]

  • Stability of Discrete Sampled Systems. N. Halbwachs, J.-F. Héry, J.-C. Laleuf, and X. Nicollin. FTRTFT'200, Pune (India), September 2000. LNCS 1926, Springer Verlag. [Abstract and Postscript]

  • Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing. N. Halbwachs and P. Raymond. ASIAN'99, Asian Computing Science Conference Phuket (Thailand), December 1999. LNCS 1742, Springer Verlag. [Abstract and Postscript]

  • Dynamic Partitioning in Analyses of Numerical Properties. B. Jeannet, N. Halbwachs, and P. Raymond. Static Analysis Symposium, SAS'99 Venezia (Italy), September 1999. [Abstract and Postscript]

  • Synchronous programming of reactive systems, a tutorial and commented bibliography. N. Halbwachs. Tenth International Conference on Computer-Aided Verification, CAV'98 Vancouver (B.C.), LNCS 1427, Springer Verlag, June 1998. [Abstract and Postscript]

  • Automatic Testing of Reactive Systems. P. Raymond, D. Weber, X. Nicollin, and N. Halbwachs. 19th IEEE Real-Time Systems Symposium. Madrid, Spain, December 1998. [Abstract and Postscript]

  • Automatic Verification of Parameterized Linear Networks of Processes. D. Lesens, N. Halbwachs, and P. Raymond. 24th ACM Symposium on Principles of Programming Languages, POPL'97. Paris, January 1997. [Abstract and Postscript]

  • Compiling ARGOS into Boolean Equations F. Maraninchi and N. Halbwachs Proc. 4th Int. School and Symposium ``Formal Techniques in Real Time and Fault Tolerant Systems'' (FTRTFT). Uppsala, Sweden, 1996. [Abstract and Postscript] ]

  • Compositional semantics of non deterministic synchronous languages. F. Maraninchi and N. Halbwachs. European Symposium on Programming, ESOP'96. Linkoping, April 1996. [Abstract and Postscript]

  • On the symbolic analysis of combinational loops in circuits and synchronous programs. N. Halbwachs and F. Maraninchi. Euromicro'95, Como (Italy). September 1995. [Abstract and Postscript]

  • About synchronous programming and abstract interpretation. N. Halbwachs. International Symposium on Static Analysis, SAS'94, LNCS 864, Springer Verlag. Namur (Belgium), September 1994. (Extended version published in Science of Computer Programming) [Abstract and Postscript]

  • Verification of linear hybrid systems by means of convex approximations. N. Halbwachs, Y.-E. Proy and P. Raymond. International Symposium on Static Analysis, SAS'94, LNCS 864, Springer Verlag. Namur (Belgium), September 1994. [Abstract and Postscript]

  • Synchronous observers and the verification of reactive systems. N. Halbwachs, F. Lagnier and P. Raymond. Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Workshops in Computing, Springer Verlag. Twente, June 1993. [Abstract and Postscript]

  • An executable temporal logic to express safety properties and its connection with the language Lustre. N. Halbwachs, J.-C. Fernandez and A. Bouajjanni. Sixth International Symp. on Lucid and Intensional Programming, ISLIP'93, Quebec, April 1993. [Abstract and Postscript]

  • Delay analysis in synchronous programs. N. Halbwachs. Fifth Conference on Computer-Aided Verification}, CAV'93, Elounda (Greece), LNCS 697, Springer Verlag. July 1993. [Abstract and Postscript]

  • An implementation of three algorithms for timing verification based on automata emptiness. R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs and H. Wong-Toi. 13th IEEE Real-Time Systems Symposium, Phoenix (Az.), December 1992. [pdf]

  • Minimization of timed transition systems. R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, H. Wong-Toi. CONCUR'92, Stony Brook (NY), June 1992. [pdf]

  • Generating Efficient Code From Data-Flow Programs. N. Halbwachs, P. Raymond and C. Ratel. Third International Symposium on Programming Language Implementation and Logic Programming, PLILP'91. Passau, August 1991. [Abstract and Postscript]

  • Pollux, a Lustre-based hardware design environment. F. Rocheteau and N. Halbwachs. Conference on Algorithms and Parallel VLSI Architectures II. Chateau de Bonas, June 1991. [Abstract and Postscript]

  • Implementing reactive programs on circuits, a hardware implementation of Lustre. F. Rocheteau and N. Halbwachs. Rex Workshop on Real-Time: Theory and Practice. DePlasmolen (Netherlands), LNCS 600, Springer Verlag, June 1991.

  • Minimal model generation. A. Bouajjani, J-C. Fernandez, N. Halbwachs. Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990.

  • Specifying, Programming and Verifying Real-Time Systems, using a synchronous declarative language. N. Halbwachs, D. Pilaud, F. Ouabdesselam and A.C. Glory. Workshop on automatic verification methods for finite state systems, Grenoble, LNCS 407, Springer Verlag. June 1989.

  • From a synchronous declarative language to a temporal logic dealing with multiform time. D. Pilaud and N. Halbwachs. Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems,, Warwick, LNCS 331, Springer Verlag. September 1988.

  • Lustre: a declarative language for programming synchronous systems. P. Caspi, D. Pilaud, N. Halbwachs and J. Plaice. 14th ACM Conf. on Principles of Programming Languages. Munich, January 1987.

  • Use of a real-time declarative language for systolic array design and simulation. N. Halbwachs and D. Pilaud. International Workshop on Systolic Arrays, Oxford, July 1986.

  • Automatic control systems programming using a real-time declarative language. J-L. Bergerand, P. Caspi, N. Halbwachs and J. Plaice. IFAC/IFIP Symp. 'SOCOCO 86, Graz (Autriche), May 1986.

  • Outline of a real-time data-flow language. J-L. Bergerand, P. Caspi, N. Halbwachs, D. Pilaud and E. Pilaud. Real-Time Symposium, San Diego, December 1985.

  • Describing and reasoning about circuits behaviour by means of time functions. P. Amblard, P. Caspi and N. Halbwachs. 1985 Conference on Computer Hardware Description Languages, Tokyo, August 1985.

  • Specification and formal validation of distributed systems, the real-time approach. J-L. Bergerand, P. Caspi and N. Halbwachs. IEE Conference Control 85. Cambridge, July 1985.

  • An approach to real-time systems modeling. P. Caspi and N. Halbwachs. International Conference on Distributed Computing Systems, Miami, October 1982.

  • Algebra of events, A model for parallel and real-time systems. P. Caspi and N. Halbwachs International Conference on Parallel Processing, Bellaire (Michigan), August 1982.

  • Automatic discovery of linear restraints among variables of a program. P. Cousot and N. Halbwachs. 5th ACM Symposium on Principles of Programming Languages, Tucson (Az), January 1978,.