?. Insert, 14. x/s(y) = e ? insert(x/s(y), e :: l) = e :: l 15. ltr (x/s(y), e) ? insert(x/s(y), e :: l) = x/s(y) :: e :: l 16. ltr (e, x/s(y)) ? insert(x/s(y), e :: l) = e :: insert(x/s(y), l) 17. isin(x/s(y)

M. Aiguier, A. Arnould, C. Boin, P. L. Gall, and B. Marre, Testing from Algebraic Specifications: Test Data Set Selection by Unfolding Axioms, Formal Approaches to Testing of Software (FATES'05), pp.203-217, 2005.
DOI : 10.1109/ASE.2000.873667

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

M. Aiguier, A. Arnould, P. L. Gall, and D. Longuet, Test Selection Criteria for Quantifier-Free First-Order Specifications, Fundamentals of Software Engineering, pp.144-159, 2007.
DOI : 10.1007/978-3-540-75698-9_10

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

M. Aiguier, A. Arnould, P. L. Gall, and D. Longuet, Exhaustive test sets for algebraic specification correctness, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01318362

A. Arnould and P. L. Gall, Test de conformité : une approche algébrique, pp.1219-1242, 2002.

A. Arnould, P. L. Gall, and B. Marre, Dynamic testing from bounded data type specifications, Dependable Computing -EDCC-2, pp.285-302, 1996.
DOI : 10.1007/3-540-61772-8_44

G. Bernot, Testing against formal specifications: A theoretical view, Theory and Practice of Software Development (TAPSOFT'91), pp.99-119, 1991.
DOI : 10.1007/3540539816_63

G. Bernot, M. Gaudel, and B. Marre, Software testing based on formal specifications: a theory and a tool, Software Engineering Journal, vol.6, issue.6, pp.387-405, 1991.
DOI : 10.1049/sej.1991.0040

D. Achim, B. Brucker, and . Wolff, Symbolic test case generation for primitive recursive functions, Formal Approaches to Software Testing, pp.16-32, 2004.

M. Carlier and C. Dubois, Functional Testing in the Focal Environment, Tests and Proofs, pp.84-98, 2008.
DOI : 10.1007/978-3-540-79124-9_7

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

K. Claessen and J. Hughes, QuickCheck, ACM SIGPLAN Notices, vol.35, issue.9, pp.268-279, 2000.
DOI : 10.1145/357766.351266

J. Dick and A. Faivre, Automating the generation and sequencing of test cases from model-based specifications, Formal Methods Europe (FME'93), pp.268-284, 1993.
DOI : 10.1007/BFb0024651

L. Frantzen, J. Tretmans, and T. A. Willemse, Test Generation Based on Symbolic Specifications, Formal Approaches to Software Testing, pp.1-15, 2004.
DOI : 10.1007/3-540-40911-4_20

C. Gaston, P. L. Gall, N. Rapin, and A. Touil, Symbolic Execution Techniques for Test Purpose Definition, Testing of Communicating Systems (Test- Com'06), pp.1-18, 2006.
DOI : 10.1007/11754008_1

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

M. Gaudel, Testing can be formal, too, Theory and Practice of Software Development (TASPOFT'95), pp.82-96, 1995.
DOI : 10.1007/3-540-59293-8_188

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.6013

R. Hennicker, M. Wirsing, and M. Bidoit, Proof systems for structured specifications with observability operators, Theoretical Computer Science, vol.173, issue.2, pp.393-443, 1997.
DOI : 10.1016/S0304-3975(96)00162-4

C. Jard and T. Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, 2004.
DOI : 10.1007/s10009-004-0153-x

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.4262

W. M. Pieter, . Koopman, M. J. Artem-alimarine-tretmans, . Plasmeijer, and . Gast, Generic automated software testing, Implementation of Functional Languages, pp.84-100, 2002.

P. L. Gall and A. Arnould, Formal specifications and test: Correctness and oracle, 11th Workshop on Algebraic Development Techniques (WADT'96), pp.342-358, 1996.
DOI : 10.1007/3-540-61629-2_52

D. Lee and M. Yannakakis, Principles and methods of testing finite state machines-a survey, Proceedings of the IEEE, pp.1090-1126, 1996.
DOI : 10.1109/5.533956

G. Lussier-andhéì-ene-waeselynck, Proof-guided test: an experimental study, International Computer Software and Applications Conference, pp.528-533, 2004.

P. Machado, On Oracles for Interpreting Test Results against Algebraic Specifications, Algebraic Methodology and Software Technology, 1999.
DOI : 10.1007/3-540-49253-4_35

P. Machado, Testing from Structured Algebraic Specifications, Algebraic Methodology and Software Technology (AMAST'00), pp.529-544, 2000.
DOI : 10.1007/3-540-45499-3_37

P. Machado and D. Sannella, Unit Testing for Casl Architectural Specifications, In Mathematical Foundations of Computer Science Lecture Notes in Computer Science, vol.2420, pp.506-518, 2002.
DOI : 10.1007/3-540-45687-2_42

B. Marre, LOFT: A tool for assisting selection of test data sets from algebraic specifications, Theory and Practice of Software Development (TAPSOFT'95), pp.799-800, 1995.
DOI : 10.1007/3-540-59293-8_240

D. Peter and . Mosses, The Complete Documentation of the Common Algebraic Specification Language, Lecture Notes in Computer Science, vol.2960, 2004.

A. Petrenko, S. Boroday, and R. Groz, Confirming configurations in EFSM, Formal Methods for Protocol Engineering and Distributed Systems (FORTE'99), volume 156 of IFIP Conference Proceedings, pp.5-24, 1999.
DOI : 10.1007/978-0-387-35578-8_1

A. George, L. Robinson, and . Wos, Paramodulation and theorem proving in first-order theories with equality, Machine Intelligence, vol.4, pp.133-150, 1969.

V. Rusu, L. Bousquet, and T. Jéron, An Approach to Symbolic Test Generation, 2nd International Workshop on Integrated Formal Method (IFM'00), pp.338-357, 1945.
DOI : 10.1007/3-540-40911-4_20

J. Tretmans, Testing labelled transition systems with inputs and outputs, International Workshop on Protocols Test Systems (IWPTS'95), 1995.