Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023
Formal Methods for the Informal Engineer: Workshop Recommendations.
CoRR, 2021
CoStar: a verified ALL(*) parser.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021
Program Sketching by Automatically Generating Mocks from Tests.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021
Using Binary Analysis Frameworks: The Case for BAP and angr.
Proceedings of the NASA Formal Methods - 11th International Symposium, 2019
A Verified LL(1) Parser Generator.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019
A Heuristic Prover for Real Inequalities.
J. Autom. Reason., 2016
Elaboration in Dependent Type Theory.
CoRR, 2015
The Structural Theory of Pure Type Systems.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012
Size-based termination: Semantics and generalizations. (Terminaison à base de tailles: Sémantique et généralisations).
PhD thesis, 2011
Refinement Types as Higher-Order Dependency Pairs.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011
On the relation between size-based termination and semantic labelling
CoRR, 2009
On the Relation between Sized-Types Based Termination and Semantic Labelling.
Proceedings of the Computer Science Logic, 23rd international Workshop, 2009