Publications of Stavros Tripakis


You may also want to check: the list at the DBLB server (it does not list all papers, though); the entry at Google scholar; the entry at Microsoft academic search.
Copyright note: The papers provided here can be accessed for personal use. They have been provided in order to ensure timely dissemination of research results. Copyright and all rights on these papers are retained by authors or by other copyright holders (e.g., publishers). All persons copying this information are expected to adhere to the terms and constraints invoked by each copyright. These works may not be redistributed without the explicit permission of the copyright holder.

Conference/Workshop Papers

  1. V. Preoteasa and S. Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014.

  2. J. Reineke and S. Tripakis. Basic Problems in Multi-View Modeling. TACAS 2014.

  3. A. Iannopollo, P. Nuzzo, S. Tripakis, and A. Sangiovanni-Vincentelli. Library-Based Scalable Refinement Checking for Contract-Based Design. DATE 2014.

  4. D. Broman, C. Brooks, L. Greenberg, E. A. Lee, S. Tripakis, M.Wetter, and M. Masin. Determinate Composition of FMUs for Co-Simulation. EMSOFT 2013.

  5. M. Persson, M. Toerngren, A. Qamar, J. Westman, M. Biehl, S. Tripakis, H. Vangheluwe, and J. Denil. A Characterization of Integrated Multi-View Modeling for Embedded Systems. EMSOFT 2013.

  6. C. Stergiou, S. Tripakis, E. Matsikoudis, E. A. Lee. On the Verification of Timed Discrete-Event Models. FORMATS 2013.

  7. S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. International SPIN Symposium on Model Checking of Software, 2013.

  8. P. Derler, E. A. Lee, M. Toerngren, and S. Tripakis. Cyber-physical system design contracts. In ACM/IEEE 4th International Conference on Cyber-Physical Systems - ICCPS 2013. Extended version available as technical report.

  9. D. Broman, E.A. Lee, S. Tripakis, and M. Toerngren. Viewpoints, Formalisms, Languages, and Tools for Cyber-Physical Systems. In 6th International Workshop on Multi-Paradigm Modeling (MPM12), 2012.

  10. A. Ghosal, R. Limaye, K. Ravindran, S. Tripakis, A. Prasad, G. Wang, T. Tran, and H. Andrade. Static Dataflow with Access Patterns: Semantics and Analysis. In Design Automation Conference (DAC). ACM, 2012.

  11. S. Tripakis, H. Andrade, A. Ghosal, R. Limaye, K. Ravindran, G. Wang, G. Yang, J. Kornerup, and I. Wong. Correct and non-defensive glue design using abstract models. In CODES+ISSS 2011. ACM, 2011.

  12. M. Geilen, S. Tripakis and M. Wiggers. The Earlier the Better: A Theory of Timed Actor Interfaces. HSCC 2011. Extended version available as technical report.

  13. E. A. Lee and S. Tripakis. Modal Models in Ptolemy. In EOOLT 2010. Voted Best Paper.

  14. S. Tripakis, C. Stergiou and R. Lublinerman. Checking Equivalence of SPMD Programs Using Non-Interference. Shorter version appears at HotPar 2010.

  15. S. Tripakis, B. Lickly, T.A. Henzinger, and E.A. Lee. On Relational Interfaces. In EMSOFT'09. PDF.

  16. K. Bae, P. Csaba Olveczky, T.H. Feng, and S. Tripakis. Verifying Ptolemy II Discrete-Event Models using Real-Time Maude. In Formal Methods and Software Engineering: 11th InternationalConference on Formal Engineering Methods (ICFEM09), 2009. PDF.

  17. M-K. Leung, T. Mandl, E.A. Lee, E. Latronico, C. Shelton, S. Tripakis, and B. Lickly. Scalable Semantic Annotation using Lattice-based Ontologies. In 12th Intl. Conf. Model Driven Engineering Languages and Systems (MODELS 2009), 2009. ACM SIGSOFT Distinguished Paper Award. link.

  18. S. Tripakis. A Combined On-line/Off-line Framework for Black-Box Fault Diagnosis. In RV'09. PDF.

  19. S. Tripakis, A. Benveniste, P. Caspi, C. Pinello, A. Sangiovanni-Vincentelli, and C. Sofronis. Correct and Efficient Implementations of Synchronous Models on Asynchronous Execution Platforms. In 2nd Exploiting Concurrency Efficiently and Correctly Workshop. PDF.

  20. P. Caspi, A. Benveniste, R. Lublinerman, and S. Tripakis. Actors without Directors: a Kahnian View of Heterogeneous Systems. In HSCC'09. PDF. Also see the extended technical report.

  21. R. Lublinerman, C. Szegedy and S. Tripakis. Modular Code Generation from Synchronous Block Diagrams --- Modularity vs. Code Size. In POPL'09. PDF.

  22. R. Lublinerman and S. Tripakis. Translating Data Flow to Synchronous Block Diagrams. In ESTIMedia'08. PDF.

  23. R. Lublinerman and S. Tripakis. Modular Code Generation from Synchronous Block Diagrams. In 1st Intl. Workshop on Numerical Abstractions for Software Verification (NSV'08). This paper summarizes in an intuitive manner, with lots of examples, the DATE'08 and RTAS'08 papers below. PDF.

  24. N. Abed, S. Tripakis and J-M. Vincent. Resource-Aware Verification Using Randomized Exploration of Large State Spaces. In SPIN'08. PDF.

  25. R. Lublinerman and S. Tripakis. Modular Code Generation from Triggered and Timed Block Diagrams. In Real-Time and Embedded Technology and Applications Symposium (RTAS'08). PDF.

  26. R. Lublinerman and S. Tripakis. Modularity vs. Reusability: Code Generation from Synchronous Block Diagrams. In Design, Automation and Test in Europe (DATE'08). PDF.

  27. M. Di Natale, A. Benveniste, P. Caspi, C. Pinello, A. Sangiovanni-Vincentelli and S. Tripakis. Applying LTTA to guarantee flow of data requirements in distributed systems using Controller Area Network. In DATE'08 Workshop on Dependable Software Systems. PDF.

  28. A. Benveniste, P. Caspi, M. Di Natale, C. Pinello, A. Sangiovanni-Vincentelli and S. Tripakis. Loosely Time-Triggered Architectures based on Communication by Sampling. In 7th ACM Intl. Conf. on Embedded Software (EMSOFT'07).

  29. F. Cassez, S. Tripakis and K. Altisen. Synthesis of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete Event Systems. In TASE'07. Postscript.

  30. F. Cassez, S. Tripakis and K. Altisen. Sensor Minimization Problems with Static and Dynamic Observers for Fault Diagnosis. In ACSD'07. PDF.

  31. C. Sofronis, S. Tripakis and P. Caspi. A Memory-Optimal Buffering Protocol for Preservation of Synchronous Semantics under Preemptive Scheduling. In 6th ACM Intl. Conf. on Embedded Software (EMSOFT'06). PDF.

  32. A. Benveniste, B. Caillaud, L. Carloni, P. Caspi, A. Sangiovanni-Vincentelli and S. Tripakis. Communication by Sampling in Time-Sensitive Distributed Systems. In 6th ACM Intl. Conf. on Embedded Software (EMSOFT'06).

  33. K. Altisen, F. Cassez and S. Tripakis. Monitoring and Fault Diagnosis with Digital Clocks. In ACSD'06. Postscript.

  34. M. Krichen and S. Tripakis. State identification problems for finite-state transducers. In FATES-RV'06. Available as VERIMAG Technical Report TR-2005-5.

  35. M. Krichen and S. Tripakis. Interesting properties of the conformance relation tioco. In ICTAC'06.

  36. J.-F. Condotta, G. Ligozat, M. Saade, and S. Tripakis. Ultimately Periodic Simple Temporal Problems (UPSTPs). 13th Intl. Symposium on Temporal Representation and Reasoning (TIME06). PDF.

  37. S. Tripakis. Decentralized observation problems. CDC-ECC'05 (invited paper). PDF.

  38. S. Bensalem, D. Peled, H. Qu and S. Tripakis. Generating path conditions for timed systems. In IFM'05. PDF.

  39. S. Tripakis, C. Sofronis, N. Scaife and P. Caspi. Semantics-preserving and memory-efficient implementation of inter-task communication under static-priority or EDF schedulers. In 5th ACM Intl. Conf. on Embedded Software (EMSOFT'05). PDF.

  40. J-F. Condotta, G. Ligozat and S. Tripakis. Ultimately periodic qualitative constraint networks for spatial and temporal reasoning. In ICTAI'05. PDF.

  41. K. Altisen and S. Tripakis. Implementation of timed automata: an issue of semantics or modeling?. In FORMATS'05. A previous version of this paper is available as VERIMAG Technical Report TR-2005-12.

  42. S. Tripakis. Two-phase distributed observation problems. In 5th Intl. Conf. on Application of Concurrency to System Design (ACSD'05). See the VERIMAG Technical Report TR-2004-14.

  43. M. Krichen and S. Tripakis. State identification problems for timed automata. In 17th IFIP Intl. Conf. on Testing of Communicating Systems (TestCom'05). PDF.

  44. M. Krichen and S. Tripakis. An Expressive and Implementable Formal Framework for Testing Real-Time Systems. In 17th IFIP Intl. Conf. on Testing of Communicating Systems (TestCom'05). PDF. A previous version of this paper (not containing the BRP case study) is available as VERIMAG Technical Report TR-2004-13.

  45. N. Scaife, C. Sofronis, P. Caspi, S. Tripakis and F. Maraninchi. Defining and translating a "safe" subset of Simulink/Stateflow into Lustre. In EMSOFT'04. Available as VERIMAG Technical Report TR-2004-16.

  46. M. Krichen and S. Tripakis. Real-time testing with timed automata testers and coverage criteria. In Joint conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT'04). Available as VERIMAG Technical Report TR-2004-15.

  47. M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. In SPIN'04 Workshop on Model Checking Software. PDF.

  48. S. Bensalem, M. Bozga, M. Krichen and S. Tripakis. Testing conformance of real-time applications with automatic generation of observers. In Runtime Verification 2004. PDF.

  49. P. Caspi, A. Curic, A. Maignan, C. Sofronis and S. Tripakis. Translating Discrete-Time Simulink to Lustre. In EMSOFT'03, 2003. Technical report in PDF.

  50. P. Caspi, A. Curic, A. Maignan, C. Sofronis, S. Tripakis and P. Niebert. From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications. In ACM-SIGPLAN Languages, Compilers, and Tools for Embedded Systems (LCTES'03), 2003. Postscript.

  51. S. Tripakis. Folk theorems on the determinization and minimization of timed automata. In FORMATS, 2003. PDF.

  52. S. Tripakis. Automated Module Composition. In TACAS, 2003. PDF.

  53. S. Tripakis. Fault Diagnosis for Timed Automata. In FTRTFT, 2002. Improved version in PDF.

  54. S. Tripakis. Description and Schedulability Analysis of the Software Architecture of an Automated Vehicle Control System. In EMSOFT, 2002. Extended version in PDF.

  55. A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J.P. Talpin and S. Tripakis. A Protocol for Loosely Time-Triggered Architectures. In EMSOFT, 2002. Available as INRIA Irisa Research Report here.

  56. S. Tripakis. Automated Composition of Module Chains. In ETAPS'02 Workshop on Software Composition, 2002. Volume 65, issue 4 of ENTCS, Elsevier.

  57. S. Tripakis. Decentralized Control of Discrete Event Systems with Bounded or Unbounded Delay Communication. In 6th International Workshop on Discrete Event Systems, 2002. Extended version in PDF.

  58. K. Altisen and S. Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. PDF.

  59. A. Puri and S. Tripakis. Algorithms for Routing with Multiple Constraints. In AIPS'02 Workshop on Planning and Scheduling using Multiple Criteria, 2002. Postscript.

  60. S. Tripakis. Undecidable Problems of Decentralized Observation and Control. In IEEE Conference on Decision and Control, 2001. Extended version in PDF.

  61. J. Ko, R. Sengupta, S. Tripakis and M. Zennaro. A Service Network Architecture for a Multi-Vehicle Search Mission. In IEEE Conference on Decision and Control, 2001. PDF.

  62. S. Tripakis and S. Yovine. Timing Analysis and Code Generation of Vehicle Control Software using Taxys. In Workshop on Runtime Verification, 2001. Postscript.

  63. A. Puri, S. Tripakis and P. Varaiya. Problems and Examples of Decentralized Observation and Control for Discrete Event Systems. In Symposium on the Supervisory Control of Discrete Event Systems, 2001. Also in B. Caillaud, P. Darondeau, L. Lavagno and X. Xie, editors, Synthesis and Control of Discrete Event Systems, Kluwer Academic Publishers, 2002. Postscript.

  64. R. Attias, D. Lee, A. Puri and S. Tripakis. A Token-Ring Medium-Access Control Protocol with Quality of Service Guarantees for Wireless Ad-hoc Networks. In ACM MobiCom, 2001. Extended version in Postscript.

  65. P. Niebert, S. Tripakis and S. Yovine. Minimum-Time Reachability for Timed Automata. In Mediterranean Conference on Control and Automation, 2000. Postscript.

  66. O. Botchkarev and S. Tripakis. Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations. In Hybrid Systems: Computation and Control, 2000. Lecture Notes in Computer Science, Springer-Verlag.

  67. K. Altisen, G. Goessler, A. Pnueli, J. Sifakis, S. Tripakis and S. Yovine. A Framework for Scheduler Synthesis. In IEEE Real-Time Systems Symposium, RTSS'99, 1999. Postscript.

  68. S. Tripakis. Solving Cyclic Constraints. In Workshop on Real-Time Constraints, RTC'99, 1999. Postscript.

  69. S. Tripakis and K. Altisen. On-the-Fly Controller Synthesis for Discrete and Timed Systems. In World Congress on Formal Methods, FM'99, 1999. Postscript.

  70. M. Bozga, O. Maler and S. Tripakis. Efficient Verification of Timed Automata using Dense and Discrete Time Semantics. In CHARME'99, 1999. Postscript.

  71. S. Tripakis. Verifying Progress in Timed Systems. In ARTS'99, Bamberg, Germany, 1999. Postscript.

  72. S. Tripakis. Timed Diagnostics for Reachability Properties. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'99, Amsterdam, Holland, 1999. Postscript.

  73. S. Tripakis and S .Yovine. Verification of the Fast-Reservation Protocol with Delayed Transmission using the tool Kronos. In 4th IEEE Real-Time Technology and Applications Symposium, RTAS'98, Denver, Colorado, 1998. Postscript.

  74. M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. KRONOS: a model-checking tool for real-time systems. In Computer Aided Verification, CAV'98, 1998. Postscript.

  75. C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'98, Lisbon, Portugal, LNCS 1384, 1998. Postscript.

  76. S. Bornot, J. Sifakis and S. Tripakis. Modeling Urgency in Timed Systems. In Compositionality: the significant difference, COMPOS'97, LNCS 1536. Postscript.

  77. A. Bouajjani, S. Tripakis and S. Yovine. On-the-fly Symbolic Model checking for Real-time Systems. In 18th IEEE Real-Time Systems Symposium, RTSS'97, San Francisco, CA, 1997. Postscript.

  78. S. Tripakis and C. Courcoubetis. Probabilistic model checking: formalisms and algorithms for discrete and real-time systems. In summer school Verification of Digital and Hybrid Systems, Antalya, Turkey, 1997. Postscript.

  79. S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Computer-Aided Verification, CAV'96, Rutgers, NJ, LNCS 1102, 1996. PDF.

  80. C. Daws, A. Olivero, S. Tripakis and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, LNCS 1066, 1996. PDF.

  81. S. Tripakis and C. Courcoubetis. Extending PROMELA and SPIN for Real Time. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'96, Passau, Germany, LNCS 1055, 1996. PDF.

Journal Papers

  1. S. Tripakis, C. Stergiou, C. Shaver, and E.A. Lee. A Modular Formal Semantics for Ptolemy. Mathematical Structures in Computer Science. Link.

  2. S. Tripakis, B. Lickly, T.A. Henzinger, and E.A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS. pre-print.

  3. S. Tripakis, D. Bui, M. Geilen, B. Rodiers, and E.A. Lee. Compositionality in Synchronous Data Flow: Modular Code Generation from Hierarchical SDF Graphs. ACM TECS. pre-print.

  4. K. Bae, P. Csaba Olveczky, T. H. Feng, E. A. Lee, and S. Tripakis. Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude. To appear in Science of Computer Programming.

  5. S. Tripakis. Checking Timed Buchi Automata Emptiness on Simulation Graphs. In ACM Transactions on Computational Logic. PDF.

  6. S. Tripakis, C. Pinello, A. Benveniste, A. Sangiovanni-Vincentelli, P. Caspi and M. Di Natale. Implementing Synchronous Models on Loosely Time Triggered Architectures. In IEEE Transactions on Computers. PDF.

  7. F. Cassez and S. Tripakis. Fault Diagnosis with Static or Dynamic Observers. In Fundamenta Informaticae. PDF.

  8. P. Caspi, N. Scaife, C. Sofronis and S. Tripakis. Semantics-Preserving Multitask Implementation of Synchronous Programs. In ACM Trans. Embedded Computing Systems, 7(2), 2008. PDF.

  9. M. Krichen and S. Tripakis. Conformance Testing for Real-Time Systems. In Formal Methods in System Design. PDF.

  10. S. Bensalem, D. Peled, H. Qu and S. Tripakis. Automatic Generation of Path Conditions for Concurrent Timed Systems. In Theoretical Computer Science. PDF.

  11. S. Tripakis. Folk theorems on the determinization and minimization of timed automata. Information Processing Letters, Vol. 99, Issue 6, 30 Sep 2006, Pg 222-226, PDF.

  12. S. Tripakis, C. Sofronis, P. Caspi and A. Curic. Translating Discrete-Time Simulink to Lustre. In ACM Transactions on Embedded Computing Systems, 4(4), 2005. Technical report in PDF.

  13. S. Tripakis, S. Yovine and A. Bouajjani. Checking Timed Buchi Automata Emptiness Efficiently. In Formal Methods in System Design, 26(3):267-292, May 2005. PDF.

  14. S. Tripakis. Undecidable Problems in Decentralized Observation and Control for Regular Languages. In Information Processing Letters, Volume 90, Issue 1, Pages 21-28 (15 April 2004). See the full version of CDC'01 paper.

  15. S. Tripakis. Decentralized Control of Discrete Event Systems with Bounded or Unbounded Delay Communication. In IEEE Transactions on Automatic Control, Special Issue on Networked Control Systems. Volume 49, Number 9, September 2004. Available as VERIMAG Technical Report TR-2004-26.

  16. J. Sifakis, S. Tripakis and S. Yovine. Building Models of Real-Time Systems from Application Software. Proceedings of the IEEE, January 2003.

  17. S. Tripakis and S. Yovine. Analysis of Timed Systems using Time-abstracting Bisimulations. In Formal Methods in System Design, 18(1):25-68, January 2001. Kluwer Academic Publishers. Postscript.


Edited Volumes

  1. U. Fahrenberg and S. Tripakis, editors. Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2011, Aalborg University, Denmark, September 21-23, 2011, LNCS. Springer.

  2. L. Carloni and S. Tripakis, editors. Proceedings of the 10th ACM & IEEE International Conference on Embedded Software, EMSOFT 2010, Scottsdale, AZ, October 25-27, 2010. ACM, 2010.

Book Chapters

  1. S. Tripakis and T. Dang. Modeling, Verification and Testing using Timed and Hybrid Automata. In P. Mosterman and G. Nicolescu, editors, Model-Based Design for Embedded Systems. CRC Press, 2009. PDF.

  2. F. Cassez and S. Tripakis. Monitoring, Fault-Diagnosis and Testing. In C. Jard and O.H. Roux, editors, Communicating Embedded Systems -- Formal Methods. Hermes, France, 2009.

  3. P. Caspi, P. Raymond and S. Tripakis. Synchronous Programming. In I. Lee, J. Leung, and S. Son, editors, Handbook of Real-Time and Embedded Systems. Chapman & Hall, 2007. PDF.

  4. A. Puri, S. Tripakis, and P. Varaiya. Problems and Examples of Decentralized Observation and Control for Discrete Event Systems. In B. Caillaud, P. Darondeau, L. Lavagno, and X. Xie, editors, Synthesis and Control of Discrete Event Systems. Kluwer, 2001. Gzipped PS.


Ph.D. Thesis

S. Tripakis. The analysis of timed systems in practice, December 1998. Universite Joseph Fourier, Grenoble, France.

  1. In full (about 200 pages).

  2. In half (about 100 pages, saves paper).

  3. Slides (in Powerpoint format).


Technical reports and other documents