Filtrer vos résultats
- 21
- 7
- 12
- 9
- 5
- 1
- 1
- 9
- 23
- 2
- 1
- 1
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 2
- 2
- 2
- 1
- 1
- 2
- 1
- 1
- 1
- 1
- 1
- 3
- 25
- 3
- 21
- 20
- 5
- 4
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 28
- 11
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
28 résultats
|
|
|
triés par
|
|
|
A Logical Framework to Prove Properties of Alpha Programs (revised version)[Research Report] RR-3177, INRIA. 1997
Rapport
inria-00073512v1
|
||
|
|
Comparing Techniques for Certified Static AnalysisThe NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. pp.111-115
Communication dans un congrès
inria-00538772v1
|
||
|
|
Inference of polynomial invariants for imperative programs: a farewell to Gröbner basesScience of Computer Programming, 2014, 93, pp.21. ⟨10.1016/j.scico.2014.02.028⟩
Article dans une revue
hal-00932351v1
|
||
Combining Constraint Languages via Abstract Interpretation2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI), Nov 2019, Portland, France. pp.50-58, ⟨10.1109/ICTAI.2019.00016⟩
Communication dans un congrès
hal-02945596v1
|
|||
|
|
Proving Data-Parallel Programs : a Unifying Approach[Research Report] RR-3032, INRIA. 1996
Rapport
inria-00073661v1
|
||
|
|
Octogones entiers pour le problème RCPSPJFPC 2019 - Journées Francophones de Programmation par Contraintes, Jun 2019, Albi, France. pp.1-10
Communication dans un congrès
hal-02157804v1
|
||
|
|
Verifying a Concurrent Garbage Collector using a Rely-Guarantee MethodologyITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩
Communication dans un congrès
hal-01613389v1
|
||
|
|
Certified Static Analysis by Abstract InterpretationFoundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257
Communication dans un congrès
inria-00538753v1
|
||
|
|
Validation formelle des langages à parallélisme de donnéesGénie logiciel [cs.SE]. École normale supérieure de Lyon - ENS Lyon, 1998. Français. ⟨NNT : ⟩
Thèse
tel-00425390v1
|
||
|
|
An ω-Algebra for Real-Time Energy Problems35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2015, Bengaluru, India. pp.394
Communication dans un congrès
hal-01237667v1
|
||
|
|
Compilation of Linearizable Data Structures[Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017
Rapport
hal-01538128v1
|
||
|
|
Extracting a data flow analyser in constructive logicTheoretical Computer Science, 2005, 342 (1), pp.56-78. ⟨10.1016/j.tcs.2005.06.004⟩
Article dans une revue
inria-00564611v1
|
||
|
|
Extracting a Data Flow Analyser in Constructive LogicESOP, 2004, Barcelona, Spain
Communication dans un congrès
inria-00564633v1
|
||
|
|
Advances in Bit Width Selection Methodology[Research Report] RR-4452, INRIA. 2002
Rapport
inria-00072136v1
|
||
Long-Run Cost Analysis by Approximation of Linear Operators over DioidsMathematical Structures in Computer Science, 2010, 20 (4), pp.589-624. ⟨10.1017/S0960129510000113⟩
Article dans une revue
hal-00699608v1
|
|||
|
|
Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic RefinementSAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩
Communication dans un congrès
hal-01653620v1
|
||
|
|
Formal Validation of Data-Parallel Programs : a Two-Component Assertional Proof System for a Simple Language[Research Report] RR-3033, INRIA. 1996
Rapport
inria-00073660v1
|
||
|
|
A Logical Framework to Prove Properties of Alpha Programs[Research Report] RR-3031, INRIA. 1996
Rapport
inria-00073662v1
|
||
|
|
Verification of Control Properties in the Polyhedral Model[Research Report] RR-4756, INRIA. 2003
Rapport
inria-00071830v1
|
||
Inference of polynomial invariants for imperative programs: a farewell to Gröbner basesSAS - 19th International Static Analysis Symposium - 2012, Sep 2012, Deauville, France
Communication dans un congrès
hal-00758890v1
|
|||
|
|
A Certified Denotational Abstract InterpreterInternational Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. pp.9-24
Communication dans un congrès
inria-00537810v1
|
||
|
|
Fast inference of polynomial invariants for imperative programs[Research Report] RR-7627, INRIA. 2011, pp.31
Rapport
inria-00595783v1
|
||
Programmation d'un interpréteur abstrait certifié en logique constructiveRevue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2011, pp.28. ⟨10.3166/tsi.30.381-408⟩
Article dans une revue
istex
hal-01112680v1
|
|||
|
|
Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩
Article dans une revue
hal-01897251v1
|
||
|
|
An Extended Buffered Memory Model With Full ReorderingsFtFjp - Ecoop workshop, Jul 2016, Rome, Italy. pp.1 - 6, ⟨10.1145/2955811.2955816⟩
Communication dans un congrès
hal-01379514v1
|
||
|
|
Long-Run Cost Analysis by Approximation of Linear Operators over Dioids[Research Report] RR-6338, INRIA. 2007, pp.35
Rapport
inria-00182338v4
|
||
|
|
Proving Parameterized Systems: the use of pseudo-pipelines in polyhedral logicCorrect Hardware Design and Verification Methods, springer, pp.376-379, 2005, 978-3-540-29105-3. ⟨10.1007/11560548_35⟩
Chapitre d'ouvrage
hal-00102816v1
|
||
Designing parallel programs and integrated circuitsInternational Mathematica Symposium (IMS'06), 2006, Avignon, France. 13 p
Communication dans un congrès
hal-00142674v1
|