357 results  save search

hal-01401812v1  Conference papers
Jasmin BlanchetteAymeric BouzyAndreas LochbihlerAndrei PopescuDmitriy Traytel. Friends with Benefits
Isabelle Workshop 2016, Aug 2016, Nancy, France
hal-01592186v1  Conference papers
Heiko BeckerJasmin BlanchetteUwe WaldmannDaniel Wand. A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.432-453, ⟨10.1007/978-3-319-63046-5_27⟩
inria-00637756v1  Journal articles
Dominique MéryNeeraj Kumar Singh. Formal Specification of Medical Systems by Proof-Based Refinement
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩
hal-01145407v1  Conference papers
Jean-Daniel BoissonnatKarthik C. S.Sébastien Tavenas. Building Efficient and Compact Data Structures for Simplicial Complexes
International Symposium on Computational Geometry 2015, Jun 2015, Eindhoven, Netherlands. ⟨10.4230/LIPIcs.SOCG.2015.642⟩
hal-01590899v2  Conference papers
Pascal FontaineMizuhito OgawaThomas SturmXuan Vu. Subtropical Satisfiability
FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. ⟨10.1007/978-3-319-66167-4⟩
hal-01648694v1  Conference papers
Russell BradfordJames DavenportMatthew EnglandHassan ErramiVladimir Gerdt et al.  A Case Study on the Parametric Occurrence of Multiple Steady States
ISSAC 2017 - International Symposium on Symbolic and Algebraic Computation, Jul 2017, Kaiserslautern, Germany. pp.45-52, ⟨10.1145/3087604.3087622⟩
hal-01648695v1  Journal articles
Thomas SturmErika AbrahamJohn AbbottBern W. BeckerAnna Bigatti et al.  Satisfiability Checking and Symbolic Computation
ACM Communications in Computer Algebra, Association for Computing Machinery (ACM), 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
hal-01946733v1  Conference papers
Pascal FontaineMizuhito OgawaThomas SturmVan Khanh ToXuan Tung Vu. Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom
hal-01442691v2  Reports
Haniel BarbosaPascal FontaineAndrew Reynolds. Congruence Closure with Free Variables
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
hal-01097624v1  Conference papers
Yamine Aït AmeurJ. Paul GibsonDominique Méry. On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium,, Tiziana Margaria and Bernhard Steffen, Oct 2014, Corfu, Greece. pp.604-618
hal-01097645v1  Conference papers
Dominique MéryNeeraj Kumar Singh. Formal Evaluation of Landing Gear System
SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam
inria-00536824v1  Conference papers
Joachim NiehrenAndreas PodelskiRalf Treinen. Equational and Membership Constraints for Infinite Trees
5th International Conference on Rewriting Techniques and Applications, 1993, Montreal, Canada. pp.106-120
inria-00193551v1  Book sections
Stefanie HahmannAlexander BelyaevLaurent BuséGershon ElberBernard Mourrain et al.  Shape Interrogation
Leila De Floriani, Michela Spagnuolo. Shape Analysis and Structuring, Springer, pp.1-51, 2008, Mathematics and Visualization, 978-3-540-33265-7. ⟨10.1007/978-3-540-33265-7_1⟩
hal-01235912v1  Reports
Haniel BarbosaPascal Fontaine. Congruence Closure with Free Variables (Work in Progress)
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France). 2015
hal-01336074v1  Conference papers
Jasmin Christian BlanchetteMathias FleuryChristoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. ⟨10.1007/978-3-319-40229-1_4⟩
hal-01336082v1  Conference papers
Andrew ReynoldsJasmin Christian BlanchetteSimon CruanesCesare Tinelli. Model Finding for Recursive Functions in SMT
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. ⟨10.1007/978-3-319-40229-1_10⟩
hal-01157898v1  Conference papers
Paula ChocronPascal FontaineChristophe Ringeissen. A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
25th International Conference on Automated Deduction, CADE-25, Christoph Benzmueller, Aug 2015, Berlin, Germany. pp.419-433, ⟨10.1007/978-3-319-21401-6_29⟩
hal-01377655v1  Conference papers
Eriká AbrahámJohn AbbottBernd BeckerAnna BigattiMartin Brain et al.  SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland
inria-00536539v1  Journal articles
Ernst AlthausDenys DuchierAlexander KollerKurt MehlhornJoachim Niehren et al.  An Efficient Graph Algorithm for Dominance Constraints
Journal of Algorithms in Cognition, Informatics and Logic, Elsevier, 2003, Special issue: Twelfth annual ACM-SIAM symposium on discrete algorithms, 48 (1), pp.194-219. ⟨10.1016/S0196-6774(03)00050-6⟩
hal-02296014v1  Journal articles
Alexander BentkampJasmin BlanchetteDietrich Klakow. A Formal Proof of the Expressiveness of Deep Learning
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
hal-01643157v1  Journal articles
Jasmin Christian BlanchetteAndrei PopescuDmitriy Traytel. Soundness and Completeness Proofs by Coinductive Methods
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. ⟨10.1007/s10817-016-9391-3⟩