Journal articles

2014

auteur
Jade Alglave, Luc Maranget, Michael Tautschnig
titre
Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (2), pp.7:1--7:74. ⟨10.1145/2627752⟩
DOI
DOI : 10.1145/2627752
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081364/file/a7-alglave.pdf BibTex
auteur
Siva Anantharaman, Christopher Bouchard, Paliath Narendran, Michaël Rusinowitch
titre
Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (1:5), pp. 1--26. ⟨10.2168/LMCS-10(1:5)2014⟩
DOI
DOI : 10.2168/LMCS-10(1:5)2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00854841/file/dbctheory-LMCS2014.pdf BibTex
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
titre
Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version)
article
Computer Science and Information Systems, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. ⟨10.2298/CSIS130122007A⟩
DOI
DOI : 10.2298/CSIS130122007A
Accès au bibtex
BibTex
auteur
Myrto Arapinis, Marie Duflot
titre
Bounding messages for free in security protocols – extension to various security properties
article
Information and Computation, Elsevier, 2014, pp.34. ⟨10.1016/j.ic.2014.09.003⟩
DOI
DOI : 10.1016/j.ic.2014.09.003
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01083657/file/versionjournal.pdf BibTex
auteur
Myrto Arapinis, Stéphanie Delaune, Steve Kremer
titre
Dynamic Tags for Security Protocols
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (2), pp.50. ⟨10.2168/LMCS-10(2:11)2014⟩
DOI
DOI : 10.2168/LMCS-10(2:11)2014
Accès au bibtex
https://arxiv.org/pdf/1405.2738 BibTex
auteur
Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune
titre
Modeling and Verifying Ad Hoc Routing Protocols
article
Information and Computation, Elsevier, 2014, 238, pp.38
Accès au bibtex
BibTex
auteur
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, Benoît Valiron
titre
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10:4 (8), pp.40. ⟨http://lmcs-online.org/ojs/viewarticle.php?id=1567⟩. ⟨10.2168/LMCS-10(4:8)2014⟩
DOI
DOI : 10.2168/LMCS-10(4:8)2014
Accès au bibtex
https://arxiv.org/pdf/1005.2897 BibTex
auteur
Emilie Balland, Pierre-Etienne Moreau, Antoine Reilles
titre
Effective Strategic Programming for Java Developers
article
International Journal on Software - Practice and Experience, 2014, Software: Practice and Experience, 44 (2), pp.34. ⟨http://onlinelibrary.wiley.com/doi/10.1002/spe.2159/abstract⟩. ⟨10.1002/spe.2159⟩
DOI
DOI : 10.1002/spe.2159
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01265319/file/final.pdf BibTex
auteur
Walid Belkhir, Alain Giorgetti, Michel Lenczner
titre
A Symbolic Transformation Language and its Application to a Multiscale Method
article
Journal of Symbolic Computation, Elsevier, 2014, 65, pp.49 - 78
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00917323/file/0.pdf BibTex
auteur
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
titre
Implementing and reasoning about hash-consed data structures in Coq
article
Journal of Automated Reasoning, Springer Verlag, 2014, 53 (3), pp.271-304. ⟨10.1007/s10817-014-9306-0⟩
DOI
DOI : 10.1007/s10817-014-9306-0
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00881085/file/main.pdf BibTex
auteur
Christopher W. Brown, Marek Kosta
titre
Constructing a single cell in cylindrical algebraic decomposition
article
Journal of Symbolic Computation, Elsevier, 2014, pp.35
Accès au bibtex
BibTex
auteur
Jérome Cantenot, Fabrice Ambert, Fabrice Bouquet
titre
Test generation with SMT solvers in Model Based Testing
article
Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2014, 24 (7), pp.33. ⟨10.1002/stvr.1537⟩
DOI
DOI : 10.1002/stvr.1537
Accès au bibtex
BibTex
auteur
Yan Chen, Joshua Dunfield, Matthew A. Hammer, Umut A. Acar
titre
Implicit self-adjusting computation for purely functional programs
article
Journal of Functional Programming, Cambridge University Press (CUP), 2014, 24 (1), pp.56-112
Accès au bibtex
BibTex
auteur
Jingshu Chen, Marie Duflot, Stephan Merz
titre
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
article
Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14. ⟨http://journal.ub.tu-berlin.de/eceasst/article/view/978⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087871/file/postproceedings.pdf BibTex
auteur
Asma Cherif, Abdessamad Imine, Michael Rusinowitch
titre
Practical access control management for distributed collaborative editors
article
Pervasive and Mobile Computing, Elsevier, 2014, pp.62-86
Accès au bibtex
BibTex
auteur
Véronique Cortier, Graham Steel
titre
A Generic Security API for Symmetric Key Management on Cryptographic Devices
article
Information and Computation, Elsevier, 2014, 238, pp.25
Accès au bibtex
BibTex
auteur
Véronique Cortier, Steve Kremer
titre
Formal Models and Techniques for Analyzing Security Protocols: A Tutorial
article
Foundations and Trends in Programming Languages, Now Publishers, 2014, 1 (3), pp.117. ⟨10.1561/2500000001⟩
DOI
DOI : 10.1561/2500000001
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01090874/file/CK-fntpl-14.pdf BibTex
auteur
Pierre-Évariste  Dagand, Conor  Mcbride
titre
Transporting functions across ornaments
article
Journal of Functional Programming, Cambridge University Press (CUP), 2014, 24 (2-3), pp.67. ⟨10.1017/S0956796814000069⟩
DOI
DOI : 10.1017/S0956796814000069
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00922581/file/paper_colour.pdf https://hal.inria.fr/hal-00922581/file/paper_bw.pdf BibTex
auteur
David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
titre
Integrating SMT solvers in Rodin
article
Science of Computer Programming, Elsevier, 2014, Abstract State Machines, Alloy, B, VDM, and Z — Selected and extended papers from ABZ 2012, 94, pp.14
Accès au bibtex
BibTex
auteur
Aloïs Dreyfus, Pierre-Cyrille Héam, Olga Kouchnarenko, Catherine Masson
titre
A random testing approach using pushdown automata
article
Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2014, 24, pp.656 - 683. ⟨10.1002/stvr.1526⟩
DOI
DOI : 10.1002/stvr.1526
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088712/file/STVR-Hal.pdf BibTex
auteur
Hugo Férée, Walid Gomaa, Mathieu Hoyrup
titre
Analytical properties of resource-bounded real functionals
article
Journal of Complexity, Elsevier, 2014, 30 (5), pp.33. ⟨10.1016/j.jco.2014.02.008⟩
DOI
DOI : 10.1016/j.jco.2014.02.008
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00848482/file/submitted_version.pdf BibTex
auteur
David Galindo, Srinivas Vivek
titre
Limits of a conjecture on a leakage-resilient cryptosystem
article
Information Processing Letters, Elsevier, 2014, 114 (4), pp.192-196. ⟨10.1016/j.ipl.2013.11.014⟩
DOI
DOI : 10.1016/j.ipl.2013.11.014
Accès au bibtex
BibTex
auteur
David Galindo
titre
Compact hierarchical identity-based encryption based on a harder decisional problem
article
International Journal of Computer Mathematics, Taylor & Francis, 2014, ⟨10.1080/00207160.2014.912278⟩
DOI
DOI : 10.1080/00207160.2014.912278
Accès au bibtex
BibTex
auteur
Pierre Genevès, Nabil Layaïda
titre
Equipping IDEs with XML-Path Reasoning Capabilities
article
ACM Transactions on Internet Technology, Association for Computing Machinery, 2014, 13 (4), pp.20. ⟨10.1145/2602573⟩
DOI
DOI : 10.1145/2602573
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00868723/file/xqdeadcode.pdf BibTex
auteur
Marek Kosta, Pavol Duris
titre
Flip-Pushdown Automata with k Pushdown Reversals and E0L Systems are Incomparable
article
Information Processing Letters, Elsevier, 2014, 114 (8), pp.417-420
Accès au bibtex
BibTex
auteur
Manuel Lamotte-Schubert, Christoph Weidenbach
titre
BDI: a new decidable clause class
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (6), pp.28
Accès au bibtex
BibTex
auteur
Dominique Larchey-Wendling
titre
The formal strong completeness of partial monoidal Boolean BI
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014, ⟨10.1093/logcom/exu031⟩
DOI
DOI : 10.1093/logcom/exu031
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01256932/file/larchey-jlc-rd-init.pdf BibTex
auteur
Gerald Lüttgen, Stephan Merz
titre
Editorial: Special Issue of Automated Verification of Critical Systems
article
Science of Computer Programming, Elsevier, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
Accès au bibtex
BibTex
auteur
Dominique Méry, Bernhard Schätz, Alan Wassyng
titre
The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
article
Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2014, 4 (2), pp.17--37
Accès au bibtex
BibTex
auteur
Mathieu Razafimahazo, Nabil Layaïda, Pierre Genevès, Thibaud Michel
titre
Mobile Augmented Reality Applications for Smart Cities
article
ERCIM News, ERCIM, 2014, ERCIM News 98, pp.45-46
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102797/file/vital-iot.eu_sites_default_files_EN98-web.pdf BibTex
auteur
Bin Yang, Walid Belkhir, Michel Lenczner
titre
Computer-Aided Derivation of Multi-scale Models: A Rewriting Framework
article
International Journal for Multiscale Computational Engineering, Begell House, 2014, 12 (2), pp.91--114
Accès au bibtex
https://arxiv.org/pdf/1302.2224 BibTex

2013

auteur
Jean-Christophe Bach
titre
Une approche hybride GPL-DSL pour transformer des modèles
article
Technique et Science Informatiques, Hermès-Lavoisier, 2013, 33 (3), pp.26. ⟨http://tsi.revuesonline.com/article.jsp?articleId=19256⟩. ⟨10.3166/tsi.33.175-201⟩
DOI
DOI : 10.3166/tsi.33.175-201
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00786254/file/bachTSI2014.pdf BibTex
auteur
Mathieu Baudet, Véronique Cortier, Stéphanie Delaune
titre
YAPA: A generic tool for computing intruder knowledge
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 14 (1), ⟨10.1145/2422085.2422089⟩
DOI
DOI : 10.1145/2422085.2422089
Accès au bibtex
BibTex
auteur
Alexis Bernadet, Stéphane Graham-Lengrand
titre
Non-idempotent intersection types and strong normalisation
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), pp.17-42
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00906778/file/Journal13.pdf BibTex
auteur
Olivier Bournez, Daniel Graça, Emmanuel Hainry
titre
Computation with perturbed dynamical systems
article
Journal of Computer and System Sciences, Elsevier, 2013, 79 (5), pp.714-724. ⟨10.1016/j.jcss.2013.01.025⟩
DOI
DOI : 10.1016/j.jcss.2013.01.025
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00643634/file/jcss13.pdf BibTex
auteur
Marc Caillet, Cécile Roisin, Jean Carrive
titre
Multimedia applications for playing with digitized theater performances
article
Multimedia Tools and Applications, Springer Verlag, 2013, ⟨10.1007/s11042-013-1651-1 ⟩
DOI
DOI : 10.1007/s11042-013-1651-1 
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00855102/file/mtapPrePrint.pdf BibTex
auteur
Vincent Cheval, Véronique Cortier, Stéphanie Delaune
titre
Deciding equivalence-based properties using constraint solving
article
Theoretical Computer Science, Elsevier, 2013, 492, pp.1-39. ⟨10.1016/j.tcs.2013.04.016⟩
DOI
DOI : 10.1016/j.tcs.2013.04.016
Accès au bibtex
BibTex
auteur
Céline Chevalier, Stéphanie Delaune, Steve Kremer, Mark D. Ryan
titre
Composition of Password-based Protocols
article
Formal Methods in System Design, Springer Verlag, 2013, 43 (3), pp.369-413. ⟨10.1007/s10703-013-0184-6⟩
DOI
DOI : 10.1007/s10703-013-0184-6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00878640/file/CDKR-fmsd13.pdf BibTex
auteur
Véronique Cortier, Ben Smyth
titre
Attacking and fixing Helios: An analysis of ballot secrecy
article
Journal of Computer Security, IOS Press, 2013, 21 (1), pp.89-148. ⟨10.3233/JCS-2012-0458⟩
DOI
DOI : 10.3233/JCS-2012-0458
Accès au bibtex
BibTex
auteur
David Galindo
titre
A note on an IND-CCA2 secure Paillier-based cryptosystem
article
Information Processing Letters, Elsevier, 2013, 113 (22-24), pp.913-914. ⟨10.1016/j.ipl.2013.09.008⟩
DOI
DOI : 10.1016/j.ipl.2013.09.008
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Mery
titre
A Connection-based Characterization of Bi-intuitionistic Validity
article
Journal of Automated Reasoning, Springer Verlag, 2013, 51 (1), pp.3--26. ⟨10.1007/s10817-013-9279-4⟩
DOI
DOI : 10.1007/s10817-013-9279-4
Accès au bibtex
BibTex
auteur
Mathieu Hoyrup
titre
Computability of the ergodic decomposition
article
Annals of Pure and Applied Logic, Elsevier Masson, 2013, 164 (5), pp.542-549. ⟨10.1016/j.apal.2012.11.005⟩
DOI
DOI : 10.1016/j.apal.2012.11.005
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00746473/file/paper.pdf BibTex
auteur
Abdessamad Imine, Michael Rusinowitch
titre
Secure Collaboration for Smartphones
article
ERCIM News, ERCIM, 2013
Accès au bibtex
BibTex
auteur
Emmanuel Jeandel, Guillaume Theyssier
titre
Subshifts as models for MSO logic
article
Information and Computation, Elsevier, 2013, pp.1-15. ⟨10.1016/j.ic.2013.01.003⟩
DOI
DOI : 10.1016/j.ic.2013.01.003
Accès au bibtex
BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Turing degrees of multidimensional subshifts
article
Theoretical Computer Science, Elsevier, 2013, http://dx.doi.org/10.1016/j.tcs.2012.08.027. ⟨10.1016/j.tcs.2012.08.027⟩
DOI
DOI : 10.1016/j.tcs.2012.08.027
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00613165/file/tcs-arxiv.pdf BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Characterizations of periods of multi-dimensional shifts
article
Ergodic Theory and Dynamical Systems, Cambridge University Press (CUP), 2013, FirstView, pp.1--30. ⟨10.1017/etds.2013.60⟩
DOI
DOI : 10.1017/etds.2013.60
Accès au bibtex
BibTex
auteur
Dominique Larchey-Wendling, Didier Galmiche
titre
Nondeterministic Phase Semantics and the Undecidability of Boolean BI
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 14 (1), pp.6. ⟨10.1145/2422085.2422091⟩
DOI
DOI : 10.1145/2422085.2422091
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01256956/file/dlwgal_submitted.pdf BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Formal Specification of Medical Systems by Proof-Based Refinement
article
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩
DOI
DOI : 10.1145/2406336.2406351
Accès au bibtex
BibTex
auteur
Gérard Morel, Jean-Marc Dupont, Romain Lieber, Fabien Bouffaron, Dominique Méry, Frédérique Mayer, Jean-Luc Marty
titre
Spécification d'exigences physico-physiologiques d'interaction homme-machine en ingénierie système
article
Génie logiciel, C & S, 2013, Mars 2013 (104), pp.29-39
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00805851/file/Specification_d_exigences_physico-physiologique_d_interaction_homme-machine_en_Ingenierie_Systeme.pdf.pdf BibTex
auteur
François Pottier
titre
Syntactic soundness proof of a type-and-capability system with hidden state
article
Journal of Functional Programming, Cambridge University Press (CUP), 2013, 23 (1), pp.38-144. ⟨10.1017/S0956796812000366⟩
DOI
DOI : 10.1017/S0956796812000366
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00877589/file/fpottier-ssphs.pdf BibTex
auteur
Martin Quinson, Jean-Christophe Bach
titre
Idée reçue : l'informatique nomade, c'est la liberté !
article
Interstices, INRIA, 2013
Accès au bibtex
BibTex
auteur
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
titre
A step-indexed Kripke Model of Hidden State
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (1), pp.1--54
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772757/file/sikmhs.pdf BibTex

Conference papers

2014

auteur
Pietro Abate, Roberto Di Cosmo, Louis Gesbert, Fabrice Le Fessant, Stefano Zacchiroli
titre
Using Preferences to Tame your Package Manager
article
OCaml 2014, Sep 2014, Goteborg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091177/file/ocaml2014_17.pdf BibTex
auteur
Umut A. Acar, Arthur Charguéraud, Mike Rainey
titre
Theory and Practice of Chunked Sequences
article
European Symposium on Algorithms, Sep 2014, Wrocław, Poland. pp.25 - 36, ⟨10.1007/978-3-662-44777-2_3⟩
DOI
DOI : 10.1007/978-3-662-44777-2_3
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087245/file/chunkedseq.pdf BibTex
auteur
Jade Alglave, Luc Maranget, Michael Tautschnig
titre
Herding cats: Modelling, simulation, testing, and data-mining for weak memory
article
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2014, Edinburg, United Kingdom. pp.40, ⟨10.1145/2594291.2594347⟩
DOI
DOI : 10.1145/2594291.2594347
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081413/file/p40-alglave.pdf BibTex
auteur
Yamine Aït Ameur, J. Paul Gibson, Dominique Méry
titre
On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
article
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
Accès au bibtex
BibTex
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
titre
Analysis of Self-* and P2P Systems using Refinement
article
ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Yamine AIT AMEUR and Klaus-Dieter SCHEWE, Jun 2014, Toulouse, France. pp.117-123, ⟨10.1007/978-3-662-43652-3_9⟩
DOI
DOI : 10.1007/978-3-662-43652-3_9
Accès au bibtex
BibTex
auteur
Thibaut Balabonski, François Pottier, Jonathan Protzenko
titre
Type Soundness and Race Freedom for Mezzo
article
FLOPS 2014: 12th International Symposium on Functional and Logic Programming, Jun 2014, Kanazawa, Japan. pp.253 - 269, ⟨10.1007/978-3-319-07151-0_16⟩
DOI
DOI : 10.1007/978-3-319-07151-0_16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081194/file/bpp-mezzo.pdf BibTex
auteur
Philippe Balbiani, Vincent Demange, Didier Galmiche
titre
A sequent calculus with labels for Public Announcement Logic
article
Int. Conference on Advances in Modal Logic, AiML 2014, 2014, Groningen, Netherlands
Accès au bibtex
BibTex
auteur
Clark Barrett, Leonardo de Moura, Pascal Fontaine
titre
Proofs in satisfiability modulo theories
article
APPA (All about Proofs, Proofs for All), Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
auteur
Peter Baumgartner, Joshua Bax, Uwe Waldmann
titre
Finite Quantification in Hierarchic Theorem Proving
article
7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. pp.152-167
Accès au bibtex
BibTex
auteur
Bruno Bauwens
titre
Asymmetry of the Kolmogorov complexity of online predicting odd and even bits
article
STACS - 31th Symposium on Theoretical Aspects of Computer Science - 2014, Mar 2014, Lyon, France
Accès au bibtex
BibTex
auteur
Walid Belkhir, Gisela Rossi, Michael Rusinowitch
titre
A Parametrized Propositional Dynamic Logic with Application to Service Synthesis
article
Advances in Modal Logic, Aug 2014, Groningen, Netherlands. pp.34-53
Accès au bibtex
BibTex
auteur
Pramod Bhatotia, Umut A. Acar, Flavio P. Junqueira, Rodrigo Rodrigues
titre
Slider: Incremental Sliding Window Analytics
article
Middleware 2014: Proceedings of the 15th International Middleware Conference, Dec 2014, Bordeaux, France. ⟨10.1145/2663165.2663334⟩
DOI
DOI : 10.1145/2663165.2663334
Accès au bibtex
BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet
titre
Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus
article
Mathematical Foundations of Programming Semantics Thirtieth Conference, Jun 2014, Ithaca, United States. pp.49 - 64, ⟨10.1016/j.entcs.2014.10.004⟩
DOI
DOI : 10.1016/j.entcs.2014.10.004
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01080960/file/lambdamuentcs.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Thanh Dinh Ta
titre
Malware Message Classification by Dynamic Analysis
article
The 7th International Symposium on Foundations and Practice of Security, Nov 2014, Montreal, Canada. pp.16
Accès au bibtex
BibTex
auteur
Martí Bosch, Pierre Genevès, Nabil Layaïda
titre
Automated Refactoring for Size Reduction of CSS Style Sheets
article
Proceedings of the 2014 ACM symposium on Document engineering, Sep 2014, Fort Collins, Denver, United States. ⟨10.1145/2644866.2644885⟩
DOI
DOI : 10.1145/2644866.2644885
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081876/file/doc085s-bosch.pdf BibTex
auteur
Thomas Braibant, Jonathan Protzenko, Gabriel Scherer
titre
Well-typed generic smart-fuzzing for APIs
article
ML'14 - ACM SIGPLAN ML Family Workshop, Aug 2014, Göteborg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094006/file/articheck-ml-workshop-extended-abstract.pdf BibTex
auteur
Hadrien Bride, Olga Kouchnarenko, Fabien Peureux
titre
Verifying Modal Workflow Specifications Using Constraint Solving
article
The 11th International Conference on Integrated Formal Methods, IFM'2014, Sep 2014, Bertinoro, Italy. pp.171 - 186, ⟨10.1007/978-3-319-10181-1_11⟩
DOI
DOI : 10.1007/978-3-319-10181-1_11
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091283/file/BrideKP_2014.pdf BibTex
auteur
Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani
titre
Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation
article
POPL '14, 41th ACM Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. pp.5-17, ⟨10.1145/2535838.2535840⟩
DOI
DOI : 10.1145/2535838.2535840
Accès au bibtex
BibTex
auteur
David Cattanéo, Simon Perdrix
titre
The Parameterized Complexity of Domination-type Problems and Application to Linear Codes
article
Theory and Applications of Models of Computation, Apr 2014, Chennai, India. pp.86-103, ⟨10.1007/978-3-319-06089-7_7⟩
DOI
DOI : 10.1007/978-3-319-06089-7_7
Accès au bibtex
https://arxiv.org/pdf/1209.5267 BibTex
auteur
Yan Chen, Umut A. Acar, Kanat Tangwongsan
titre
Functional Programming for Dynamic and Large Data with Self-Adjusting Computation
article
ICFP 2014: 19th ACM SIGPLAN International Conference on Functional Programming, Sep 2014, Gothenburg, Sweden. ⟨10.1145/2628136.2628150⟩
DOI
DOI : 10.1145/2628136.2628150
Accès au bibtex
BibTex
auteur
James Cheney, Ahmed Amal, Umut A. Acar
titre
Database Queries that Explain their Work
article
PPDP 2014: 16th International Symposium on Principles and Practice of Declarative Programming, Sep 2014, Canterbury, United Kingdom. ⟨10.1145/2643135.2643143⟩
DOI
DOI : 10.1145/2643135.2643143
Accès au bibtex
BibTex
auteur
Paul Chippendale, Valeria Tomaselli, Viviana d'Alto, Giulio Urlini, Carla Maria Modena, Stefano Messelodi, Sebastiano Mauro Strano, Günter Alce, Klas Hermodsson, Mathieu Razafimahazo, Thibaud Michel, Maria Farinella Giovanni
titre
Personal Shopping Assistance and Navigator System for Visually Impaired People
article
ACVR2014: Second Workshop on Assistive Computer Vision and Robotics, Sep 2014, Zurich, Switzerland
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102707/file/PChippendale_PersonalShoppingAssistance_2014.pdf BibTex
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
titre
Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
article
Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures
article
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. pp.122-136, ⟨10.1007/978-3-319-08587-6_9⟩
DOI
DOI : 10.1007/978-3-319-08587-6_9
Accès au bibtex
BibTex
auteur
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
titre
Typing messages for free in security protocols: the~case of equivalence properties
article
25th International Conference on Concurrency Theory (CONCUR'14), Sep 2014, Rome, Italy
Accès au bibtex
BibTex
auteur
Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri
titre
A tool for automating the computationally complete symbolic attacker (Extended Abstract)
article
Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography (FCS-FCC'14), Jul 2014, Vienne, Austria
Accès au bibtex
BibTex
auteur
Sylvain Conchon, Luc Maranget, Alain Mebsout, David Declerck
titre
Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières
article
JFLA, Jan 2014, Fréjus, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088655/file/main.pdf BibTex
auteur
Véronique Cortier, David Galindo, Stephane Glondu, Malika Izabachène
titre
Election Verifiability for Helios under Weaker Trust Assumptions
article
Proceedings of the 19th European Symposium on Research in Computer Security (ESORICS'14), Sep 2014, Wroclaw, Poland
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Electronic Voting: How Logic Can Help
article
12th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienne, Austria
Accès au bibtex
BibTex
auteur
Pierrick Couderc, Benjamin Canou, Pierre Chambart, Fabrice Le Fessant
titre
A Proposal for Non-Intrusive Namespaces in OCaml
article
OCaml 2014, Sep 2014, Goteborg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091173/file/ocaml2014_8.pdf BibTex
auteur
Julien Cretin, Didier Rémy
titre
System F with Coercion Constraints
article
CSL-LICS 2014: Joint Meeting of the Annual Conference on Computer Science Logic and the Annual Symposium on Logic in Computer Science, Jul 2014, Vienna, Austria. pp.34, ⟨10.1145/2603088.2603128⟩
DOI
DOI : 10.1145/2603088.2603128
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093239/file/Cretin-Remy%21fcc%40lics2014.pdf BibTex
auteur
Frédéric Dadeau, Kalou Cabrera Castillos, Jacques Julliand
titre
Coverage Criteria for Model-Based Testing using Property Patterns
article
MBT 2014, 9th Workshop on Model-Based Testing, Satellite workshop of ETAPS 2014, Apr 2014, Grenoble, France. pp.15, ⟨10.4204/EPTCS.141.3⟩
DOI
DOI : 10.4204/EPTCS.141.3
Accès au bibtex
BibTex
auteur
Stephane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Mery
titre
Separation Logic with One Quantified Variable
article
CSR 2014, Jun 2014, Moscou, Russia. ⟨10.1007/978-3-319-06686-8_10⟩
DOI
DOI : 10.1007/978-3-319-06686-8_10
Accès au bibtex
BibTex
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
article
ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf BibTex
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
article
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. pp.1-16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf BibTex
auteur
Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, Peter Ryan
titre
Formal Analysis of Electronic Exams
article
11th International Conference on Security and Cryptography (SECRYPT 2014), Aug 2014, Vienne, Austria. ⟨10.5220/0005050901010112⟩
DOI
DOI : 10.5220/0005050901010112
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01337413/file/secrypt2014.pdf BibTex
auteur
Jannik Dreier, Hugo Jonker, Pascal Lafourcade
titre
Secure Auctions without Cryptography
article
7th International Conference on Fun with Algorithms - FUN 2014, Jul 2014, Lipari, Italy. pp.158-170, ⟨10.1007/978-3-319-07890-8_14⟩
DOI
DOI : 10.1007/978-3-319-07890-8_14
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01337414/file/fun2014.pdf BibTex
auteur
Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, Peter Ryan
titre
Formal Security Analysis of Traditional and Electronic Exams
article
E-Business and Telecommunications - 11th International Joint Conference, ICETE 2014, Revised Selected Papers, Aug 2014, Vienne, Austria. ⟨10.1007/978-3-319-25915-4_16⟩
DOI
DOI : 10.1007/978-3-319-25915-4_16
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01337412/file/icete2014.pdf BibTex
auteur
Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, Peter Ryan
titre
Formal Analysis of Electronic Exams
article
First Symposium on Digital Trust in Auvergne (SDTA'14), Dec 2014, Clermont-Ferrand, France
Accès au bibtex
BibTex
auteur
Serdar Erbatur, Deepak Kapur, Andrew Marshall, Catherine Meadows, Paliath Narendran, Christophe Ringeissen
titre
On Asymmetric Unification and the Combination Problem in Disjoint Theories
article
Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Apr 2014, Grenoble, France. pp.15, ⟨10.1007/978-3-642-54830-7_18⟩
DOI
DOI : 10.1007/978-3-642-54830-7_18
Accès au bibtex
BibTex
auteur
Didier Fass
titre
Reclaiming human machine nature
article
HCI International 2014, Jul 2014, Heraklion, Greece. pp.588-589
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01069481/file/HCII2014-FASS.pdf BibTex
auteur
Elizabeta Fourneret, Jérome Cantenot, Fabrice Bouquet, Bruno Legeard, Julien Botella
titre
SeTGaM: Generalized Technique for Regression Testing Based on UML/OCL Models
article
Software Security and Reliability (SERE), Jun 2014, San Francisco, CA, France. pp.19, ⟨10.1109/SERE.2014.28⟩
DOI
DOI : 10.1109/SERE.2014.28
Accès au bibtex
BibTex
auteur
Simon J. Gay, Nils Gesbert, António Ravara
titre
Session Types as Generic Process Types
article
Proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics (EXPRESS/SOS)., Sep 2014, Rome, Italy. pp.94 - 110, ⟨10.4204/EPTCS.160.9⟩
DOI
DOI : 10.4204/EPTCS.160.9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102349/file/1408.1459v1.pdf BibTex
auteur
Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan
titre
Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials
article
American Control Conference (ACC), Jun 2014, Portland, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633155/file/goubault2014finding.pdf BibTex
auteur
Ahmed Hammad, Fabrice Bouquet, Jean-Marie Gauthier, Dominique Gendreau
titre
Modeling and simulation of modular complex system: Application to air-jet conveyor
article
Advanced Intelligent Mechatronics (AIM), Jul 2014, Besançon, France. pp.6, ⟨10.1109/AIM.2014.6878244⟩
DOI
DOI : 10.1109/AIM.2014.6878244
Accès au bibtex
BibTex
auteur
Mathieu Hoyrup
titre
Irreversible computable functions
article
STACS - 31st Symposium on Theoretical Aspects of Computer Science - 2014, Mar 2014, Lyon, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00915952/file/stacs.pdf BibTex
auteur
Jean-Pierre Jacquot
titre
Premières leçons sur la spécification d'un train d'atterrissage en B événementiel
article
AFADL 2014, CNAM - Cédrics, Jun 2014, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00982982/file/version-HAL.pdf BibTex
auteur
Emmanuel Jeandel
titre
Computability of the entropy of one-tape Turing Machines
article
STACS - Symposium on Theoretical Aspects of Computer Science, Mar 2014, Lyon, France. pp.421-432, ⟨10.4230/LIPIcs.STACS.2014.421⟩
DOI
DOI : 10.4230/LIPIcs.STACS.2014.421
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00785232/file/entropy.pdf BibTex
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
titre
Towards Conflict-Driven Learning for Virtual Substitution
article
Computer Algebra in Scientific Computing - 16th International Workshop, CASC 2014, 2014, Warsaw, Poland. pp.256-270
Accès au bibtex
BibTex
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
titre
Towards Conflict-Driven Learning for Virtual Substitution
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Philipp Rümmer and Christoph M. Wintersteiger, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
titre
Better Answers to Real Questions
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Philipp Rümmer and Christoph M. Wintersteiger, Jul 2014, Vienna, Austria. pp.69
Accès au bibtex
BibTex
auteur
Robbert Krebbers, Xavier Leroy, Freek Wiedijk
titre
Formal C semantics: CompCert and the C standard
article
ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩
DOI
DOI : 10.1007/978-3-319-08970-6_36
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00981212/file/Formal-C-CompCert.pdf BibTex
auteur
Steve Kremer, Robert Künnemann
titre
Automated Analysis of Security Protocols with Global State
article
35th IEEE Symposium on Security and Privacy (S&P'14), May 2014, San Jose, United States. pp.163-178, ⟨10.1109/SP.2014.18⟩
DOI
DOI : 10.1109/SP.2014.18
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091241/file/KK-sp14.pdf BibTex
auteur
Arnaud Lanoix, Olga Kouchnarenko
titre
Component Substitution through Dynamic Reconfigurations
article
11th International Workshop on Formal Engineering approaches to Software Components and Architectures, Satellite event of ETAPS, Apr 2014, Grenoble, France. 14 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00935129/file/submitted_fesca2014_13.pdf BibTex
auteur
Dominique Larchey-Wendling, Didier Galmiche
titre
Looking at Separation Algebras with Boolean BI-eyes
article
8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp. 326-340, ⟨10.1007/978-3-662-44602-7_25⟩
DOI
DOI : 10.1007/978-3-662-44602-7_25
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01256804/file/978-3-662-44602-7_25_Chapter.pdf BibTex
auteur
Fabrice Le Fessant
titre
A Case for Multi-Switch Constraints in OPAM
article
OCaml 2014, Sep 2014, goteborg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091175/file/ocaml2014_12.pdf BibTex
auteur
Xavier Leroy
titre
Formal verification of a static analyzer: abstract interpretation in type theory
article
Types - The 2014 Types Meeting, May 2014, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00983847/file/invited-2.pdf BibTex
auteur
Xavier Leroy
titre
Proof assistants in computer science research
article
IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France
Accès au bibtex
BibTex
auteur
Xavier Leroy
titre
Formal proofs of code generation and verification tools
article
SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩
DOI
DOI : 10.1007/978-3-319-10431-7_1
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01059423/file/abstract.pdf BibTex
auteur
Xavier Leroy
titre
Compiler verification for fun and profit
article
FMCAD 2014 - Formal Methods in Computer-Aided Design, Oct 2014, Lausanne, Switzerland. pp.9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01076547/file/FMCAD14-Leroy.pdf BibTex
auteur
Ghazi Maatoug, Frédéric Dadeau, Michael Rusinowitch
titre
Model-Based Vulnerability Testing of Payment Protocol Implementations
article
HotSpot'14 - 2nd Workshop on Hot Issues in Security Principles and Trust, affiliated with ETAPS 2014, Apr 2014, Grenoble, France
Accès au bibtex
BibTex
auteur
Jean-Yves Marion, Romain Péchoux
titre
Complexity Information Flow in a Multi-threaded Imperative Language
article
TAMC 2014, Apr 2014, Chennai, India. pp.124 - 140, ⟨10.1007/978-3-319-06089-7_9⟩
DOI
DOI : 10.1007/978-3-319-06089-7_9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01084043/file/hulotte.pdf BibTex
auteur
Michel Mauny, Benoît Vaugon
titre
Nullable Type Inference
article
OCaml 2014 - The OCaml Users and Developers Workshop, Sep 2014, Gothenbourg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413294/file/ocaml2014_14.pdf BibTex
auteur
Dominique Méry
titre
Playing with State-Based Models for Designing Better Algorithms
article
Model and Data Engineering - 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. pp.1-3
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Formal Evaluation of Landing Gear System
article
SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
The Semantics of Refinement Chart
article
HCI International, Jun 2014, Heraklion, Greece. pp.415-426, ⟨10.1007/978-3-319-07725-3_42⟩
DOI
DOI : 10.1007/978-3-319-07725-3_42
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Modeling an Aircraft Landing System in Event-B
article
ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. pp.154-159
Accès au bibtex
BibTex
auteur
Stephan Merz, Hernán Vanzetto
titre
Refinement Types for TLA+
article
NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩
DOI
DOI : 10.1007/978-3-319-06200-6_11
Accès au bibtex
BibTex
auteur
Hiep H. Nguyen, Abdessamad Imine, Michael Rusinowitch
titre
A Maximum Variance Approach for Graph Anonymization
article
The 7th International Symposium on Foundations & Practice of Security FPS’2014, Nov 2014, Montreal, Canada
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092442/file/uncertain-graph-fps-final.pdf BibTex
auteur
Hiep H. Nguyen, Abdessamad Imine, Michael Rusinowitch
titre
Enforcing Privacy in Decentralized Mobile Social Networks
article
ESSoS Doctoral Symposium 2014, Feb 2014, Munich, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092447/file/essos-phd.pdf BibTex
auteur
Romain Péchoux, Thanh Dinh Ta
titre
A Categorical Treatment of Malicious Behavioral Obfuscation
article
TAMC 2014, Apr 2014, Chennai, India. pp.280 - 299, ⟨10.1007/978-3-319-06089-7_20⟩
DOI
DOI : 10.1007/978-3-319-06089-7_20
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01084041/file/paper48-Ta-Pechoux.pdf BibTex
auteur
Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
titre
How Test Generation Helps Software Specification and Deductive Verification in Frama-C
article
Tests and Proofs, Jul 2014, York, United Kingdom. pp.204 - 211, ⟨10.1007/978-3-319-09099-3_16⟩
DOI
DOI : 10.1007/978-3-319-09099-3_16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01108553/file/main.pdf BibTex
auteur
François Pottier
titre
Hindley-Milner Elaboration in Applicative Style
article
ICFP 2014: 19th ACM SIGPLAN International Conference on Functional Programming, Sep 2014, Goteborg, Sweden. ⟨10.1145/2628136.2628145⟩
DOI
DOI : 10.1145/2628136.2628145
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081233/file/fpottier-elaboration.pdf BibTex
auteur
Perrine Ruer, Philippe Cabon, Fabrice Vienne
titre
Prevention of wrong way accidents on highways: a human factors approach
article
TRA2014 - Transport Research Arena, Apr 2014, PARIS, France. 8p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01214459/file/doc00020996.pdf BibTex
auteur
Michaël Rusinowitch
titre
Automated Verification of Security Protocols and Services
article
Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation, Tudor Jebelean; Wei Li ; Dongming Wang, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
Deciding unique inhabitants with sums (work in progress)
article
TYPES, May 2014, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094127/file/scherer-types14-extended-abstract.pdf BibTex
auteur
Alexandre Vernotte, Frédéric Dadeau, Franck Lebeau, Bruno Legeard, Fabien Peureux, François Piat
titre
Efficient Detection of Multi-step Cross-Site Scripting Vulnerabilities
article
ICISS'14, 10th Int. Conf. on Information Systems Security, Dec 2014, Hyderabad, India
Accès au bibtex
BibTex
auteur
Daniel Wand
titre
Polymorphic+Typeclass Superposition
article
4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01098078/file/draft.pdf BibTex
auteur
Thomas Williams, Pierre-Évariste Dagand, Didier Rémy
titre
Ornaments in practice
article
WGP 2014: ACM workshop on Generic programming, Aug 2014, Gothenburg, Sweden. ⟨10.1145/2633628.2633631⟩
DOI
DOI : 10.1145/2633628.2633631
Accès au bibtex
BibTex
auteur
Faqing Yang, Jean-Pierre Jacquot, Jeanine Souquières
titre
Proving the Fidelity of Simulations of Event-B Models
article
The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Jan 2014, Miami, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00908066/file/hase2014-final.pdf BibTex

2013

auteur
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
titre
Certification of Bounds of Non-linear Functions: the Templates Method
article
Conferences on Intelligent Computer Mathematics (CICM 2013), Jul 2013, Bath, United Kingdom. pp.51-65, ⟨10.1007/978-3-642-39320-4_4⟩
DOI
DOI : 10.1007/978-3-642-39320-4_4
Accès au bibtex
https://arxiv.org/pdf/1307.3231 BibTex
auteur
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner
titre
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation
article
European Control Conference (ECC'13), Jul 2013, Zurich, Switzerland. pp.2244 - 2250
Accès au bibtex
https://arxiv.org/pdf/1307.7002 BibTex
auteur
Fabrice Ambert, Fabrice Bouquet, Jonathan Lasalle, Bruno Legeard, Fabien Peureux
titre
Applying a Def-Use Approach on Signal Exchange to Implement SysML Model-Based Testing
article
ECMFA'13, 9-th European Conference on Modelling Foundations and Applications, Jul 2013, Montpellier, France. pp.134--151, ⟨10.1007/978-3-642-39013-5_10⟩
DOI
DOI : 10.1007/978-3-642-39013-5_10
Accès au bibtex
BibTex
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
titre
Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms
article
iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland
Accès au bibtex
BibTex
auteur
Myrto Arapinis, Véronique Cortier, Steve Kremer, Mark D. Ryan
titre
Practical Everlasting Privacy
article
2nd Conferences on Principles of Security and Trust (POST'13), Mar 2013, Rome, Italy. pp.21-40, ⟨10.1007/978-3-642-36830-1_2⟩
DOI
DOI : 10.1007/978-3-642-36830-1_2
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00878630/file/ACKR-post13.pdf BibTex
auteur
Carlos Areces, David Déharbe, Pascal Fontaine, Orbe Ezequiel
titre
SyMT: finding symmetries in SMT formulas
article
11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland
Accès au bibtex
BibTex
auteur
Mathilde Arnaud, Véronique Cortier, Cyrille Wiedling
titre
Analysis of an electronic Boardroom Voting System
article
VoteID'13 - 4th International Conference on e-Voting and Identity - 2013, Jul 2013, Guildford, United Kingdom. pp.109-126, ⟨10.1007/978-3-642-39185-9_7⟩
DOI
DOI : 10.1007/978-3-642-39185-9_7
Accès au bibtex
BibTex
auteur
Thibaut Balabonski
titre
Weak Optimality, and the Meaning of Sharing
article
International Conference on Functional Programming (ICFP), Sep 2013, Boston, United States. pp.263-274, ⟨10.1145/2500365.2500606⟩
DOI
DOI : 10.1145/2500365.2500606
Accès au bibtex
BibTex
auteur
Hoang Bao Thien, Abdessamad Imine
titre
On Constrained Adding Friends in Social Networks
article
SocInfo - The 5th International Conference on Social Informatics - 2013, Nov 2013, Kyoto, Japan. pp.467-477, ⟨10.1007/978-3-319-03260-3_40⟩
DOI
DOI : 10.1007/978-3-319-03260-3_40
Accès au bibtex
BibTex
auteur
Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Accès au bibtex
BibTex
auteur
Peter Baumgartner, Uwe Waldmann
titre
Hierarchic Superposition With Weak Abstraction
article
24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. pp.39-57, ⟨10.1007/978-3-642-38574-2_3⟩
DOI
DOI : 10.1007/978-3-642-38574-2_3
Accès au bibtex
BibTex
auteur
Peter Baumgartner, Uwe Waldmann
titre
Hierarchic Superposition: Completeness without Compactness
article
MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12
Accès au bibtex
BibTex
auteur
Walid Belkhir, Yannick Chevalier, Michael Rusinowitch
titre
Fresh-Variable Automata for Service Composition
article
SYNASC 2013 -15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, West University of Timisoara Department of Computer Science, Sep 2013, Timisoara, Romania
Accès au bibtex
https://arxiv.org/pdf/1302.4205 BibTex
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Marek Materzok
titre
Proving termination of evaluation for System F with control operators
article
COS 2013 - First Workshop on Control Operators and their Semantics, Jun 2013, Eindhoven, Netherlands. pp.15-29, ⟨10.4204/EPTCS.127.2⟩
DOI
DOI : 10.4204/EPTCS.127.2
Accès au bibtex
https://arxiv.org/pdf/1309.1261 BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet
titre
Environmental Bisimulations for Delimited-Control Operators
article
APLAS - 11th Asian Symposium on Programming Languages and Systems - 2013, Dec 2013, Melbourne, Australia. pp.333-348
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00903839/file/aplas.pdf BibTex
auteur
Florian Boehl, Véronique Cortier, Bogdan Warinschi
titre
Deduction Soundness: Prove One, Get Five for Free
article
CCS '13 - Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security - 2013, Nov 2013, Berlin, Germany. pp.1261-1272, ⟨10.1145/2508859.2516711⟩
DOI
DOI : 10.1145/2508859.2516711
Accès au bibtex
BibTex
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
article
Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00743090/file/article.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Fabrice Sabatier, Aurélien Thierry
titre
Analysis and Diversion of Duqu's Driver
article
Malware 2013 - 8th International Conference on Malicious and Unwanted Software, Oct 2013, Fajardo, Puerto Rico
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00925517/file/malware2013.pdf BibTex
auteur
Guillaume Bonfante, Bruno Guillaume
titre
Non-simplifying Graph Rewriting Termination
article
TERMGRAPH, Mar 2013, Rome, Italy. pp.4-16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00921053/file/termgraph.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Fabrice Sabatier, Aurélien Thierry
titre
Duqu contre Duqu : Analyse et détournement du driver de Duqu
article
SSTIC - Symposium sur la sécurité des technologies de l'information et des communications, Jun 2013, Rennes, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00925184/file/SSTIC2013-Duqu-contre-Duqu-papier.pdf BibTex
auteur
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
titre
Implementing hash-consed structures in Coq
article
Interactive Theorem Proving, 4th international conference, Jul 2013, Rennes, France. pp.477-483, ⟨10.1007/978-3-642-39634-2_36⟩
DOI
DOI : 10.1007/978-3-642-39634-2_36
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00816672/file/Braibant_Jourdan_Monniaux_ITP2013.pdf BibTex
auteur
Thomas Braibant, Adam Chlipala
titre
Formal Verification of Hardware Synthesis
article
Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. pp.213-228, ⟨10.1007/978-3-642-39799-8_14⟩
DOI
DOI : 10.1007/978-3-642-39799-8_14
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00776876/file/main.pdf BibTex
auteur
Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, Safouan Taha, Bilal Kanso
titre
A Compositional Automata-based Semantics for Property Patterns
article
iFM'2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. pp.316-330, ⟨10.1007/978-3-642-38613-8_22⟩
DOI
DOI : 10.1007/978-3-642-38613-8_22
Accès au bibtex
BibTex
auteur
Christophe Calvès
titre
Unifying Nominal Unification
article
Rewriting Techniques and Applications, Eindhoven University of Technology, Jun 2013, Eindhoven, Netherlands. pp.143-157, ⟨10.4230/LIPIcs.RTA.2013.143⟩
DOI
DOI : 10.4230/LIPIcs.RTA.2013.143
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00926833/file/calves_RTA2013.pdf BibTex
auteur
David Cattanéo, Simon Perdrix
titre
Parameterized Complexity of Weak Odd Domination Problems
article
19th International Symposium on Fundamentals of Computation Theory, Aug 2013, Liverpool, United Kingdom. pp.107-120, ⟨10.1007/978-3-642-40164-0_13⟩
DOI
DOI : 10.1007/978-3-642-40164-0_13
Accès au bibtex
https://arxiv.org/pdf/1206.4081 BibTex
auteur
Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda
titre
Evaluating and benchmarking SPARQL query containment solvers
article
Proc. 12th International semantic web conference (ISWC), Oct 2013, Sydney, Australia. pp.408-423, ⟨10.1007/978-3-642-41338-4_26⟩
DOI
DOI : 10.1007/978-3-642-41338-4_26
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00917911/file/wudagechekol2013a.pdf BibTex
auteur
Vincent Cheval, Véronique Cortier, Antoine Plet
titre
Lengths may break privacy -- or how to check for equivalences with length
article
CAV'13 - 25th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersbourg, Russia. pp.708-723, ⟨10.1007/978-3-642-39799-8_50⟩
DOI
DOI : 10.1007/978-3-642-39799-8_50
Accès au bibtex
BibTex
auteur
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
titre
From security protocols to pushdown automata
article
ICALP'2013 - 40th International Colloquium on Automata, Languages and Programming - 2013, Jul 2013, Riga, Lithuania. pp.137-149, ⟨10.1007/978-3-642-39212-2_15⟩
DOI
DOI : 10.1007/978-3-642-39212-2_15
Accès au bibtex
BibTex
auteur
Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri
titre
Tractable inference systems: an extension with a deducibility predicate
article
CADE'24 - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, United States. pp.91-108, ⟨10.1007/978-3-642-38574-2_6⟩
DOI
DOI : 10.1007/978-3-642-38574-2_6
Accès au bibtex
BibTex
auteur
Véronique Cortier, David Galindo, Stephane Glondu, Malika Izabachène
titre
Distributed ElGamal à la Pedersen - Application to Helios
article
WPES 2013 - Proceedings of the 12th ACM workshop on privacy in the electronic society - 2013, Nov 2013, Berlin, Germany. pp.131-142, ⟨10.1145/2517840.2517852⟩
DOI
DOI : 10.1145/2517840.2517852
Accès au bibtex
BibTex
auteur
Jean-René Courtault, Didier Galmiche, Daniel Méry
titre
An Interactive Prover for Bi-intuitionistic Logic
article
Int. Workshop on the Implementation of Logics, IWIL 2013, 2013, Stellenbosch, South Africa
Accès au bibtex
BibTex
auteur
Jean-René Courtault, Didier Galmiche
titre
A Modal BI Logic for Dynamic Resource Properties
article
Int. Symposium on Logical Foundations of Computer Science, LFCS, 2013, San Diego, CA, United States. pp.134-148
Accès au bibtex
BibTex
auteur
Jean-René Courtault, Didier Galmiche
titre
A Modal Extension of Boolean BI for Resource Transformations
article
Int. Workshop on Logics for Resources, Processes and Programs, LRPP 2013, 2013, Nancy, France
Accès au bibtex
BibTex
auteur
Frédéric Dadeau, Kalou Cabrera Castillos, Yves Ledru, Taha Triki, German Vega, Julien Botella, Safouan Taha
titre
Test Generation and Evaluation from High-Level Properties for Common Criteria Evaluations -- The TASCCC Testing Tool
article
ICST 2013 - IEEE 6th International Conference on Software Testing, Verification and Validation, Yves Le Traon, Mar 2013, Luxembourg, Luxembourg. pp.431-438, ⟨10.1109/ICST.2013.60⟩
DOI
DOI : 10.1109/ICST.2013.60
Accès au bibtex
BibTex
auteur
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
titre
Computing prime implicant
article
FMCAD - Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. pp.46-52
Accès au bibtex
BibTex
auteur
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
titre
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
article
IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909688/file/zenon-modulo-iwil-2013.pdf BibTex
auteur
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
titre
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
article
LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩
DOI
DOI : 10.1007/978-3-642-45221-5_20
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909784/file/Zenon-modulo-lpar-19.pdf BibTex
auteur
Jannik Dreier, Hugo Jonker, Pascal Lafourcade
titre
Defining Verifiability in e-Auction Protocols
article
8th ACM Symposium on Information, Computer and Communications Security (AsiaCCS '13), ACM, May 2013, Hangzhou, China. ⟨10.1145/2484313.2484387⟩
DOI
DOI : 10.1145/2484313.2484387
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01337416/file/asiaccs2013.pdf BibTex
auteur
Jannik Dreier, Hugo Jonker, Pascal Lafourcade
titre
Verifiability in e-Auction Protocols
article
1st Workshop on Hot Issues in Security Principles and Trust (HotSpot'13), Mar 2013, Rome, Italy
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01338057/file/main.pdf BibTex
auteur
Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
titre
On Unique Decomposition of Processes in the Applied π-Calculus
article
16th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2013), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013), Mar 2013, Rome, Italy. ⟨10.1007/978-3-642-37075-5_4⟩
DOI
DOI : 10.1007/978-3-642-37075-5_4
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01338002/file/fossacs2013.pdf BibTex
auteur
Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech
titre
Formal Verification of e-Auction Protocols
article
International Conference on Principles of Security and Trust, POST 2013, Mar 2013, Rome, Italy. ⟨10.1007/978-3-642-36830-1_13⟩
DOI
DOI : 10.1007/978-3-642-36830-1_13
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01338020/file/post2013.pdf BibTex
auteur
Alois Dreyfus, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Random Grammar-based Testing for Covering All Non-Terminals
article
2013 IEEE Sixth International Conference on Software Testing, Verification and Validation - CSTVA Workshop, Mar 2013, Luxembourg, Luxembourg
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909225/file/cstva.pdf BibTex
auteur
Alois Dreyfus, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Enhancing Approximations for Regular Reachability Analysis
article
CIAA 2013 - 18th International Conference on Implementation and Application of Automata - 2013, Jul 2013, Halifax, Canada. pp.331-339, ⟨10.1007/978-3-642-39274-0_29⟩
DOI
DOI : 10.1007/978-3-642-39274-0_29
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909204/file/document.pdf BibTex
auteur
Ivan Enderlin, Alain Giorgetti, Fabrice Bouquet
titre
A Constraint Solver for PHP Arrays
article
ICSTW - Sixth International IEEE Conference on Software Testing, Verification and Validation Workshops - 2013, Mar 2013, Luxembourg, Luxembourg. pp.218-223, ⟨10.1109/ICSTW.2013.80⟩
DOI
DOI : 10.1109/ICSTW.2013.80
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00909202/file/EGB13.pdf BibTex
auteur
Serdar Erbatur, Deepak Kapur, Andrew Marshall, Paliath Narendran, Christophe Ringeissen
titre
Hierarchical Combination of Unification Algorithms
article
The 27th International Workshop on Unification (UNIF 2013), Jun 2013, Eindhoven, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00920509/file/Hierarchical.pdf BibTex
auteur
Serdar Erbatur, Deepak Kapur, Andrew Marshall, Paliath Narendran, Christophe Ringeissen
titre
Hierarchical Combination
article
CADE-24 - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, United States. pp.249-266, ⟨10.1007/978-3-642-38574-2_17⟩
DOI
DOI : 10.1007/978-3-642-38574-2_17
Accès au bibtex
BibTex
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner Seiler, Thomas Sturm, Andreas Weber
titre
Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
article
CASC 2013 - 15th International Workshop on Computer Algebra in Scientific Computing, Sep 2013, Berlin, Germany. pp.88-99, ⟨10.1007/978-3-319-02297-0_7⟩
DOI
DOI : 10.1007/978-3-319-02297-0_7
Accès au bibtex
BibTex
auteur
Didier Fass
titre
Putting in perspective human-machine system theory and modeling: from theoretical biology to artifacts integrative design and organization.
article
4th International Conference - DHM 2013, Held as Part of HCI International 2013, Jul 2013, Las Vegas, United States. pp.316-325, ⟨10.1007/978-3-642-39173-6_37⟩
DOI
DOI : 10.1007/978-3-642-39173-6_37
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00867070/file/FASS_HCII2013.pdf BibTex
auteur
Hugo Férée, Mathieu Hoyrup
titre
Higher-order complexity in analysis
article
CCA - 10th International Conference on Computability and Complexity in Analysis - 2013, Jul 2013, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00915973/file/final.pdf BibTex
auteur
Hugo Férée, Mathieu Hoyrup, Walid Gomaa
titre
On the query complexity of real functionals
article
LICS - 28th ACM/IEEE Symposium on Logic in Computer Science, Jun 2013, New Orleans, United States. pp.103-112, ⟨10.1109/LICS.2013.15⟩
DOI
DOI : 10.1109/LICS.2013.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00773653/file/preprint.pdf BibTex
auteur
David Galindo, Srinivas Vivek
titre
A Leakage-Resilient Pairing-Based Variant of the Schnorr Signature Scheme
article
IMACC 2013 - 14th IMA International Conference Cryptography and Coding, Institute of Mathematics and its Applications, Dec 2013, Oxford, United Kingdom. pp.173-192, ⟨10.1007/978-3-642-45239-0_11⟩
DOI
DOI : 10.1007/978-3-642-45239-0_11
Accès au bibtex
BibTex
auteur
Jacques Garrigue, Didier Rémy
titre
Ambivalent Types for Principal Type Inference with GADTs
article
APLAS 2013 - 11th Asian Symposium on Programming Languages and Systems, 2013, Melbourne, Australia. pp.257-272, ⟨10.1007/978-3-319-03542-0_19⟩
DOI
DOI : 10.1007/978-3-319-03542-0_19
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00914560/file/Garrigue-Remy_gadts_applas2013.pdf BibTex
auteur
Jean-Marie Gauthier, Fabrice Bouquet, Ahmed Hammad, Fabien Peureux
titre
Verification and Validation of Meta-Model Based Transformation from SysML to VHDL-AMS
article
MODELSWARD 2013, 1st Int. Conf. on Model-Driven Engineering and Software Development, Feb 2013, Barcelona, Spain. pp.123--128
Accès au bibtex
BibTex
auteur
Pierre Genevès, Nabil Layaïda
titre
XML Validation: Looking Backward -- Strongly Typed and Flexible XML Processing are not Incompatible
article
22nd International World Wide Web Conference (WWW'13), May 2013, Rio de Janeiro, Brazil
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00837765/file/p219-geneves.pdf BibTex
auteur
Emmanuel Hainry, Jean-Yves Marion, Romain Péchoux
titre
Type-based complexity analysis for fork processes
article
16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Mar 2013, Rome, Italy. pp.305-320, ⟨10.1007/978-3-642-37075-5_20⟩
DOI
DOI : 10.1007/978-3-642-37075-5_20
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00755450/file/fossacs.pdf BibTex
auteur
Emmanuel Hainry, Romain Péchoux
titre
Types for controlling heap and stack in Java
article
Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA), Ugo Dal Lago and Ricardo Pena, Aug 2013, Bertinoro, Italy
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910166/file/ObjectIsBeautiful.pdf BibTex
auteur
Florent Jacquemard, Michael Rusinowitch
titre
Rewrite Closure and CF Hedge Automata
article
7th International Conference on Language and Automata Theory and Application, Apr 2013, Bilbao, Spain
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00767719/file/CFHA.pdf BibTex
auteur
Florent Jacquemard, Michaël Rusinowitch
titre
Unranked Tree Rewriting and Effective Closures of Languages
article
Meeting of the IFIP WG 1.6 on Term Rewriting, Jun 2013, Eindhoven, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00852379/file/abstract.pdf BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Hardness of Conjugacy, Embedding and Factorization of multidimensional Subshifts of Finite Type
article
30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27 - March 2, 2013, Kiel, Germany, Feb 2013, Kiel, Germany. ⟨10.4230/LIPIcs.STACS.2013.490⟩
DOI
DOI : 10.4230/LIPIcs.STACS.2013.490
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00690285/file/conf-arxiv.pdf BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Hardness of Conjugacy, Embedding and Factorization of multidimensional Subshifts of Finite Type
article
STACS - 30th International Symposium on Theoretical Aspects of Computer Science, Christian-Albrechts-Universität zu Kiel, Feb 2013, Kiel, Germany. pp.490--501, ⟨10.4230/LIPIcs.STACS.2013.490⟩
DOI
DOI : 10.4230/LIPIcs.STACS.2013.490
Accès au bibtex
BibTex
auteur
Ralf Karrenberg, Marek Kosta, Thomas Sturm
titre
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
article
9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. pp.56-70, ⟨10.1007/978-3-642-40885-4_5⟩
DOI
DOI : 10.1007/978-3-642-40885-4_5
Accès au bibtex
BibTex
auteur
Chantal Keller
titre
Extended Resolution as Certificates for Propositional Logic
article
PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00836845/file/keller-pxtp13.pdf BibTex
auteur
Marek Kosta
titre
SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
article
Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), 2013, Nanning, China
Accès au bibtex
BibTex
auteur
Olga Kouchnarenko, Jean-Francois Weber
titre
Adapting Component-based Systems at Runtime via Policies with Temporal Patterns
article
10th International Symposium on Formal Aspect of Component Software - FACS 2013, Oct 2013, Nanchang, China
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00940682/file/facs2013_adapting.pdf BibTex
auteur
Steve Kremer, Robert Künnemann, Graham Steel
titre
Universally Composable Key-Management
article
18th European Symposium on Research in Computer Security (ESORICS'13), 2013, Egham, United Kingdom. ⟨10.1007/978-3-642-40203-6_19⟩
DOI
DOI : 10.1007/978-3-642-40203-6_19
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00878632/file/KKS-esorics13.pdf BibTex
auteur
Daniel Leivant, Jean-Yves Marion
titre
Evolving graph-structures and their implicit computational complexity
article
ICALP, Jul 2013, RIGA, Latvia. pp.349-360
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00939484/file/LeivantMarion.pdf BibTex
auteur
Jacques Lemordant, Thibaud Michel, Mathieu Razafinahazo
titre
Mixed Reality Browsers and Pedestrian Navigation in Augmented Cities
article
The Graphical Web Conference, Oct 2013, San Francisco, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00872721/file/MRBAugmentedCity2.pdf BibTex
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
titre
Certifying Network Calculus in a Proof Assistant
article
EUCASS - 5th European Conference for Aeronautics and Space Sciences, Astrium and Technische Universität München, Jul 2013, Munich, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904817/file/submission.pdf BibTex
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
titre
Towards Certifying Network Calculus
article
ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.484-489, ⟨10.1007/978-3-642-39634-2_37⟩
DOI
DOI : 10.1007/978-3-642-39634-2_37
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904796/file/final.pdf BibTex
auteur
Houari Mahfoud, Abdessamad Imine, Michael Rusinowitch
titre
SVMAX: a system for secure and valid manipulation of XML data
article
IDEAS'13 Proceedings of the 17th International Database Engineering & Applications Symposium, Oct 2013, Barcelone, Spain. ⟨10.1145/2513591.2513657⟩
DOI
DOI : 10.1145/2513591.2513657
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Ideal Mode Selection of a Cardiac Pacing System
article
4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. pp.258-267, ⟨10.1007/978-3-642-39173-6_31⟩
DOI
DOI : 10.1007/978-3-642-39173-6_31
Accès au bibtex
BibTex
auteur
Dominique Méry, Monahan Rosemary
titre
Transforming EVENT B Models into Verified C# Implementations
article
VPT 2013 - First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
Accès au bibtex
BibTex
auteur
Dominique Méry, Mike Poppleton
titre
Formal Modelling and Verification of Population Protocols
article
iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland
Accès au bibtex
BibTex
auteur
Romain Péchoux
titre
Bounding Reactions in the Pi-calculus using Interpretations
article
Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA 2013), Ugo Dal Lago and Ricardo Pena, Aug 2013, Bertinoro, Italy
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910170/file/R.pdf BibTex
auteur
François Pottier, Jonathan Protzenko
titre
Programming with permissions in Mezzo
article
ICFP - The 18th ACM SIGPLAN International Conference on Functional Programming - 2013, Sep 2013, Boston, United States. pp.173-184, ⟨10.1145/2500365.2500598⟩
DOI
DOI : 10.1145/2500365.2500598
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00877590/file/pottier-protzenko-mezzo.pdf BibTex
auteur
Aurel Randolph, Abdessamad Imine, Hanifa Boucheneb, Quintero Alejandro
titre
Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors
article
FMICS 2013 - 18th International Workshop on Formal Methods for Industrial Critical Systems, Sep 2013, Madrid, Spain. pp.184-198, ⟨10.1007/978-3-642-41010-9_13⟩
DOI
DOI : 10.1007/978-3-642-41010-9_13
Accès au bibtex
BibTex
auteur
Michael Rusinowitch
titre
Automated verification of security protocols and application to services
article
Verification and Evaluation of Computer and Communication Systems, Alessandro Fantechi, University of Florence, Italy, Nov 2013, Florence, Italy
Accès au bibtex
BibTex
auteur
Gabriel Scherer, Jan Hoffmann
titre
Tracking Data-Flow with Open Closure Types
article
LPAR- 19th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, Dec 2013, Stellenbosch, South Africa. pp.710-726
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00911656/file/closures.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
GADTs meet subtyping
article
ESOP 2013 - 22nd European Symposium on Programming, Mar 2013, Rome, Italy. pp.554-573, ⟨10.1007/978-3-642-37036-6⟩
DOI
DOI : 10.1007/978-3-642-37036-6
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00772993/file/esop.pdf BibTex
auteur
Mohammed Tounsi, Mohammed Mosbah, Dominique Méry
titre
From Event-B Specifications to Programs for Distributed Algorithms
article
WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩
DOI
DOI : 10.1109/WETICE.2013.44
Accès au bibtex
BibTex
auteur
Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, Olga Kouchnarenko
titre
Automatic Decidability for Theories with Counting Operators
article
Automated Deduction: Decidability, Complexity, Tractability (workshop ADDCT), Jun 2013, Lake Placid, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00920496/file/TushkanovaRGK-ADDCT13.pdf BibTex
auteur
Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, Olga Kouchnarenko
titre
Automatic Decidability: A Schematic Calculus for Theories with Counting Operators
article
RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. pp.303-318, ⟨10.4230/LIPIcs.RTA.2013.303⟩
DOI
DOI : 10.4230/LIPIcs.RTA.2013.303
Accès au bibtex
BibTex
auteur
Laurent Vigneron
titre
Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Apr 2013, Nancy, France
Accès au bibtex
BibTex
auteur
Faqing Yang, Jean-Pierre Jacquot
titre
JeB : un environnement de simulation en JavaScript pour B événementiel
article
Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Apr 2013, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00908037/file/yang-afadl2013.pdf BibTex
auteur
Faqing Yang, Jean-Pierre Jacquot, Jeanine Souquières
titre
JeB: Safe Simulation of Event-B Models in JavaScript
article
The 20th Asia-Pacific Software Engineering Conference (APSEC), Dec 2013, Bangkok, Thailand
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00908056/file/apsec2013-final.pdf BibTex

Book sections

2014

auteur
Guillaume Bonfante, Bruno Guillaume, Mathieu Morey, Guy Perrier
titre
Supertagging with Constraints
article
Philippe Blache; Henning Christiansen; Verónica Dahl; Denys Duchier; Jørgen Villadsen. Constraint and Language, Cambridge Scholar Publishing, pp.253-297, 2014
Accès au bibtex
BibTex
auteur
Fabrice Bouquet, Fabien Peureux, Fabrice Ambert
titre
Model-Based Testing for Functional and Security Test Generation
article
Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer International Publishing, pp.33, 2014, LNCS, 978-3-319-10081-4. ⟨10.1007/978-3-319-10082-1_1⟩
DOI
DOI : 10.1007/978-3-319-10082-1_1
Accès au bibtex
BibTex
auteur
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart
titre
The CompCert memory model
article
Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010
Accès au bibtex
BibTex
auteur
Jose Antonio Martin, Fabio Martinelli, Ilaria Matteucci, Ernesto Pimentel, Mathieu Turuani
titre
On the Synthesis of Secure Services Composition
article
Maritta Heisel; Wouter Joosen; Javier Lopez; Fabio Martinelli. Engineering Secure Future Internet Services and Systems, LNCS 8431 (8431), Springer, pp.392, 2014, Lecture Notes in Computer Science, 978-3-319-07451-1. ⟨http://dx.doi.org/10.1007/978-3-319-07452-8_6⟩
Accès au bibtex
BibTex
auteur
Didier Rémy, Julien Cretin
titre
From Amber to Coercion Constraints
article
Martin Abadi; Philippa Gardner; Andrew D. Gordon; Radu Mardare. Essays for the Luca Cardelli Fest, Microsoft Research, 2014, TechReport, ⟨http://research.microsoft.com/pubs/226237/Luca-Cardelli-Fest-MSR-TR-2014-104.pdf⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093216/file/DidierRemyCoercions.pdf BibTex
auteur
Neeraj Kumar Singh, Dominique Méry
titre
Event B (english version)
article
Jean-Louis Boulanger. Formal Methods Applied to Complex Systems, Wiley, 2014, Formal Methods Applied to Complex Systems, 9781119002727. ⟨10.1002/9781119002727.ch10⟩
DOI
DOI : 10.1002/9781119002727.ch10
Accès au bibtex
BibTex

2013

auteur
Nabil Layaïda, Cécile Roisin
titre
Le temps dans les documents -- Langage SMIL
article
Les Techniques de l'Ingénieur. Représentation et traitement des documents numériques, H7228, Les Techniques de l'Ingénieur, 2013, TIB312DUO
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Event B
article
Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7
Accès au bibtex
BibTex

Directions of work or proceedings

2014

auteur
Martin Abadi, Steve Kremer
titre
Principles of Security and Trust
article
Martín Abadi and Steve Kremer. 3rd International Conference on Principles of Security and Trust (POST'14), France. 8414, Springer, 2014, Lecture Notes in Computer Science, 978-3-642-54791-1. ⟨10.1007/978-3-642-54792-8⟩
DOI
DOI : 10.1007/978-3-642-54792-8
Accès au bibtex
BibTex
auteur
Gabriel Ciobanu, Dominique Méry
titre
Theoretical Aspects of Computing – ICTAC 2014
article
Gabriel Ciobanu; Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, Sep 2014, Bucharest, Romania. 8687, Springer, 2014, Lecture Notes in Computer Science, ⟨10.1007%2F978-3-319-10882-7⟩
DOI
DOI : 10.1007%2F978-3-319-10882-7
Accès au bibtex
BibTex
auteur
Stéphane Demri, Deepak Kapur, Christoph Weidenbach
titre
Automated Reasoning – Seventh International Joint Conference (IJCAR 2014)
article
Stéphane Demri; Deepak Kapur; Christoph Weidenbach. 7th International Joint Conference - IJCAR 2014, Jun 2014, Vienna, Austria. 8562, Springer, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-08586-9. ⟨10.1007/978-3-319-08587-6⟩. ⟨http://link.springer.com/book/10.1007%2F978-3-319-08587-6⟩
DOI
DOI : 10.1007/978-3-319-08587-6
Accès au bibtex
BibTex
auteur
Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry
titre
Proceedings 1st Workshop on Formal Integrated Development Environment
article
Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. France. 149, EPTCS, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩
DOI
DOI : 10.4204/EPTCS.149
Accès au bibtex
BibTex
auteur
Didier Galmiche, Stéphane Graham-Lengrand
titre
Special issue on computational logic in honour of Roy Dyckhoff. Journal of Logic and Computation.
article
United Kingdom. Oxford University Press, 2014, ⟨http://dx.doi.org/10.1093/logcom/exu039⟩
Accès au bibtex
BibTex
auteur
Gerald Lüttgen, Stephan Merz
titre
Science of Computer Programming Special Issue: Automated Verification of Critical Systems
article
Netherlands. 96 (3), Elsevier, 2014, Science of Computer Programming
Accès au bibtex
BibTex
auteur
Stephan Merz, Jun Pang
titre
Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014)
article
Stephan Merz; Jun Pang. 16th International Conference on Formal Engineering Methods - ICFEM 2014, Nov 2014, Luxembourg, Luxembourg. 8829, Springer, pp.460, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-11737-9. ⟨10.1007/978-3-319-11737-9⟩
DOI
DOI : 10.1007/978-3-319-11737-9
Accès au bibtex
BibTex

2013

auteur
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
titre
Formal Verification of Distributed Algorithms
article
Bernadette Charron-Bost and Stephan Merz and Andrey Rybalchenko and Josef Widder. 3, Dagstuhl, pp.16, 2013, Dagstuhl Reports, ⟨10.4230/DagRep.3.4.1⟩
DOI
DOI : 10.4230/DagRep.3.4.1
Accès au bibtex
BibTex
auteur
Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
titre
Frontiers of Combining Systems
article
Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. 8152, Springer, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
Accès au bibtex
BibTex
auteur
Didier Galmiche, Dominique Larchey-Wendling
titre
22nd Int. Conference on Automated Reasoning with Analytic Tableaux and Related Methods
article
Didier Galmiche and Dominique Larchey-Wendling Nancy, France. 2013, Lecture Notes in Artificial Intelligence 8123
Accès au bibtex
BibTex

Habilitation à diriger des recherches

2014

auteur
Pierre Genevès
titre
Static Analysis for Data-Centric Web Programming
article
Computer Science [cs]. Université Grenoble Alpes, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01102401/file/index.pdf BibTex

2013

auteur
Nabil Layaïda
titre
Representation and Analyses of Web Content and Processing
article
Web. Université de Grenoble, 2013
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00872752/file/Nabil-Layaida-HDR.pdf BibTex

Master thesis

2014

auteur
Abdullah Abbas
titre
SPARQL Query Rewriting with Paths [Master's Thesis]
article
Web. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01930697/file/Report.pdf BibTex
auteur
Rémi Nazin
titre
Quels fondements épistémologiques pour l’humain machine ?
article
Sciences cognitives. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01107316/file/m%C3%A9moire.pdf BibTex

Other publications

2014

auteur
Olga Kouchnarenko, Jean-Francois Weber
titre
Decentralised Evaluation of Temporal Patterns over Component-based Systems at Runtime
article
2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01044639/file/hal2014_decentralised_v4.pdf BibTex

2013

auteur
Véronique Cortier, David Galindo, Stephane Glondu, Malika Izabachène
titre
A generic construction for voting correctness at minimum cost - Application to Helios
article
2013
Accès au bibtex
BibTex
auteur
Alois Dreyfus, Pierre-Cyrille Heam, Olga Kouchnarenko, Catherine Masson
titre
A Random Testing Approach Using Pushdown Automata
article
2013
Accès au bibtex
BibTex
auteur
Emmanuel Hainry, Romain Péchoux
titre
Type-based heap and stack space analysis in Java
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00773141/file/ObjectIsBeautiful.pdf BibTex

Books

2014

auteur
Didier Galmiche, Stéphane Graham-Lengrand
titre
Special Issue on Computational Logic ( in honor to Roy Dyckhoff) of Journal of Logic and Computation
article
Oxford University Press (OUP), 2014
Accès au bibtex
BibTex

Reports

2014

auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
titre
Analysis of Self-* and P2P Systems using Refinement (Full Report)
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01018162/file/paperv1.pdf BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet
titre
Sound and Complete Bisimilarities for Call-by-Name and Call-by-Value Lambda-mu Calculus
article
[Research Report] RR-8447, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00926100/file/RR-8447.pdf BibTex
auteur
Maxime Bride, Pierre-Cyrille Héam, Isabelle Jacques
titre
Computing Semicommutation Closures: a Machine Learning Approach
article
[Research Report] FEMTO-ST. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087740/file/mainLearning.pdf BibTex
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)
article
[Research Report] RR-8529, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00985135/file/RR-8529.pdf BibTex
auteur
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
titre
Typing messages for free in security protocols: the case of equivalence properties
article
[Research Report] RR-8546, INRIA. 2014, pp.46
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01007580/file/RR-8546.pdf BibTex
auteur
Véronique Cortier, David Galindo, Stephane Glondu, Malika Izabachène
titre
Election Verifiability for Helios under Weaker Trust Assumptions
article
[Research Report] RR-8555, INRIA. 2014, pp.20
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01011294/file/rapport.pdf BibTex
auteur
Julien Cretin, Didier Rémy
titre
System F with Coercion Constraints
article
[Research Report] RR-8456, INRIA. 2014, pp.36
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00934408/file/RR-8456.pdf BibTex
auteur
Jannik Dreier, Hugo Jonker, Pascal Lafourcade
titre
Secure Auctions Without Cryptography (extended version)
article
[Technical Report] ETH Zurich. 2014
DOI
DOI : 10.3929/ethz-a-010127116
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01337415/file/eth-8490-01.pdf BibTex
auteur
Ivan Enderlin, Fabrice Bouquet, Frédéric Dadeau, Alain Giorgetti
titre
Praspel: Contract-Driven Testing for PHP using Realistic Domains
article
[Research Report] RR-8592, INRIA. 2014, pp.39
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01061900/file/RR-8592.pdf BibTex
auteur
Serdar Erbatur, Deepak Kapur, Andrew Marshall, Catherine Meadows, Paliath Narendran, Christophe Ringeissen
titre
Asymmetric Unification and the Combination Problem in Disjoint Theories
article
[Research Report] RR-8476, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00947088/file/RR-8476.pdf BibTex
auteur
Pierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko
titre
The Emptiness Problem for Tree Automata with at Least One Disequality Constraint is NP-hard
article
[Research Report] FEMTO-ST. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01089711/file/tagednk.pdf BibTex
auteur
Sorina Ionica, Malika Izabachène
titre
Weak instances on composite order protocols
article
[Research Report] INRIA. 2014, pp.1--13
Accès au bibtex
BibTex
auteur
Steve Kremer, Robert Künnemann
titre
Automated analysis of security protocols with global state
article
[Research Report] arXiv. 2014, pp.56
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00955869/file/translation.pdf BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Modelling an Aircraft Landing System in Event-B (Full Report)
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00971787/file/full.pdf BibTex
auteur
Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
titre
StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00992159/file/PKGJ14rr.pdf BibTex
auteur
Denis Roegel
titre
The "Villarceau circles" in Uhlberger's staircase (ca. 1580)
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00941465/file/roegel2014staircase-ond.pdf BibTex
auteur
Denis Roegel
titre
Easter-based walks on a sphere
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01009458/file/roegel2014easter-walks.pdf BibTex
auteur
Denis Roegel
titre
Easter bracelets for 5700000 years
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01009457/file/roegel2014easter-bracelets.pdf BibTex
auteur
Denis Roegel
titre
The strange beauty of the twilight flower
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00978237/file/roegel2014twilight-flower.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Arnaudeau’s table of triangular numbers (ca. 1896)
article
[Research Report] LORIA - Université de Lorraine. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01098344/file/arnaudeau1896doc.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
Full reduction in the face of absurdity
article
[Research Report] INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093910/file/Scherer-Remy%21fich%40rr2014.pdf BibTex

2013

auteur
Umut Acar, Arthur Charguéraud, Stefan Muller, Mike Rainey
titre
Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910130/file/main.pdf BibTex
auteur
Philippe Beaucamps, Isabelle Gnaedig, Jean-Yves Marion
titre
Behavior Analysis of Malicious Code by Weighted Behavior Abstraction
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00803412/file/pondere-hal.pdf BibTex
auteur
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
titre
From security protocols to pushdown automata
article
[Research Report] RR-8290, INRIA. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00817230/file/RR-8290.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Plassmann's table of quarter-squares (1933)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880838/file/plassmann1933doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Ulbrich's table of factors (1791-1800)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880839/file/ulbrich1800doc1.pdf https://hal.inria.fr/hal-00880839/file/ulbrich1800doc2.pdf https://hal.inria.fr/hal-00880839/file/ulbrich1800doc3.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Lifchitz's table of primes (1971)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880841/file/lifchitz1971doc2.pdf https://hal.inria.fr/hal-00880841/file/lifchitz1971doc1.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Joncourt's table of triangular numbers (1762)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880843/file/joncourt1762doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Bojko's table of quarter-squares (1909)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880837/file/bojko1909doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Centnerschwer's table of quarter-squares (1825)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880833/file/centnerschwer1825doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Goldberg's table of factors (1862)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880840/file/goldberg1862doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Magini's Tabula tetragonica (1592)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880844/file/magini1592doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Ludolfs's Tetragonometria tabularia (1690)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880845/file/ludolf1690doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Schiereck's table of squares (1827)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880846/file/schiereck1827doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Bürger's table of quarter-squares (1817)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880832/file/buerger1817doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Laundy's table of quarter-squares (1856)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880835/file/laundy1856doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Herwart's table of multiplication (1610)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880842/file/herwart1610doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Shortrede's traverse tables (1864)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880847/file/shortrede1864doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Voisin's table of quarter-squares (1817)
article
[Research Report] 2013, pp.133
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00812834/file/voisin1817doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Kulik's table of multiplication (1851)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654436/file/kulik1851doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Merpaut's table of quarter-squares (1832)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880834/file/merpaut1832doc.pdf BibTex
auteur
Denis Roegel
titre
A reconstruction of Blater's table of quarter-squares (1887)
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880836/file/blater1887doc.pdf BibTex
auteur
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie de Quatrebarbes, Stéphane Laurent
titre
Médiation Scientifique : une facette de nos métiers de la recherche
article
[Interne] none. 2013, pp.34
Accès au bibtex
BibTex
auteur
Gabriel Scherer, Jan Hoffmann
titre
Tracking Data-Flow with Open Closure Types
article
[Research Report] RR-8345, INRIA. 2013, pp.24
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00851658/file/RR-8345.pdf BibTex

Theses

2014

auteur
Jean-Christophe Bach
titre
Un îlot formel pour les transformations de modèles qualifiables
article
Langage de programmation [cs.PL]. Université de Lorraine, 2014. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01081055/file/JCBach-these.pdf BibTex
auteur
Çağdaş Bozman
titre
Profilage mémoire d’applications OCaml
article
Informatique [cs]. ENSTA ParisTech, 2014. Français
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-01122262/file/thesis-cagdas-bozman.pdf BibTex
auteur
Julien Cretin
titre
Erasable coercions: a unified approach to type systems
article
Programming Languages [cs.PL]. Université Paris-Diderot - Paris VII, 2014. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00940511/file/manuscript-final.pdf BibTex
auteur
Aloïs Dreyfus
titre
Contributions à la vérification et à la validation efficaces fondées sur des modèles
article
Systèmes et contrôle [cs.SY]. Université de Franche-Comté, 2014. Français. ⟨NNT : 2014BESA2076⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01090759/file/these_A_DREYFUS_Alois_2014.pdf BibTex
auteur
Hugo Férée
titre
Complexité d'ordre supérieur et analyse récursive
article
Complexité [cs.CC]. Université de Lorraine, 2014. Français. ⟨NNT : 2014LORR0173⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01751160/file/manuscrit_hferee.pdf BibTex
auteur
Houari Mahfoud
titre
Efficient Access Control to XML Data: Querying and Updating Problems
article
Distributed, Parallel, and Cluster Computing [cs.DC]. Université de Lorraine, 2014. English. ⟨NNT : 2014LORR0011⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01750706/file/ThesisFinalVersion.pdf BibTex
auteur
Jonathan Protzenko
titre
Mezzo: a typed language for safe effectful concurrent programs
article
Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01086106/file/snapshot-0909.pdf BibTex
auteur
Hernán Vanzetto
titre
Proof automation and type synthesis for set theory in the context of TLA+
article
Computer Science [cs]. Université de Lorraine, 2014. English. ⟨NNT : 2014LORR0208⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01751181/file/thesis.pdf BibTex
auteur
Cyrille Wiedling
titre
Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs
article
Cryptography and Security [cs.CR]. Université de Lorraine, 2014. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01107718/file/these_main.pdf BibTex

2013

auteur
Kalou Cabrera Castillos
titre
Génération automatique de scénarios de tests à partir de propriétés temporelles et de modèles comportementaux
article
Génie logiciel [cs.SE]. Université de Franche-Comté, 2013. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00924485/file/These.pdf BibTex
auteur
Joan Calvet
titre
Analyse Dynamique de Logiciels Malveillants
article
Cryptographie et sécurité [cs.CR]. Université de Lorraine, 2013. Français. ⟨NNT : 2013LORR0083⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01750369/file/Document_UDL.pdf BibTex
auteur
Jérome Cantenot
titre
Stratégies de génération de tests à partir de modèles UML/OCL interprétés en logique du premier ordre et système de contraintes
article
Génie logiciel [cs.SE]. Université de Franche-Comté, 2013. Français
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01094360/file/master.pdf BibTex
auteur
Chantal Keller
titre
A Matter of Trust: Skeptical Communication Between Coq and External Provers
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00838322/file/thesis-keller.pdf BibTex
auteur
Elena Tushkanova
titre
Schematic calculi for the analysis of decision procedures
article
Other [cs.OH]. Université de Franche-Comté, 2013. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00910929/file/Manuscrit_These_Tushkanova.pdf BibTex
auteur
Faqing Yang
titre
A Simulation Framework for the Validation of Event-B Specifications
article
Formal Languages and Automata Theory [cs.FL]. Université de Lorraine, 2013. English. ⟨NNT : 2013LORR0158⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01750224/file/DDOC_T_2013_0158_YANG.pdf BibTex

Preprints, Working Papers, ...

2014

auteur
Marti Bosch, Pierre Genevès, Nabil Layaïda
titre
Automated Refactoring for Size Reduction of CSS Style Sheets
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01021332/file/report.pdf BibTex
auteur
Vincent Demange
titre
Pedagogical lambda-cube: the λ² case
article
2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00958835/file/index.pdf BibTex
auteur
Pierre Guillon, Emmanuel Jeandel
titre
Infinite Communication Complexity
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01108690/file/comm.pdf BibTex
auteur
Pierre-Cyrille Héam, Jean-Luc Joly
titre
On the Uniform Random Generation of Determinisitic Partially Ordered Automata using Monte Carlo Techniques
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087751/file/mainAutoPo.pdf BibTex
auteur
Denis Roegel
titre
The (re)discovery of one of the oldest modular digital mechanical counters (1844)
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096151/file/roegel2014counter.pdf BibTex
auteur
Denis Roegel
titre
The (re)discovery of an early specialized mechanical calculating machine (ca. 1850)
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096153/file/roegel2014series.pdf BibTex
auteur
Denis Roegel
titre
The (re)discovery of some of the oldest key-driven adding machines (1844)
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096468/file/roegel2014adding-machine.pdf BibTex
auteur
Gabriel Scherer
titre
2-or-more approximation for intuitionistic logic
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094120/file/2-or-more-approximation.pdf BibTex

2013

auteur
Alexis Ballier, Emmanuel Jeandel
titre
Structuring multi-dimensional subshifts
article
2013
Accès au bibtex
https://arxiv.org/pdf/1309.6289 BibTex
auteur
Walid Belkhir, Yannick Chevalier, Michael Rusinowitch
titre
Guarded Variable Automata over Infinite Alphabets
article
2013
Accès au bibtex
https://arxiv.org/pdf/1304.6297 BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet
titre
Environmental Bisimulations for Delimited-Control Operators
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862189/file/aplasLong.pdf BibTex
auteur
Jacques Garrigue, Didier Rémy
titre
Ambivalent Types for Principal Type Inference with GADTs (extended version)
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00914493/file/Garrigue-Remy_gadts_long2013.pdf BibTex
auteur
Armaël Guéneau, François Pottier, Jonathan Protzenko
titre
The ins and outs of iteration in Mezzo
article
2013
Accès au bibtex
https://arxiv.org/pdf/1311.7256 BibTex
auteur
Jonathan Protzenko
titre
Illustrating the Mezzo programming language
article
2013
Accès au bibtex
https://arxiv.org/pdf/1311.6929 BibTex