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

Showing results 1 to 20 of 44.
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)
  5. Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
  6. André, Étienne; Fribourg, Laurent: Behavioral cartography of timed automata (2010)
  7. 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)
  8. Bozga, Marius; Iosif, Radu; Konečný, Filip: Fast acceleration of ultimately periodic relations (2010)
  9. Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
  10. Harris, William R.; Lal, Akash; Nori, Aditya V.; Rajamani, Sriram K.: Alternation for termination (2010)
  11. Jerson Ortiz, James; Legay, Axel; Schobbens, Pierre-Yves: Memory event clocks (2010)
  12. Kalyanasundaram, Bala; Velauthapillai, Mahe: Learning behaviors of functions (2010)
  13. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  14. Bouchy, Florent; Finkel, Alain; Sangnier, Arnaud: Reachability in timed counter systems (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)
  18. Bouchy, Florent; Finkel, Alain; Leroux, Jér^ome: Decomposition of decidable first-order logics over integers and reals (2008)
  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)

1 2 3 next

Further publications can be found at: