| Reasoning with triggers C Dross, S Conchon, A Paskevich INRIA, 2012 | 37 | 2012 |
| Rail, space, security: Three case studies for SPARK 2014 C Dross, P Efstathopoulos, D Lesens, D Mentré, Y Moy Proc. ERTS 19, 2014 | 33 | 2014 |
| Adding decision procedures to SMT solvers using axioms with triggers C Dross, S Conchon, J Kanig, A Paskevich Journal of Automated Reasoning 56, 387-457, 2016 | 32 | 2016 |
| Auto-active proof of red-black trees in SPARK C Dross, Y Moy NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field …, 2017 | 28 | 2017 |
| Correct code containing containers C Dross, JC Filliâtre, Y Moy Tests and Proofs: 5th International Conference, TAP 2011, Zurich …, 2011 | 26 | 2011 |
| Climbing the Software Assurance Ladder-Practical Formal Verification for Reliable Software C Dross, G Foliard, T Jouanny, L Matias, S Matthews, JM Mota, Y Moy, ... | 14* | |
| Recursive data structures in SPARK C Dross, J Kanig Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020 | 13 | 2020 |
| VerifyThis 2019: a program verification competition C Dross, CA Furia, M Huisman, R Monahan, P Müller International Journal on Software Tools for Technology Transfer 23 (6), 883-893, 2021 | 10 | 2021 |
| Verification of Programs with Pointers in SPARK GA Jaloyan, C Dross, M Maalej, Y Moy, A Paskevich International Conference on Formal Engineering Methods, 55-72, 2020 | 9 | 2020 |
| Practical application of SPARK to OpenUxAS MA Aiello, C Dross, P Rogers, L Humphrey, J Hamil Formal Methods–The Next 30 Years: Third World Congress, FM 2019, Porto …, 2019 | 9 | 2019 |
| Teaching deductive verification through FRAMA-C and SPARK for non computer scientists L Creuse, C Dross, C Garion, J Hugues, J Huguet Formal Methods Teaching: Third International Workshop and Tutorial, FMTea …, 2019 | 8 | 2019 |
| Hi-Lite: the convergence of compiler technology and program verification J Kanig, E Schonberg, C Dross Proceedings of the 2012 ACM conference on High integrity language technology …, 2012 | 8 | 2012 |
| Abstract software specifications and automatic proof of refinement C Dross, Y Moy International Conference on Reliability, Safety and Security of Railway …, 2016 | 6 | 2016 |
| Specification and proof of high-level functional properties of bit-level programs C Fumex, C Dross, J Gerlach, C Marché NASA Formal Methods Symposium, 291-306, 2016 | 6 | 2016 |
| Generic decision procedures for axiomatic first-order theories C Dross Université Paris Sud-Paris XI, 2014 | 6 | 2014 |
| High-level functional properties of bit-level programs: Formal specifications and automated proofs C Dross, C Fumex, J Gerlach, C Marché | 5 | 2015 |
| Co-Developing Programs and Their Proof of Correctness R Chapman, C Dross, S Matthews, Y Moy Communications of the ACM 67 (3), 84-94, 2024 | 4 | 2024 |
| Making proofs of floating-point programs accessible to regular developers C Dross, J Kanig International Workshop on Numerical Software Verification, 7-24, 2021 | 4 | 2021 |
| Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK BM Brosgol, C Dross, Y Moy 2019 IEEE Cybersecurity Development (SecDev), 1-2, 2019 | 3 | 2019 |
| SPARK 2014 Rationale: Type Predicates, Variables that are Constant, Support for Ravenscar and Support for Type Invariants. Y Moy, C Dross Ada User Journal 38 (1), 2017 | 1 | 2017 |
