Rewriting logic: roadmap and bibliography, Theoretical Computer Science, vol.285, issue.2, pp.121-154, 2002. ,
DOI : 10.1016/S0304-3975(01)00357-7
Maude as a wide-spectrum framework for formal modeling and analysis of active networks, Proceedings DARPA Active Networks Conference and Exposition, pp.494-510, 2002. ,
DOI : 10.1109/DANCE.2002.1003516
PATHWAY LOGIC: SYMBOLIC ANALYSIS OF BIOLOGICAL SIGNALING, Biocomputing 2002, pp.400-412, 2002. ,
DOI : 10.1142/9789812799623_0038
The rewriting logic semantics project, Theoretical Computer Science, vol.373, issue.3, pp.213-237, 2007. ,
DOI : 10.1016/j.tcs.2006.12.018
All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007. ,
An Overview of ELAN, Electronic Notes in Theoretical Computer Science, vol.15, 1998. ,
DOI : 10.1016/S1571-0661(05)82552-6
Logical foundations of CafeOBJ, Theoretical Computer Science, vol.285, issue.2, pp.289-318, 2002. ,
DOI : 10.1016/S0304-3975(01)00361-9
Membership algebra as a logical framework for equational specification, Lecture Notes in Computer Science, vol.1376, pp.18-61, 1997. ,
DOI : 10.1007/3-540-64299-4_26
The Maude LTL Model Checker, Electronic Notes in Theoretical Computer Science, vol.71, 2002. ,
DOI : 10.1016/S1571-0661(05)82534-4
Equational Abstractions, Lecture Notes in Computer Science, vol.2741, pp.2-16, 2003. ,
DOI : 10.1007/978-3-540-45085-6_2
Introducing the ITP tool : a tutorial, J. Universal Computer Science, vol.12, issue.11, pp.1618-1650, 2006. ,
Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol.360, issue.1-3, pp.386-414, 2006. ,
DOI : 10.1016/j.tcs.2006.04.012
Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, WRLA, 2004. ,
Verifying Specifications with Proof Scores in CafeOBJ, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pp.3-10, 2006. ,
DOI : 10.1109/ASE.2006.73
State Machines as Inductive Types, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol.90, issue.12, pp.90-2985, 2007. ,
DOI : 10.1093/ietfec/e90-a.12.2985
A lightweight integration of theorem proving and model checking for system verification, 12th Asia-Pacific Software Engineering Conference (APSEC'05), pp.59-66, 2005. ,
DOI : 10.1109/APSEC.2005.9
Chocolat/SMV: A Translator from CafeOBJ into SMV, Sixth International Conference on Parallel and Distributed Computing Applications and Technologies (PDCAT'05), pp.416-420, 2005. ,
DOI : 10.1109/PDCAT.2005.98
A Specification Translation from Behavioral Specifications to Rewrite Specifications, IEICE Transactions on Information and Systems, vol.91, issue.5, pp.91-1492, 2008. ,
DOI : 10.1093/ietisy/e91-d.5.1492
Symbolic model checking with rich assertional languages, Theoretical Computer Science, vol.256, issue.1-2, pp.93-112, 2001. ,
DOI : 10.1016/S0304-3975(00)00103-1
Liveness with (0,1, ???)- Counter Abstraction, Lecture Notes in Computer Science, pp.107-122, 2002. ,
DOI : 10.1007/3-540-45657-0_9
Par induction sur la longueur de la réécriture close R ? ?(t) ?? t ? correspondant à R ?? t ?? t ? (cf. définition 3) ,