Filtrer vos résultats
- 226
- 101
- 187
- 53
- 26
- 15
- 11
- 8
- 7
- 5
- 4
- 3
- 3
- 2
- 1
- 1
- 1
- 16
- 7
- 311
- 13
- 12
- 2
- 2
- 1
- 1
- 46
- 37
- 40
- 45
- 36
- 36
- 52
- 13
- 3
- 5
- 1
- 3
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 275
- 52
- 320
- 218
- 23
- 21
- 17
- 16
- 14
- 13
- 11
- 11
- 10
- 9
- 9
- 9
- 8
- 8
- 8
- 7
- 7
- 7
- 6
- 6
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 38
- 33
- 32
- 31
- 25
- 22
- 22
- 21
- 19
- 18
- 18
- 17
- 15
- 15
- 13
- 13
- 12
- 12
- 9
- 9
- 9
- 9
- 8
- 8
- 7
- 7
- 7
- 7
- 6
- 6
- 6
- 6
- 6
- 6
- 6
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
327 résultats
|
|
A Coq Mechanised Formal Semantics for Realistic SQL QueriesCPP 19, ACM, Jan 2019, Cascais, Portugal. pp.249-261, ⟨10.1145/3293880.3294107⟩
Communication dans un congrès
hal-01955433v1
|
||
|
|
Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matricielsAFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2019, Toulouse, France
Communication dans un congrès
hal-02391924v1
|
||
|
|
Arithmétique des Ordinateurs et Preuves FormellesJFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Communication dans un congrès
hal-02013540v1
|
||
|
|
Alt-Ergo 2.2SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
Communication dans un congrès
hal-01960203v1
|
||
|
|
Recent Developments in OCL and Textual ModellingInternational Workshop on OCL and Textual Modeling (OCL 2016), Oct 2016, Saint-Malo, France. pp.157 - 165
Communication dans un congrès
hal-01589574v1
|
||
|
|
Formally Verified Approximations of Definite IntegralsInteractive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩
Communication dans un congrès
hal-01289616v2
|
||
|
|
Infeasible Path Detection : a Formal Model and an AlgorithmOther [cs.OH]. Université Paris Saclay (COmUE), 2017. English. ⟨NNT : 2017SACLS036⟩
Thèse
tel-01567093v1
|
||
|
|
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016, Jul 2016, Coimbra, Portugal
Communication dans un congrès
hal-01388984v1
|
||
Monadic Sequence Testing and Explicit Test-RefinementsTests and Proofs - 10th International Conference, 2016, Vienna, France
Communication dans un congrès
hal-01765528v1
|
|||
Automatic Skeleton Generation for Data-Aware Service Choreographies24th IEEE International Symposium on Software Reliability Engineering, ISSRE 2013, Nov 2013, Pasadena, CA, United States. pp.320-329, ⟨10.1109/ISSRE.2013.6698885⟩
Communication dans un congrès
hal-01216413v1
|
|||
|
|
SMTCoq: automatisation expressive et extensible dans CoqJFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Communication dans un congrès
hal-02369249v1
|
||
|
|
Manifestability Verification of Discrete Event SystemsDX 2019 - 30th International Workshop on Principles of Diagnosis, Nov 2019, Klagenfurt, Austria. pp.1-9
Communication dans un congrès
hal-02425146v1
|
||
Automated Certified Proofs with CiME3RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia
Communication dans un congrès
hal-00777669v1
|
|||
Towards a Tool for Featherweight OCL: A Case Study On Semantic ReflectionProceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Sep 2014, Valencia, Spain
Communication dans un congrès
hal-01214466v1
|
|||
|
|
Generic decision procedures for axiomatic first-order theoriesOther [cs.OH]. Université Paris Sud - Paris XI, 2014. English. ⟨NNT : 2014PA112059⟩
Thèse
tel-01002190v1
|
||
|
|
A3PAT, an Approach for Certified Automated Termination Proofs2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Communication dans un congrès
inria-00535655v1
|
||
Test Program Generation for a Microprocessor -- A Case-StudyProceedings of the 6th Intl. Conf. on Test and Proof (TAP '13), 2013, Budapest, France
Communication dans un congrès
hal-01765545v1
|
|||
|
|
Adding Decision Procedures to SMT Solvers using Axioms with Triggers2013
Pré-publication, Document de travail
hal-00915931v1
|
||
|
|
Why3 -- Where Programs Meet ProversESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy
Communication dans un congrès
hal-00789533v1
|
||
|
|
Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrièresJFLA, Jan 2014, Fréjus, France
Communication dans un congrès
hal-01088655v1
|
||
|
|
The COST IC0701 Verification Competition 2011Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy
Communication dans un congrès
hal-00789525v1
|
||
|
|
A Formally-Verified C Compiler Supporting Floating-Point ArithmeticArith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
Communication dans un congrès
hal-00743090v2
|
||
|
|
Dag-calculus: a calculus for parallel computationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Sep 2016, Nara, Japan. pp.18 - 32, ⟨10.1145/2951913.2951946⟩
Communication dans un congrès
hal-01409022v1
|
||
Des ordinateurs capables de calculer plus justeLa Recherche, 2014, pp.46-53
Article dans une revue
ensl-01069744v1
|
|||
|
|
Automatically verified implementation of data structures based on AVL trees6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès
hal-01067217v1
|
||
|
|
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. ProceedingsBlazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩
Ouvrages
hal-00908865v1
|
||
|
|
Formalizing Semantics with an Automatic Program Verifier6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès
hal-01067197v1
|
||
|
|
A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System Testing15th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS 2017, Sep 2017, Berlin, Germany. ⟨10.1007/978-3-319-65765-3_18⟩
Communication dans un congrès
hal-01583815v1
|
||
|
|
Towards a formal semantics of the TESL specification language3rd International Workshop on the Globalization Of Modeling Languages (GEMOC 2015), Benoit Combemale; Julien Deantoni; Jeff Gray, Sep 2015, Ottawa, Canada. pp.14-19
Communication dans un congrès
hal-01239669v1
|
||
|
|
Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific LanguagesProgramming Languages [cs.PL]. Université Paris Saclay (COmUE), 2016. English. ⟨NNT : 2016SACLS085⟩
Thèse
tel-01318156v1
|