Resolution Theorem Proving, Handbook of Automated Reasoning, I, pp.19-99, 2001. ,
DOI : 10.1016/B978-044450813-3/50004-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450
Computing finite models by reduction to function-free clause logic, Journal of Applied Logic, vol.7, issue.1, pp.58-74, 2009. ,
DOI : 10.1016/j.jal.2007.07.005
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
Automatic Proofs and Refutations for Higher-Order Logic, 2012. ,
Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions, Softw. Qual. J, vol.21, issue.1, pp.101-12610, 2013. ,
Hammering towards QED, J. Formal. Reasoning, vol.9, issue.1, pp.101-148, 2016. ,
Nitpick: A counterexample generator for higher-order logic based on a relational model finder, ITP 2010, pp.131-146, 2010. ,
The New Quickcheck for Isabelle, CPP 2012, pp.92-108, 2012. ,
DOI : 10.1007/978-3-642-35308-6_10
Automated Model Building Applied Logic 31, 2004. ,
A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest, TAP 2012, pp.35-50, 2012. ,
DOI : 10.1007/978-3-642-30473-6_5
URL : https://hal.archives-ouvertes.fr/hal-01126115
Proof Synthesis and Reflection for Linear Arithmetic, Journal of Automated Reasoning, vol.10, issue.5, pp.33-5910, 2008. ,
DOI : 10.1007/s10817-008-9101-x
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.304.7968
QuickCheck: A lightweight tool for random testing of Haskell programs, ICFP '00, pp.268-27910, 2000. ,
New techniques that improve MACE-style model finding, 2003. ,
Orna Grumberg & Doron A. Peled (1999): Model Checking ,
TLA???+??? Proofs, FM 2012, pp.147-154, 2012. ,
DOI : 10.1007/978-3-642-32759-9_14
URL : https://hal.archives-ouvertes.fr/hal-00726632
Automated Flaw Detection in Algebraic Specifications, Journal of Automated Reasoning, vol.20, issue.1, pp.359-39510, 2010. ,
DOI : 10.1007/s10817-010-9166-1
Combining Testing and Proving in Dependent Type Theory, TPHOLs 2003, pp.188-20310, 2003. ,
DOI : 10.1007/10930755_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6779
Automating Algebraic Methods in Isabelle, ICFEM 2011, pp.617-632, 2011. ,
DOI : 10.1007/978-94-010-0413-8_11
Nitpick: A checkable specification language, FMSP '96, pp.60-69, 1996. ,
Software Abstractions: Logic, Language, and Analysis, 2006. ,
Translating dependent type theory into higher order logic, TLCA 1993, pp.209-22910, 1993. ,
DOI : 10.1007/BFb0037108
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.7356
Non-cyclic Sorts for First-Order Satisfiability, FroCoS 2013, pp.214-228, 2013. ,
DOI : 10.1007/978-3-642-40885-4_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.381.657
Relational analysis of algebraic datatypes, pp.207-216, 2005. ,
Property directed generation of first-order test data, Intellect, pp.105-123, 2007. ,
Animating the Formalised Semantics of a Java-Like Language, ITP 2011, pp.216-232, 2011. ,
DOI : 10.1007/978-3-642-03359-9_31
Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities, ITP 2013, p.18, 2013. ,
DOI : 10.1007/978-3-642-39634-2_4
Prover9 and Mace4 ,
A Davis?Putnam program and its application to finite first-order model search: quasigroup existence problems, 1994. ,
Random testing in PVS, AFM '06, 2006. ,
Foundational Property-Based Testing, ITP 2015, pp.325-343, 2015. ,
DOI : 10.1007/978-3-319-22102-1_22
URL : https://hal.archives-ouvertes.fr/hal-01162898
Flaw Detection in Formal Specifications, IJCAR 2001, pp.642-657, 2001. ,
DOI : 10.1007/3-540-45744-5_52
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2528
A decision procedure for (co)datatypes in SMT solvers, CADE-25, pp.197-213, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01212585
Model Finding for Recursive Functions in SMT, IJCAR 2016, 2016. ,
DOI : 10.1007/978-3-319-40229-1_10
URL : https://hal.archives-ouvertes.fr/hal-01242509
Quantifier Instantiation Techniques for Finite Model Finding in SMT, LNCS, vol.7898, pp.24-377, 2013. ,
DOI : 10.1007/978-3-642-38574-2_26
SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values, pp.37-4810, 2008. ,
DOI : 10.1145/1543134.1411292
FINDER: Finite domain enumerator?System description, LNCS, vol.814, pp.12-798, 1994. ,
First-Class Type Classes, TPHOLs 2008, pp.278-293, 2008. ,
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864
Satisfiability Modulo Recursive Programs, SAS 2011, pp.298-315, 2011. ,
DOI : 10.1007/978-3-540-77395-5_17
Kodkod: A Relational Model Finder, TACAS 2007, pp.632-647, 2007. ,
DOI : 10.1007/978-3-540-71209-1_49
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.697.8573
SAT-Based Finite Model Generation for Higher-Order Logic, 2008. ,
Type classes and overloading in higher-order logic, TPHOLs 1997, pp.307-32210, 1997. ,
DOI : 10.1007/BFb0028402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.782
SEM: A system for enumerating models, IJCAI-95, pp.298-303, 1995. ,