Automated mathematical induction with test setsBouhoula, Adel; Kounalis, Emmanuel; Rusinowitch, Michaël et al.1992, 4 p.Report

Extending Sledgehammer with SMT SolversBLANCHETTE, Jasmin Christian; BÖHME, Sascha; PAULSON, Lawrence C et al.Journal of automated reasoning. 2013, Vol 51, Num 1, pp 109-128, issn 0168-7433, 20 p.Article

Proving Newton's Propositio Kepleriana using geometry and Nonstandard Analysis in IsabelleFLEURIOT, J. D; PAULSON, L. C.Lecture notes in computer science. 1999, pp 47-66, issn 0302-9743, isbn 3-540-66672-9Conference Paper

Formal certification of a compiler back-end or : Programming a compiler with a proof assistantLEROY, Xavier.ACM SIGPLAN notices. 2006, Vol 41, Num 1, pp 42-54, issn 1523-2867, 13 p.Conference Paper

Améliorer SAT dans le cadre incrémental = Improve engines in incremental SAT solvingAUDEMARD, Gilles; BIERE, Armin; LAGNIEZ, Jean-Marie et al.Revue d'intelligence artificielle. 2014, Vol 28, Num 5, pp 593-614, issn 0992-499X, 22 p.Article

Proof Pearl: The KeY to Correct and Stable SortingDE GOUW, Stijn; DE BOER, Frank; ROT, Jurriaan et al.Journal of automated reasoning. 2014, Vol 53, Num 2, pp 129-139, issn 0168-7433, 11 p.Article

Problem solving by searching for models with a theorem proverSHIE-JUE LEE; PLAISTED, D. A.Artificial intelligence. 1994, Vol 69, Num 1-2, pp 205-233, issn 0004-3702Article

Answer set computation based on a minimal model generation theorem proverSHIRAI, Yasuyuki; HASEGAWA, Ryuzo.Lecture notes in computer science. 2004, pp 43-52, issn 0302-9743, isbn 3-540-22817-9, 10 p.Conference Paper

Formalisation en Coq et visualisation d'un cours de géométrie pour le lycéeGUILHOT, Frédérique.TSI. Technique et science informatiques. 2005, Vol 24, Num 9, pp 1113-1138, issn 0752-4072, 26 p.Article

Verification of distributed systems with local-global predicatesMANI CHANDY, K; GO, Brian; MITRA, Sayan et al.Formal aspects of computing. 2011, Vol 23, Num 5, pp 649-679, issn 0934-5043, 31 p.Conference Paper

Analysis of a biphase mark protocol with UPPAAL and PVSVAANDRAGER, F. W; DE GROOT, A. L.Formal aspects of computing. 2006, Vol 18, Num 4, pp 433-458, issn 0934-5043, 26 p.Article

SIZE-SPACE TRADEOFFS FOR RESOLUTIONBEN-SASSON, Eli.SIAM journal on computing (Print). 2009, Vol 38, Num 6, pp 2511-2525, issn 0097-5397, 15 p.Article

Locales: A Module System for Mathematical TheoriesBALLARIN, Clemens.Journal of automated reasoning. 2014, Vol 52, Num 2, pp 123-153, issn 0168-7433, 31 p.Article

A Formalisation of the Myhill-Nerode Theorem Based on Regular ExpressionsCHUNHAN WU; XINGYUAN ZHANG; URBAN, Christian et al.Journal of automated reasoning. 2014, Vol 52, Num 4, pp 451-480, issn 0168-7433, 30 p.Article

Full Functional Verification of Linked Data StructuresZEE, Karen; KUNCAK, Viktor; RINARD, Martin C et al.ACM SIGPLAN notices. 2008, Vol 43, Num 6, pp 349-361, issn 1523-2867, 13 p.Conference Paper

An Integrated Proof Language for Imperative ProgramsZEE, Karen; KUNCAK, Viktor; RINARD, Martin C et al.ACM SIGPLAN notices. 2009, Vol 44, Num 6, pp 338-351, issn 1523-2867, 14 p.Conference Paper

Formalization of the Standard Uniform random variableHASAN, Osman; TAHAR, Sofiène.Theoretical computer science. 2007, Vol 382, Num 1, pp 71-83, issn 0304-3975, 13 p.Article