CV Accueil - Archive ouverte HAL

	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code Sandrine Blazy , Vincent Laporte , David Pichardie Journal of Automated Reasoning, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩ Article dans une revue hal-01243700v1

	An Abstract Memory Functor for Verified C Static Analyzers Sandrine Blazy , Vincent Laporte , David Pichardie ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩ Communication dans un congrès hal-01339969v1
	CompCert - A Formally Verified Optimizing Compiler Xavier Leroy , Sandrine Blazy , Daniel Kästner , Bernhard Schommer , Markus Pister ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France Communication dans un congrès hal-01238879v1
	A formally-verified C static analyzer Jacques-Henri Jourdan , Vincent Laporte , Sandrine Blazy , Xavier Leroy , David Pichardie POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩ Communication dans un congrès hal-01078386v1
	Formal Verification of a C Value Analysis Based on Abstract Interpretation Sandrine Blazy , Vincent Laporte , André Maroneze , David Pichardie SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344 Communication dans un congrès hal-00812515v1
	Formal Verification of Loop Bound Estimation for WCET Analysis Sandrine Blazy , André Maroneze , David Pichardie VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303 Communication dans un congrès hal-00848703v1

	The CompCert memory model Xavier Leroy , Andrew W. Appel , Sandrine Blazy , Gordon Stewart Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010 Chapitre d'ouvrage hal-00905435v1

Sandrine Blazy