TREX

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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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

Showing results 1 to 20 of 45.
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)
  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. Bouchy, Florent; Finkel, Alain; Sangnier, Arnaud: Reachability in timed counter systems (2009)
  16. Finkel, Alain; Lozes, Étienne; Sangnier, Arnaud: Towards model-checking programs with lists (2009)
  17. Rapin, Nicolas: Symbolic execution based model checking of open systems with unbounded variables (2009)
  18. Bardin, Sébastien; Finkel, Alain; Leroux, Jérôme; Petrucci, Laure: FAST: Acceleration from theory to practice (2008) ioport
  19. Bouchy, Florent; Finkel, Alain; Leroux, Jérôme: Decomposition of decidable first-order logics over integers and reals (2008) ioport
  20. Finkel, Alain; Sangnier, Arnaud: Reversal-bounded counter machines revisited (2008)

1 2 3 next


Further publications can be found at: http://www.liafa.jussieu.fr/~sighirea/trex/index.html#Refs