J. Abrial, Extending B without changing it (for developing distributed systems), 1st B Conference, pp.169-190, 1996.

J. Abrial, The B Book: Assigning Programs to Meanings Modeling in Event-B -System and Software Engineering A theory of predicate-complete test coverage and generation, FMCO'04, pp.1-22, 1996.
DOI : 10.1017/CBO9780511624162

F. Bouquet, P. Bué, J. Julliand, and P. Masson, Génération de testsàtests`testsà partir de critères dynamiques de sélection et par abstraction, AFADL'09, pp.161-176, 2009.

F. Bouquet, P. Bué, J. Julliand, and P. Masson, Test Generation Based on Abstraction and Test Purposes to Complement Structural Tests, 2010 Third International Conference on Software Testing, Verification, and Validation Workshops, 2010.
DOI : 10.1109/ICSTW.2010.47

URL : https://hal.archives-ouvertes.fr/inria-00533281

F. Bouquet, J. Couchot, F. Dadeau, and A. Giorgetti, Instantiation of Parameterized Data Structures for Model-Based Testing, B'2007, the 7th Int. B Conference, pp.96-110, 2007.
DOI : 10.1007/11955757_10

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

F. Bellegarde, J. Julliand, and O. Kouchnarenko, Ready-Simulation Is Not Ready to Express a Modular Refinement Relation, LNCS, vol.1783, pp.266-283, 2000.
DOI : 10.1007/3-540-46428-X_19

S. Bensalem, Y. Lakhnech, and S. Owre, Computing abstractions of infinite state systems compositionally and automatically, CAV'98, 1998.
DOI : 10.1007/BFb0028755

F. Bouquet, B. Legeard, and F. Peureux, CLPS???B ??? A constraint solver to animate a B specification, International Journal on Software Tools for Technology Transfer, vol.7, issue.2, pp.143-157, 2004.
DOI : 10.1007/s10009-003-0123-8

T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani, Automatic predicate abstraction of c programs, PLDI, pp.203-213, 2001.

D. Bert, M. Potet, and N. Stouls, GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications Slicing an Integrated Formal Method for Verification, ZB'05BW05] Ingo Brückner and Heike Wehrheim ICFEM'05, pp.360-374, 2005.

W. Chan, R. Anderson, P. Beame, and D. Notkin, Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints, CAV'97, 1997.
DOI : 10.1007/3-540-63166-6_32

P. Cousot and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511

E. M. Clarke, O. Grumberg, and D. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

E. M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking, 2000.

J. Couchot, A. Giorgetti, N. Stouls, M. A. Colon, T. E. Uribe et al., Graph-based Reduction of Program Verification Conditions Generating finite-state abstractions of reactive systems using decision procedures Automating the generation and sequencing of test cases from model-based specifications, AFM'09 CAV'98 FME'93, pp.268-284, 1993.

B. Matthew, J. Dwyer, M. Hatcliff, V. Hoosier, R. Prasad-ranganath et al., Evaluating the effectiveness of slicing for model reduction of concurrent objectoriented programs, TACAS, pp.73-89, 2006.

C. Darlot, J. Julliand, and O. Kouchnarenko, Refinement preserves PLTL properties of B and Z Users ZB'03 -Formal Specification and Development in Z and B, Third International Conference, pp.408-420, 2003.

G. Friedman, A. Hartman, K. Nagin, T. Shirangs97, ]. S. Graf et al., Projected state machine coverage for software testing Construction of abstract state graphs with PVS An axiomatic basis for computer programming, ISSTA CAV'97HW97] Mats Per Erik Heimdahl and Michael W. Whalen. Reduction and slicing of hierarchical state machines ESEC / SIGSOFT FSE, pp.134-143576580, 1969.

J. Julliand, P. Masson, and R. Tissot, Generating security tests in addition to functional tests, Proceedings of the 3rd international workshop on Automation of software test , AST '08, pp.41-44, 2008.
DOI : 10.1145/1370042.1370051

J. Julliand, N. Stouls, P. Bué, and P. Masson, Syntactic Abstraction of B Models to Generate Tests, ProB: An automated analysis toolset for the B method. Software Tools for Technology Transfer, pp.151-166185, 2008.
DOI : 10.1007/978-3-642-13977-2_13

URL : https://hal.archives-ouvertes.fr/inria-00471324

S. Labbé, J. Gallois, and M. Pouzet, Slicing Communicating Automata Specifications for Efficient Model Reduction, 2007 Australian Software Engineering Conference (ASWEC'07), pp.191-200, 2007.
DOI : 10.1109/ASWEC.2007.43

R. Marlet, C. S. Mesnilnk00-]-k, R. P. Namjoshi, and . Kurshan, Demoney: A demonstrative electronic purse Technical Report SECSAFE-TL-007, Trusted Logic Syntactic program transformations for automatic abstraction, CAV'00, pp.435-449, 2000.

H. Sipma, T. Uribe, Z. Manna, and H. W. Thimbleby, Deductive model checking Formal Methods in System Design The directed chinese postman problem. Software: Practice and Experience A survey of program slicing techniques Practical Model-Based Testing -A tools approach, J. Prog. Lang. IEEE Transactions, vol.15, issue.334, pp.49-741081, 1984.