Testing noninterference, quickly.
J. Funct. Program., 2016
Formalized linear algebra over Elementary Divisor Rings in Coq.
Log. Methods Comput. Sci., 2016
Micro-Policies: Formally Verified, Tag-Based Security Monitors.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015
Foundational Property-Based Testing.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015
Étude formelle d'algorithmes efficaces en algèbre linéaire. (Formal study of efficient algorithms in linear algebra).
PhD thesis, 2013
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013
A Refinement-Based Approach to Computational Algebra in Coq.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012
Towards a Certified Computation of Homology Groups for Digital Images.
Proceedings of the Computational Topology in Image Context - 4th International Workshop, 2012
Incidence Simplicial Matrices Formalized in Coq/SSReflect.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011
Full Reduction at Full Throttle.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011
Formal Proof of Theorems on Genetic Regulatory Networks.
Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009