TREX is a tool for automatic analysis of automata-based models equipped with variables belonging to different infinite/finite domains and with parameters. These models are, at the present time, parametric (continuous-time) timed automata, extended with integer counters and finite-domain variables, and communicating through unbounded lossy FIFO channels and shared variables. This model is a subset of the model taken in high-level languages like SDL.

References in zbMATH (referenced in 47 articles , 1 standard article )

Showing results 1 to 20 of 47.
Sorted by year (citations)

1 2 3 next

  1. Leroux, Jérôme: Flat Petri nets (invited talk) (2021)
  2. Finkel, Alain; Praveen, M.: Verification of flat FIFO systems (2020)
  3. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2016)
  4. André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
  5. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  6. Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire: McScM: a general framework for the verification of communicating machines (2012) ioport
  7. Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
  8. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2011)
  9. André, Étienne; Fribourg, Laurent: Behavioral cartography of timed automata (2010)
  10. Bersani, Marcello M.; Cavallaro, Luca; Frigeri, Achille; Pradella, Matteo; Rossi, Matteo: SMT-based verification of LTL specifications with integer constraints and its application to runtime checking of service substitutability (2010) ioport
  11. Bozga, Marius; Iosif, Radu; Konečný, Filip: Fast acceleration of ultimately periodic relations (2010)
  12. Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
  13. Harris, William R.; Lal, Akash; Nori, Aditya V.; Rajamani, Sriram K.: Alternation for termination (2010)
  14. Jerson Ortiz, James; Legay, Axel; Schobbens, Pierre-Yves: Memory event clocks (2010)
  15. Kalyanasundaram, Bala; Velauthapillai, Mahe: Learning behaviors of functions (2010)
  16. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  17. Bouchy, Florent; Finkel, Alain; Sangnier, Arnaud: Reachability in timed counter systems (2009)
  18. Finkel, Alain; Lozes, Étienne; Sangnier, Arnaud: Towards model-checking programs with lists (2009)
  19. Rapin, Nicolas: Symbolic execution based model checking of open systems with unbounded variables (2009)
  20. Bardin, Sébastien; Finkel, Alain; Leroux, Jérôme; Petrucci, Laure: FAST: Acceleration from theory to practice (2008) ioport

1 2 3 next

Further publications can be found at: