@inproceedings {24913,
	title = {Constraint-Based Verification of a Mobile App Game Designed for Nudging People to Attend Cancer Screening},
	journal = {Proceedings of Innovative Applications of Artificial Intelligence (IAAI-17), Feb. 2017, San Francisco, USA},
	year = {2017},
	month = {02/2017},
	publisher = {AAAI},
	author = {Gotlieb, Arnaud and Louarn, Marine and Nyg{\r a}rd, Mari and Ruiz-Lopez, Tomas and Sen, Sagar and Gori, Roberta}
}
@article {Simula.simula.2170,
	title = {Exploiting Binary Floating-Point Representations for Constraint Propagation},
	journal = {INFORMS Journal of Computing (JoC)},
	volume = {28},
	year = {2016},
	month = {01/2016},
	pages = {31-46},
	publisher = {INFORMS Journal of Computing (JoC)},
	abstract = {Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations is a hot research topic. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, as constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the filtering of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.},
	author = {Bagnara, Roberto and Carlier, Matthieu and Gori, Roberta and Gotlieb, Arnaud}
}
@inproceedings {Simula.simula.1748,
	title = {Symbolic Path-Oriented Test Data Generation for Floating-Point Programs},
	journal = {Proc. of Int. Conf. on Soft. Testing, Validation and Verification (ICST{\textquoteright}2013) - 10 pages},
	year = {2013},
	month = {March},
	publisher = {IEEE},
	type = {Conference},
	address = {Luxembourg},
	author = {Bagnara, Roberto and Carlier, Matthieu and Gori, Roberta and Gotlieb, Arnaud},
	editor = {IEEE, }
}
