. [. Bibliography, I. Altekar, and . Stoica, ODR: Output-deterministic Replay for Multicore Debugging, ACM SIGOPS Symp. Operating Systems Principles. SOSP, pp.193-206, 2009.

M. Botin?an, M. Parkinson, and W. Schulte, Separation Logic Verification of C Programs with an SMT Solver, Electronic Notes in Theoretical Computer Science, vol.254, pp.5-23, 2009.
DOI : 10.1016/j.entcs.2009.09.057

A. [. Cimatti and . Griggio, Software Model Checking via IC3, 24th Intl. Conf. Computer Aided Verification (CAV 2012), pp.277-293, 2012.
DOI : 10.1007/978-3-642-31424-7_23

[. Choi, K. Lee, A. Loginov, R. O-'callahan, V. Sarkar et al., Efficient and Precise Datarace Detection for Multithreaded Object-oriented Programs, ACM SIGPLAN Conf. Programming Language Design and Implementation. PLDI, pp.258-269, 2002.
DOI : 10.1145/512529.512560
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.3056

L. [. Dutertre and . De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), 18th Intl. Conf. Computer-Aided Verification (CAV 2006), pp.81-94, 2006.
DOI : 10.1007/11817963_11

D. Engler and K. Ashcraft, RacerX: Effective, Static Detection of Race Conditions and Deadlocks, 10th ACM Symp. Operating Systems Principles . SOSP 2003, pp.237-252, 2003.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, 22nd Europ. Symp. Programming (ESOP 2013), pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

W. R. Harris, S. Sankaranarayanan, F. Ivan?i´ivan?i´c, and A. Gupta, Program Analysis via Satisfiability Modulo Path Programs, 37th Ann. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages. POPL 2010, pp.71-82, 2010.

J. Huang, C. Zhang, and J. Dolby, CLAP: recording local executions to reproduce concurrency failures, 34th ACM SIGPLAN Conf. Programming Language Design and Implementation. PLDI 2013, pp.141-152, 2013.

D. [. Jovanovic, O. H. Lime, and . Roux, Integer Parameter Synthesis for Timed Automata, 19th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013). LNCS 7795, pp.401-415, 2013.
DOI : 10.1007/978-3-642-36742-7_28
URL : https://hal.archives-ouvertes.fr/hal-00941007

L. Lamport, How to write a long formula, Formal Aspects of Computing, vol.6, issue.5, pp.580-584, 1994.
DOI : 10.1007/BF01211870

]. K. Lei13 and . Leino, Developing verified programs with Dafny, 35th Intl. Conf. Software Engineering. ICSE 2013, pp.1488-1490, 2013.

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, 14th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

P. Pratikakis, J. S. Foster, and M. Hicks, LOCKSMITH: Context-sensitive Correlation Analysis for Race Detection, ACM SIGPLAN Conf. Programming Language Design and Implementation. PLDI, pp.320-331, 2006.

D. [. Radoi and . Dig, Practical static race detection for Java parallel loops, Proceedings of the 2013 International Symposium on Software Testing and Analysis, ISSTA 2013, pp.178-190, 2013.
DOI : 10.1145/2483760.2483765

M. Schoeberl, W. Puffitsch, R. U. Pedersen, and B. Huber, Worst-case execution time analysis for a Java processor, Software: Practice and Experience, vol.2009, issue.1, pp.507-542, 2010.
DOI : 10.1002/spe.968

T. Sheng, N. Vachharajani, S. Eranian, and R. Hundt, RACEZ, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.401-410, 2011.
DOI : 10.1145/1985793.1985848

R. [. Thiele and . Wilhelm, Design for Timing Predictability, Real-Time Systems, vol.28, issue.2/3, pp.157-177, 2004.
DOI : 10.1023/B:TIME.0000045316.66276.6e