Mutation testing advances: An analysis and survey, Advances in Computers, vol.112, pp.275-378, 2019. ,
Formal verification of a realistic compiler, Commun. ACM, vol.52, issue.7, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
seL4: Formal verification of an OS kernel, Symposium on Operating Systems Principles, pp.207-220, 2009. ,
Planning for change in a formal verification of the Raft consensus protocol, Certified Programs and Proofs, pp.154-165, 2016. ,
QED at large: A survey of engineering of formally verified software, Foundations and Trends in Programming Languages, vol.5, pp.102-281, 2019. ,
An empirical study on the correctness of formally verified distributed systems, European Conference on Computer Systems, pp.328-343, 2017. ,
Finding and understanding bugs in C compilers, Conference on Programming Language Design and Implementation, pp.283-294, 2011. ,
How verified (or tested) is my code? Falsification-driven verification and testing, Automated Software Engineering, vol.25, issue.4, pp.917-960, 2018. ,
Vacuity in testing, Tests and Proofs, pp.4-17, 2008. ,
QuickChick Interface, 2018. ,
MuCheck: An extensible tool for mutation testing of Haskell programs, International Symposium on Software Testing and Analysis, pp.429-432, 2014. ,
Empirical evaluation of test coverage for functional programs, International Conference on Software Testing, Verification, and Validation, pp.255-265, 2016. ,
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Coq manual: Syntax extensions and interpretation scopes, 2019. ,
, Coq manual: Utilities, 2019.
iCoq: Regression proof selection for large-scale verification projects, International Conference on Automated Software Engineering, pp.171-182, 2017. ,
An extensible, regular-expression-based tool for multi-language mutant generation, International Conference on Software Engineering, pp.25-28, 2018. ,
SerAPI: Machine-Friendly, Data-Centric Serialization for Coq, MINES ParisTech, Tech. Rep, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01384408
Recursive functions of symbolic expressions and their computation by machine, part I, Commun. ACM, vol.3, issue.4, pp.184-195, 1960. ,
Coq issue #9204, 2018. ,
Coq pull request #9206, 2018. ,
The new Quickcheck for Isabelle: Random, exhaustive and symbolic testing under one roof, Certified Programs and Proofs, pp.92-108, 2012. ,
coq-dpdgraph, 2019. ,
Nitpick: A counterexample generator for higher-order logic based on a relational model finder, International Conference on Interactive Theorem Proving, pp.131-146, 2010. ,
Extending Nunchaku to dependent type theory, International Workshop on Hammers for Type Theories, vol.210, pp.3-12, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01401696
Foundational property-based testing, International Conference on Interactive Theorem Proving, pp.325-343, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01162898
The Cogent case for property-based testing, Workshop on Programming Languages and Operating Systems, pp.1-7, 2017. ,
Automated theory exploration for interactive theorem proving, International Conference on Interactive Theorem Proving, pp.1-11, 2017. ,
A tactic language for the system Coq, Logic for Programming and Automated Reasoning, pp.85-95, 2000. ,
URL : https://hal.archives-ouvertes.fr/hal-01125070
, , 2017.
jsCoq: Towards hybrid theorem proving interfaces, Workshop on User Interfaces for Theorem Provers, pp.15-27, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01425752
Hints on test data selection: Help for the practicing programmer, Computer, vol.11, issue.4, pp.34-41, 1978. ,
Theoretical and empirical studies on using program mutation to test the functional correctness of programs, Symposium on Principles of Programming Languages, pp.220-233, 1980. ,
An analysis and survey of the development of mutation testing, Transactions on Software Engineering, vol.37, issue.5, pp.649-678, 2011. ,
Are mutants a valid substitute for real faults in software testing?, " in International Symposium on Foundations of Software Engineering, pp.654-665, 2014. ,
Are mutation scores correlated with real fault detection?: A large scale empirical study on the relationship between mutants and real faults, International Conference on Software Engineering, pp.537-548, 2018. ,
Ltac anti-patterns, 2019. ,
PIT mutation testing, 2010. ,
The Major mutation framework: Efficient and scalable mutation analysis for Java, International Symposium on Software Testing and Analysis, pp.433-436, 2014. ,
Efficient mutation analysis by propagating and partitioning infected execution states, International Symposium on Software Testing and Analysis, pp.315-326, 2014. ,
Mutation reduction strategies considered harmful, Transactions on Reliability, vol.66, issue.3, pp.854-874, 2017. ,
Predictive mutation testing, Transactions on Software Engineering, 2018. ,
Topsy-Turvy: A smarter and faster parallelization of mutation analysis, International Conference on Software Engineering, pp.740-743, 2016. ,
Faster mutation analysis via equivalence modulo states, International Symposium on Software Testing and Analysis, pp.295-306, 2017. ,
Speeding up mutation testing via regression test selection: An extensive study, International Conference on Software Testing, Verification, and Validation, pp.58-69, 2018. ,
piCoq: Parallel regression proving for large-scale verification projects, International Symposium on Software Testing and Analysis, pp.344-355, 2018. ,
Constructing subtle faults using higher order mutation testing, International Working Conference on Source Code Analysis and Manipulation, pp.249-258, 2008. ,
SerAPI: The Coq Se(xp)rialized Protocol, 2019. ,
An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00515548
, , 2019.
Asynchronous processing of Coq documents: From the kernel up to the user interface, International Conference on Interactive Theorem Proving, pp.51-66, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01135919
The Lean theorem prover (system description), International Conference on Automated Deduction, pp.378-388, 2015. ,
Isabelle/HOL -A Proof Assistant for Higher-Order Logic, 2002. ,
Mitigating the effects of equivalent mutants with mutant classification strategies, Science of Computer Programming, vol.95, pp.298-319, 2014. ,
Coq manual: Conversion rules, 2019. ,
Elaboration in dependent type theory, CoRR, 2015. ,
Mutation testing of functional programming languages, 2014. ,
Automating black-box property based testing, 2016. ,
FitSpec: Refining property sets for functional testing, Haskell Symposium, pp.1-12, 2016. ,
Measuring coverage of Prolog programs using mutation testing, Functional and Constraint Logic Programming, pp.39-55, 2019. ,
Random testing in Isabelle/HOL, International Conference on Software Engineering and Formal Methods, pp.230-239, 2004. ,