Researchers

Back to the list
Share:
A A
Avatar- profil Picture
Denis Cousineau
Former member
Microsoft Research - Inria Joint Centre
Tools for Proofs
Presentation

I’m a postdoc in project ProVal at LRI and Inria. I’m working on a Coq-checkable proof-trace system for SMT-solver Alt-Ergo. Formerly, I’ve been, by reverse chronological order, Expert research engineer at Microsoft Research-Inria Joint Centre. I was working on TLA proof manager: Teacher assistant (moniteur) at Université Paris Diderot, PhD student in project Typical at Ecole Polytechnique. I was working on proof normalization.

Contact:
ue.uaenisuoC@sined
+33 1 74 85 42 68
Personal web page
Publications at the Joint Centre:

2012

Conference papers

titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science; FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. <10.1007/978-3-642-32759-9_14>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., 2012, <http://arxiv.org/abs/1208.5933>
Accès au bibtex
BibTex