Constrained Tree Grammars to Pilot Automated Proof by Induction Research...  @ NUS Home/Search
Context
Related
| lsv.enscachan.fr/...lsv200414.rr.ps Cached: PS.gz PS PDF Image Update Help From: lsv.enscachan....pportslist.php (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: In this paper, we develop a new approach for mechanizing induction on complex data structures (like bags, sorted lists, trees, powerlists. . . ) by adapting and generalizing works in tree automata with constraints. The key idea of our approach is to compute a tree grammar with constraints which describes the initial model of the given specification. (Update)
Active bibliography (related documents): More All
2.7: Constrained Tree Grammars to Pilot Automated Proof by Induction - Bouhoula, Jacquemard (2004) (Correct)
0.5: Automata-Driven Automated Induction - Bouhoula, Jouannaud (1996) (Correct)
0.3: Inductionless Induction - Comon (1994) (Correct)
Similar documents based on text: More All
0.3: Narrowing-Based Constraint Solving for the Verification of.. - Delaune, Jacquemard (2004) (Correct)
0.3: Ground Reducibility is EXPTIME-complete - Comon, Jacquemard (1998) (Correct)
0.3: The Power of Reachability Testing for Timed Automata - Aceto, Bouyer.. (2001) (Correct)
BibTeX entry: (Update)
@misc{ grammars-bouhoula,
author = "Constrained Tree Grammars",
title = "A. Bouhoula and F. Jacquemard",
url = "citeseer.comp.nus.edu.sg/659324.html" }
Citations (may not include all citations):392 A Computational Logic (context) - Boyer, Moore - 1979
270 Formal verification for fault-tolerant architectures: Proleg.. - Owre, Rushby et al. - 1995
263 The inductive Approach to verifying cryptographic protocols - Paulson - 1998
121 Handbook of Theoretical Computer Science (context) - Dershowitz, Jouannaud - 1990
102 Tree automata techniques and applications - Comon, Dauchet et al. - 2002
68 Proofs by induction in equational theories with constructors (context) - Huet, Hullot - 1982
58 Deduction with symbolic constraints (context) - Kirchner, Kirchner et al. - 1990
52 Implicit induction in conditional theories - Bouhoula, Rusinowitch - 1995
51 Proof by consistency in equational theories (context) - Bachmair - 1988
51 Specification and Proof in Membership Equational Logic - Bouhoula, Jouannaud et al. - 2000
50 On proving inductive properties of abstract data types (context) - Musser - 1980
45 Proof by Consistency (context) - Kapur, Musser - 1987
44 A mechanizable induction principle for equational specificat.. (context) - Zhang, Kapur et al. - 1988
28 Information and Computation (context) - Comon, Nieuwenhuis et al. - 2000
21 Automata-driven automated induction - Bouhoula, Jouannaud - 2001
21 cleaning and symbolic constraints solving (context) - Caron, Comon et al. - 1994
20 ground reducibility and their complexity (context) - Kapur, Narendran et al. - 1991
19 Ground reducibility is EXPTIME-complete - Comon, Jacquemard - 2003
18 Decision problems in ordered rewriting - Comon, Narendran et al. - 1998
15 Inductive proofs by specification transformations (context) - Comon - 1989
14 Equality and disequality constraints on brother terms in tre.. (context) - Bogaert, Tison - 1992
12 Proof by induction in equational theories without constructo.. (context) - Jouannaud, Kounalis - 1986
12 Automated theorem proving by test set induction - Bouhoula - 1997
10 Implementing contextual rewriting (context) - Zhang - 1992
7 Automata for reduction properties solving (context) - Dauchet, Caron et al. - 1995
5 Institut Polytechnique de Grenoble (context) - Comon, disunification et al. - 1988
3 Finding counterexamples to Inductive conjectures and discove.. - Steel, Bundy et al. - 2002
3 Automated verification by induction with associativecommutat.. - Berregeb, Bouhoula et al. - 1995
2 Essays in Honor of Larry Wos (context) - Constructors, Partial - 1997
2 Handbook of Automated Reasoning (context) - Inductionless - 2001
Documents on the same site (http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rapports-list.php): More
Log Auditing through Model-Checking - Roger, Goubault-Larrecq (2001) (Correct)
Updatable Timed Automata, an Algorithmic Approach - Bouyer (2001) (Correct)
Randomized Dining Philosophers Without Fairness Assumption - Duflot, Fribourg, Picaronny (2001) (Correct)
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.