Rewriting and approximations for java applications verification ,
Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification, CONCUR, 2010. ,
DOI : 10.1007/978-3-642-15375-4_7
Parameterized verification of infinitestate processes with global conditions, CAV, 2007. ,
Parameterized Tree Systems, In FORTE LNCS, vol.95, issue.7, pp.69-83, 2008. ,
DOI : 10.1016/S0304-3975(00)00103-1
Simulation-Based Iteration of Tree Transducers, TACAS, pp.30-40, 2005. ,
DOI : 10.1007/978-3-540-31980-1_3
Term Rewriting and All That, 1998. ,
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, IFM, 2004. ,
DOI : 10.1007/978-3-540-24756-2_1
Copster homepage, 2009. ,
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
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
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
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
Iterating transducers in the large (extended abstract), CAV, LNCS, pp.223-235, 2003. ,
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
Abstract rmc of complex dynamic data structures, SAS, 2006. ,
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
Regular Model Checking, CAV, pp.403-418, 2000. ,
DOI : 10.1007/10722167_31
URL : https://hal.archives-ouvertes.fr/hal-00159512
Extrapolating Tree Transformations, CAV, pp.539-554, 2002. ,
DOI : 10.1007/3-540-45657-0_46
URL : https://hal.archives-ouvertes.fr/hal-00161115
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
Iterating transducers, Journal of Logic and Algebraic Programming, pp.52-53109, 2002. ,
DOI : 10.1007/3-540-44585-4_27
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
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
Reachability analysis of rewriting for software verification Habilitation, Université de Rennes, vol.1, 2009. ,
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
Equational tree automata completion, p.45, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00495405
Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems, 2003. ,
Timbuk 2.0 ? a Tree Automata Library, 2001. ,
Regular tree languages and rewrite systems, Fundamenta Informaticae, vol.24, pp.157-175, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00538882
Symbolic model checking with rich assertional languages, CAV, 1997. ,
DOI : 10.1016/S0304-3975(00)00103-1
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
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement, PADL, 2007. ,
DOI : 10.1007/978-3-540-69611-7_16
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, RTA, pp.119-133, 2004. ,
DOI : 10.1007/978-3-540-25979-4_9
Using Language Inference to Verify Omega-Regular Properties, TACAS, 2005. ,
DOI : 10.1007/978-3-540-31980-1_4
Lever: A tool for learning based verification add(X,nil) -> cons(X,nil) add(X,cons, CAV, 2006. ,
X,nil) -> cons(X,nil) add(X,cons(Y,Z)) -> cons ,