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
References in zbMATH (referenced in 46 articles , 1 standard article )
Showing results 1 to 20 of 46.
Sorted by year (- Finkel, Alain; Praveen, M.: Verification of flat FIFO systems (2020)
- Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2016)
- André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
- Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
- Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire: McScM: a general framework for the verification of communicating machines (2012) ioport
- Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
- Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2011)
- André, Étienne; Fribourg, Laurent: Behavioral cartography of timed automata (2010)
- 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
- Bozga, Marius; Iosif, Radu; Konečný, Filip: Fast acceleration of ultimately periodic relations (2010)
- Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
- Harris, William R.; Lal, Akash; Nori, Aditya V.; Rajamani, Sriram K.: Alternation for termination (2010)
- Jerson Ortiz, James; Legay, Axel; Schobbens, Pierre-Yves: Memory event clocks (2010)
- Kalyanasundaram, Bala; Velauthapillai, Mahe: Learning behaviors of functions (2010)
- Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
- Bouchy, Florent; Finkel, Alain; Sangnier, Arnaud: Reachability in timed counter systems (2009)
- Finkel, Alain; Lozes, Étienne; Sangnier, Arnaud: Towards model-checking programs with lists (2009)
- Rapin, Nicolas: Symbolic execution based model checking of open systems with unbounded variables (2009)
- Bardin, Sébastien; Finkel, Alain; Leroux, Jérôme; Petrucci, Laure: FAST: Acceleration from theory to practice (2008) ioport
- Bouchy, Florent; Finkel, Alain; Leroux, Jérôme: Decomposition of decidable first-order logics over integers and reals (2008) ioport
Further publications can be found at: http://www.liafa.jussieu.fr/~sighirea/trex/index.html#Refs