1. Search
357 results  save search
...
hal-01401812v1  Conference papers
Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel. Friends with Benefits
Isabelle Workshop 2016, Aug 2016, Nancy, France
...
hal-01592186v1  Conference papers
Heiko Becker, Jasmin Blanchette, Uwe Waldmann, Daniel 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éry, Neeraj 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 Boissonnat, Karthik 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 Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan 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 Bradford, James Davenport, Matthew England, Hassan Errami, Vladimir 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 Sturm, Erika Abraham, John Abbott, Bern W. Becker, Anna 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-01648691v1  Conference papers
Matthew England, Hassan Errami, Dima Grigoriev, Ovidiu Radulescu, Thomas Sturm et al.  Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
CASC 2017 - 19th International Workshop on Computer Algebra in Scientific Computing, Sep 2017, Beijing, China. ⟨10.1007/978-3-319-66320-3⟩
...
hal-01946733v1  Conference papers
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To, Xuan 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 Barbosa, Pascal Fontaine, Andrew Reynolds. Congruence Closure with Free Variables
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
...
tel-01751181v2  Theses
Hernán Vanzetto. Proof automation and type synthesis for set theory in the context of TLA+
Computer Science [cs]. Université de Lorraine, 2014. English. ⟨NNT : 2014LORR0208⟩
hal-01097624v1  Conference papers
Yamine Aït Ameur, J. Paul Gibson, Dominique 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éry, Neeraj 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 Niehren, Andreas Podelski, Ralf Treinen. Equational and Membership Constraints for Infinite Trees
5th International Conference on Rewriting Techniques and Applications, 1993, Montreal, Canada. pp.106-120
...
hal-00644679v3  Reports
Konstantinos Karanasos, Asterios Katsifodimos, Ioana Manolescu, Spyros Zoupanos. The ViP2P Platform: XML Views in P2P
[Research Report] RR-7812, INRIA. 2011, pp.41
...
inria-00193551v1  Book sections
Stefanie Hahmann, Alexander Belyaev, Laurent Busé, Gershon Elber, Bernard 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 Barbosa, Pascal 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 Blanchette, Mathias Fleury, Christoph 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 Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare 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⟩
...
inria-00441622v1  Conference papers
Marc Stamminger, Daniel Wexler, Wolfram Kresse, Nicolas Holzschuch, Per Christensen. Advanced Radiosity: Complex Scenes and Glossy Reflections
Eurographics Tutorial, Aug 1999, Milano, Italy
...
hal-01157898v1  Conference papers
Paula Chocron, Pascal Fontaine, Christophe 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-01906155v1  Preprints, Working Papers, ...
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery. Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
2018
...
hal-01021930v3  Preprints, Working Papers, ...
Jérémie Chalopin, Shantanu Das, Pawel Gawrychowski, Adrian Kosowski, Arnaud Labourel et al.  Lock-in Problem for Parallel Rotor-router Walks
2015
...
hal-01377655v1  Conference papers
Eriká Abrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain et al.  SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland
...
inria-00536539v1  Journal articles
Ernst Althaus, Denys Duchier, Alexander Koller, Kurt Mehlhorn, Joachim 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-01386986v1  Journal articles
Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban. A Learning-Based Fact Selector for Isabelle/HOL
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. ⟨10.1007/s10817-016-9362-8⟩
...
hal-02296014v1  Journal articles
Alexander Bentkamp, Jasmin Blanchette, Dietrich 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 Blanchette, Andrei Popescu, Dmitriy 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⟩

Contact

CCSD