. Ravaj, Rewriting and approximations for java applications verification

P. A. Abdulla, Y. Chen, G. Delzanno, F. Haziza, C. Hong et al., Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification, CONCUR, 2010.
DOI : 10.1007/978-3-642-15375-4_7

P. A. Abdulla, G. Delzanno, and A. Rezine, Parameterized verification of infinitestate processes with global conditions, CAV, 2007.

P. A. Abdulla, N. B. Henda, G. Delzanno, F. Haziza, and A. Rezine, Parameterized Tree Systems, In FORTE LNCS, vol.95, issue.7, pp.69-83, 2008.
DOI : 10.1016/S0304-3975(00)00103-1

P. A. Abdulla, A. Legay, A. Rezine, and J. , Simulation-Based Iteration of Tree Transducers, TACAS, pp.30-40, 2005.
DOI : 10.1007/978-3-540-31980-1_3

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

T. Ball, B. Cook, V. Levin, and S. K. Rajamani, SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, IFM, 2004.
DOI : 10.1007/978-3-540-24756-2_1

N. Barré, F. Besson, T. Genet, L. Hubert, and L. L. Roux, Copster homepage, 2009.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Boichut, R. Courbis, P. Heam, and O. Kouchnarenko, Finer Is Better: Abstraction Refinement for Rewriting Approximations, RTA, 2008.
DOI : 10.1007/978-3-540-70590-1_4

URL : https://hal.archives-ouvertes.fr/hal-00563422

Y. Boichut, T. Dao, and V. Murat, Characterizing Conclusive Approximations by Logical Formulae, RP, pp.72-84, 2011.
DOI : 10.1007/978-3-642-24288-5_8

URL : https://hal.archives-ouvertes.fr/inria-00606100

Y. Boichut, T. Genet, T. Jensen, and L. Leroux, Rewriting Approximations for Fast Prototyping of Static Analyzers, RTA, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6

URL : https://hal.archives-ouvertes.fr/hal-00463418

B. Boigelot, A. Legay, and P. Wolper, Iterating transducers in the large (extended abstract), CAV, LNCS, pp.223-235, 2003.

A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar, Abstract regular tree model checking, ENTCS, vol.149, issue.1, pp.37-48, 2006.
DOI : 10.1016/j.entcs.2005.11.015

URL : https://hal.archives-ouvertes.fr/hal-00156828

A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar, Abstract rmc of complex dynamic data structures, SAS, 2006.

A. Bouajjani, P. Habermehl, and T. Vojnar, Abstract Regular Model Checking, CAV, pp.372-386, 2004.
DOI : 10.1007/978-3-540-27813-9_29

URL : https://hal.archives-ouvertes.fr/hal-00159512

A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, Regular Model Checking, CAV, pp.403-418, 2000.
DOI : 10.1007/10722167_31

URL : https://hal.archives-ouvertes.fr/hal-00159512

A. Bouajjani and T. Touili, Extrapolating Tree Transformations, CAV, pp.539-554, 2002.
DOI : 10.1007/3-540-45657-0_46

URL : https://hal.archives-ouvertes.fr/hal-00161115

B. Boyer, T. Genet, and T. Jensen, Certifying a Tree Automata Completion Checker, IJCAR'08, 2008.
DOI : 10.1007/978-3-540-71070-7_43

URL : https://hal.archives-ouvertes.fr/inria-00258275

D. Dams, Y. Lakhnech, and M. Steffen, Iterating transducers, Journal of Logic and Algebraic Programming, pp.52-53109, 2002.
DOI : 10.1007/3-540-44585-4_27

G. Feuillade, T. Genet, V. Viet-triem, and . Tong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004.
DOI : 10.1007/s10817-004-6246-0

URL : https://hal.archives-ouvertes.fr/inria-00071609

T. Genet, Decidable approximations of sets of descendants and sets of normal forms, RTA, pp.151-165, 1998.
DOI : 10.1007/BFb0052368

URL : https://hal.archives-ouvertes.fr/inria-00073364

T. Genet, Reachability analysis of rewriting for software verification Habilitation, Université de Rennes, vol.1, 2009.

T. Genet and F. Klay, Rewriting for Cryptographic Protocol Verification, Proc. 17th CADE, volume 1831 of LNAI, 2000.
DOI : 10.1007/10721959_21

URL : https://hal.archives-ouvertes.fr/inria-00072731

T. Genet and R. Rusu, Equational tree automata completion, p.45, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00495405

T. Genet, Y. Tang-talpin, V. Viet-triem, and . Tong, Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems, 2003.

T. Genet, V. Viet-triem, and . Tong, Timbuk 2.0 ? a Tree Automata Library, 2001.

R. Gilleron and S. Tison, Regular tree languages and rewrite systems, Fundamenta Informaticae, vol.24, pp.157-175, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00538882

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar, Symbolic model checking with rich assertional languages, CAV, 1997.
DOI : 10.1016/S0304-3975(00)00103-1

G. Patin, M. Sighireanu, and T. Touili, Spade: Verification of Multithreaded Dynamic and Recursive Programs, CAV, 2007.
DOI : 10.1007/978-3-540-73368-3_28

URL : https://hal.archives-ouvertes.fr/hal-00160449

A. Podelski and A. Rybalchenko, ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement, PADL, 2007.
DOI : 10.1007/978-3-540-69611-7_16

T. Takai, A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, RTA, pp.119-133, 2004.
DOI : 10.1007/978-3-540-25979-4_9

A. Vardhan, K. Sen, M. Viswanathan, and G. Agha, Using Language Inference to Verify Omega-Regular Properties, TACAS, 2005.
DOI : 10.1007/978-3-540-31980-1_4

A. Vardhan and M. Viswanathan, Lever: A tool for learning based verification add(X,nil) -> cons(X,nil) add(X,cons, CAV, 2006.

X. Y. Vars, X,nil) -> cons(X,nil) add(X,cons(Y,Z)) -> cons