| A verified information-flow architecture A Azevedo de Amorim, N Collins, A DeHon, D Demange, C Hriţcu, ... Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 101 | 2014 |
| Formal verification of an SSA-based middle-end for CompCert G Barthe, D Demange, D Pichardie ACM Transactions on Programming Languages and Systems (TOPLAS) 36 (1), 1-35, 2014 | 58 | 2014 |
| A formally verified SSA-based middle-end: Static single assignment meets CompCert G Barthe, D Demange, D Pichardie European Symposium on Programming, 47-66, 2012 | 44 | 2012 |
| Plan B: A buffered memory model for Java D Demange, V Laporte, L Zhao, S Jagannathan, D Pichardie, J Vitek Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013 | 43 | 2013 |
| Sawja: Static analysis workshop for java L Hubert, N Barré, F Besson, D Demange, T Jensen, V Monfort, ... International Conference on Formal Verification of Object-Oriented Software …, 2010 | 43 | 2010 |
| A provably correct stackless intermediate representation for Java bytecode D Demange, T Jensen, D Pichardie Asian Symposium on Programming Languages and Systems, 97-113, 2010 | 31 | 2010 |
| Intermittent computing with peripherals, formally verified G Berthou, PÉ Dagand, D Demange, R Oudin, T Risset The 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools …, 2020 | 23 | 2020 |
| A verified information-flow architecture A Azevedo de Amorim, N Collins, A DeHon, D Demange, C Hriţcu, ... Journal of computer security 24 (6), 689-734, 2016 | 23 | 2016 |
| Safe: A clean-slate architecture for secure systems S Chiricescu, A DeHon, D Demange, S Iyer, A Kliger, G Morrisett, ... 2013 IEEE International Conference on Technologies for Homeland Security …, 2013 | 23 | 2013 |
| Verifying fast and sparse SSA-based optimizations in Coq D Demange, D Pichardie, L Stefanesco International Conference on Compiler Construction, 233-252, 2015 | 21 | 2015 |
| Semantic reasoning about the sea of nodes D Demange, Y Fernández de Retana, D Pichardie Proceedings of the 27th International Conference on Compiler Construction …, 2018 | 18 | 2018 |
| Validating dominator trees for a fast, verified dominance test S Blazy, D Demange, D Pichardie Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 18 | 2015 |
| All secrets great and small D Demange, D Sands European Symposium on Programming, 207-221, 2009 | 13 | 2009 |
| Mechanizing conventional SSA for a verified destruction with coalescing D Demange, Y Fernandez de Retana Proceedings of the 25th International Conference on Compiler Construction, 77-87, 2016 | 11 | 2016 |
| Verifying a concurrent garbage collector using a rely-guarantee methodology Y Zakowski, D Cachera, D Demange, G Petri, D Pichardie, ... Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 10 | 2017 |
| Mechanised semantics for gated static single assignment Y Herklotz, D Demange, S Blazy Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 7 | 2023 |
| Semantic foundations of intermediate program representations D Demange École normale supérieure de Cachan-ENS Cachan, 2012 | 7 | 2012 |
| Compilation of linearizable data structures-a mechanised RG logic for semantic refinement Y Zakowski, D Cachera, D Demange, D Pichardie Symposium on Applied Computing, 2017 | 5 | 2017 |
| Verifying a concurrent garbage collector with a rely-guarantee methodology Y Zakowski, D Cachera, D Demange, G Petri, D Pichardie, ... Journal of Automated Reasoning 63, 489-515, 2019 | 2 | 2019 |
| Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement Y Zakowski, D Cachera, D Demange, D Pichardie Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 1881-1890, 2018 | 2 | 2018 |
