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 43 articles , 1 standard article )

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

1 2 3 next

  1. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2016)
  2. André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
  3. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  4. Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire: McScM: a general framework for the verification of communicating machines (2012) ioport
  5. Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
  6. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2011)
  7. André, Étienne; Fribourg, Laurent: Behavioral cartography of timed automata (2010)
  8. 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
  9. Bozga, Marius; Iosif, Radu; Konečný, Filip: Fast acceleration of ultimately periodic relations (2010) ioport
  10. Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
  11. Harris, William R.; Lal, Akash; Nori, Aditya V.; Rajamani, Sriram K.: Alternation for termination (2010)
  12. Jerson Ortiz, James; Legay, Axel; Schobbens, Pierre-Yves: Memory event clocks (2010)
  13. Kalyanasundaram, Bala; Velauthapillai, Mahe: Learning behaviors of functions (2010)
  14. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  15. Finkel, Alain; Lozes, Étienne; Sangnier, Arnaud: Towards model-checking programs with lists (2009)
  16. Rapin, Nicolas: Symbolic execution based model checking of open systems with unbounded variables (2009)
  17. Bardin, Sébastien; Finkel, Alain; Leroux, Jér^ome; Petrucci, Laure: FAST: Acceleration from theory to practice (2008) ioport
  18. Bouchy, Florent; Finkel, Alain; Leroux, Jér^ome: Decomposition of decidable first-order logics over integers and reals (2008) ioport
  19. Finkel, Alain; Sangnier, Arnaud: Reversal-bounded counter machines revisited (2008)
  20. Walter, David; Little, Scott; Myers, Chris J.; Seegmiller, Nicholas; Yoneda, Tomohiro: Verification of analog/Mixed-signal circuits using symbolic methods (2008) ioport

1 2 3 next

Further publications can be found at: