@inproceedings(BJ08,
 author       = "Adel Bouhoula and Florent Jacquemard",
 year         = "2008",
 title        = "Automated Induction with Constrained Tree Automata",
 editor       = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
 booktitle    = "Proceedings of the 4th International Joint Conference on Automated Reasoning",
 series       = "Lecture Notes in Computer Science",
 volume       = "5195",
 publisher    = "Springer",
 pages        = "539--554",
 doi          = "10.1007/978-3-540-71070-7\_44",
)
@article(BJ12,
 author       = "Adel Bouhoula and Florent Jacquemard",
 year         = "2012",
 title        = "Sufficient completeness verification for conditional and constrained {TRS}",
 journal      = "Journal of Applied Logic",
 volume       = "10",
 number       = "1",
 pages        = "127--143",
 doi          = "10.1016/j.jal.2011.09.001",
)
@misc(TATA,
 author       = "Hubert Comon and Max Dauchet and R\'emi Gilleron and Florent Jacquemard and Denis Lugiez and Christof L\"oding and Sophie Tison and Marc Tommasi",
 year         = "2007",
 title        = "Tree Automata Techniques and Applications",
 howpublished = "Available on: \url {http://www.grappa.univ-lille3.fr/tata}",
 note         = "Release October, 12th 2007",
)
@article(Fri89,
 author       = "Laurent Fribourg",
 year         = "1989",
 title        = "A Strong Restriction of the Inductive Completion Procedure",
 journal      = "Journal of Symbolic Computation",
 volume       = "8",
 number       = "3",
 pages        = "253--276",
 doi          = "10.1016/S0747-7171(89)80069-0",
)
@article(furuichi,
 author       = "Yuki Furuichi and Naoki Nishida and Masahiko Sakai and Keiichirou Kusakari and Toshiki Sakabe",
 year         = "2008",
 title        = "Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems",
 journal      = "IPSJ Transactions on Programming",
 volume       = "1",
 number       = "2",
 pages        = "100--121",
 note         = "In Japanese",
)
@book(Logic,
 author       = "Michael Huth and Mark Ryan",
 year         = "2000",
 title        = "Logic in Computer Science: Modelling and Reasoning about Systems",
 publisher    = "Cambridge University Press",
)
@article(NNKSS11,
 author       = "Naoki Nakabayashi and Naoki Nishida and Keiichirou Kusakari and Toshiki Sakabe and Masahiko Sakai",
 year         = "2011",
 title        = "Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems",
 journal      = "Computer Software",
 volume       = "28",
 number       = "1",
 pages        = "173--189",
 doi          = "10.11309/jssst.28.1\_173",
 note         = "In Japanese",
)
@inproceedings(CTA,
 author       = "Naoki Nishida and Futoshi Nomura and Katsuhisa Kurahashi and Masahiko Sakai",
 year         = "2012",
 title        = "Constrained Tree Automata and their Closure Properties",
 editor       = "Keisuke Nakano and Hiroyuki Seki",
 booktitle    = "Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers",
 pages        = "24--34",
)
@inproceedings(SNS11,
 author       = "Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe",
 year         = "2011",
 title        = "On Proving Termination of Constrained Term Rewriting Systems by Eliminating Edges from Dependency Graphs",
 editor       = "Herbert Kuchen",
 booktitle    = "Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2011)",
 series       = "Lecture Notes in Computer Science",
 volume       = "6816",
 publisher    = "Springer",
 pages        = "138--155",
 doi          = "10.1007/978-3-642-22531-4\_9",
)
@article(sakata,
 author       = "Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe and Masahiko Sakai and Keiichirou Kusakari",
 year         = "2009",
 title        = "Rewriting Induction for Constrained Term Rewriting Systems",
 journal      = "IPSJ Transactions on Programming",
 volume       = "2",
 number       = "2",
 pages        = "80--96",
 note         = "In Japanese",
)