Journal articles

2019

auteur
Alexander Bentkamp, Jasmin Blanchette, Dietrich Klakow
titre
A Formal Proof of the Expressiveness of Deep Learning
article
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
DOI
DOI : 10.1007/s10817-018-9481-5
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02296014/file/paper.pdf BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
titre
Proving Soundness of Extensional Normal-Form Bisimilarities
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, ⟨10.23638/LMCS-15(1:31)2019⟩
DOI
DOI : 10.23638/LMCS-15(1:31)2019
Accès au bibtex
https://arxiv.org/pdf/1711.00113 BibTex
auteur
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
titre
Bisimulations for Delimited-Control Operators
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, ⟨10.23638/LMCS-15(2:18)2019⟩
DOI
DOI : 10.23638/LMCS-15(2:18)2019
Accès au bibtex
https://arxiv.org/pdf/1804.08373 BibTex
auteur
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
titre
Bindings as Bounded Natural Functors
article
Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), pp.1-34. ⟨10.1145/3290335⟩
DOI
DOI : 10.1145/3290335
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01989726/file/bindings.pdf BibTex
auteur
Angela Bonifati, Ugo Comignani, Emmanuel Coquery, Romuald Thion
titre
Interactive Mapping Specification with Exemplar Tuples
article
ACM Transactions on Database Systems, Association for Computing Machinery, In press
Accès au bibtex
BibTex
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
titre
Politeness and Combination Methods for Theories with Bridging Functions
article
Journal of Automated Reasoning, Springer Verlag, In press
Accès au bibtex
BibTex
auteur
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat
titre
Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques
article
Journal of Symbolic Computation, Elsevier, 2019, 90, pp.3-41. ⟨10.1016/j.jsc.2018.04.002⟩
DOI
DOI : 10.1016/j.jsc.2018.04.002
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01590654/file/paper.pdf BibTex
auteur
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
titre
TLA+ Model Checking Made Symbolic
article
Proc. ACM Program. Lang. 3, OOPSLA, Article, In press, 3, ⟨10.1145/3360549⟩
DOI
DOI : 10.1145/3360549
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02280888/file/camera.pdf BibTex

2018

auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
titre
A Machine-Checked Correctness Proof for Pastry
article
Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩
DOI
DOI : 10.1016/j.scico.2017.08.003
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01768758/file/paper.pdf BibTex
auteur
Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas
titre
Opacity for linear constraint Markov chains
article
Discrete Event Dynamic Systems, Springer Verlag, 2018, 28 (1), pp.83-108. ⟨10.1007/s10626-017-0259-4⟩
DOI
DOI : 10.1007/s10626-017-0259-4
Accès au bibtex
BibTex
auteur
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
article
Journal of Automated Reasoning, Springer Verlag, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩
DOI
DOI : 10.1007/s10817-018-9455-7
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01904579/file/sat_article.pdf BibTex
auteur
Angela Bonifati, Stefania Dumbrava
titre
Graph Queries: From Theory to Practice
article
SIGMOD record, ACM, 2018, 47 (4)
Accès au bibtex
BibTex
auteur
Melisachew Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda
titre
SPARQL Query Containment under Schema
article
Journal on Data Semantics, Springer, 2018, 7 (3), pp.133-154. ⟨10.1007/s13740-018-0087-1⟩
DOI
DOI : 10.1007/s13740-018-0087-1
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01767887/file/jods18.pdf BibTex
auteur
Joel dos Santos, Débora Muchaluat-Saade, Cécile Roisin, Nabil Layaïda
titre
A Hybrid Approach for Spatio-Temporal Validation of Declarative Multimedia Documents
article
ACM Transactions on Multimedia Computing, Communications and Applications, Association for Computing Machinery, 2018, 14 (4), pp.1-24. ⟨10.1145/3267127⟩
DOI
DOI : 10.1145/3267127
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01946641/file/2018-10-ACM-TOMMa86-santos.pdf BibTex
auteur
Pierre Genevès, Thomas Calmant, Nabil Layaïda, Marion Lepelley, Svetlana Artemova, Jean-Luc Bosson
titre
Scalable Machine Learning for Predicting At-Risk Profiles Upon Hospital Admission
article
Big Data Research, Elsevier, 2018, 12, pp.23-34. ⟨10.1016/j.bdr.2018.02.004⟩
DOI
DOI : 10.1016/j.bdr.2018.02.004
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01517087/file/predictive.pdf BibTex
auteur
Wei Lin, Philippe Rossi, Michel Faure, Xian-Hua Li, Wenbin Ji, Yang Chu
titre
Detrital zircon age patterns from turbidites of the Balagne and Piedmont nappes of Alpine Corsica (France): Evidence for a European margin source
article
Tectonophysics, Elsevier, 2018, 722, pp.69-105. ⟨10.1016/j.tecto.2017.09.015⟩
DOI
DOI : 10.1016/j.tecto.2017.09.015
Accès au texte intégral et bibtex
https://hal-insu.archives-ouvertes.fr/insu-01592867/file/WeiLin-Tectonophysics-2017.pdf BibTex
auteur
Stephan Merz, Hernán Vanzetto
titre
Encoding TLA+ into unsorted and many-sorted first-order logic
article
Science of Computer Programming, Elsevier, 2018, 158, pp.3-20. ⟨10.1016/j.scico.2017.09.004⟩
DOI
DOI : 10.1016/j.scico.2017.09.004
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01768750/file/tla2smt2_v3.pdf BibTex
auteur
Thibaud Michel, Pierre Genevès, Hassen Fourati, Nabil Layaïda
titre
Attitude Estimation for Indoor Navigation and Augmented Reality with Smartphones
article
Pervasive and Mobile Computing, Elsevier, 2018, 46, pp.96-121. ⟨10.1016/j.pmcj.2018.03.004⟩
DOI
DOI : 10.1016/j.pmcj.2018.03.004
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01650142/file/main.pdf BibTex
auteur
Margarida Romero, Marie Duflot-Kremer, Thierry Viéville
titre
Le jeu du robot : analyse d’une activité d’informatique débranchée sous la perspective de la cognition incarnée
article
Review of science, mathematics and ICT education, Laboratory of Didactics of Sciences, Mathematics and ICT, Department of Educational Sciences and Early Childhood Education - University of Patras., A paraître
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01950335/file/RESMICTE-JeuDuRobot-R08.2-final.pdf BibTex
auteur
Pierre Senellart, Louis Jachiet, Silviu Maniu, Yann Ramusat
titre
ProvSQL: Provenance and Probability Management in PostgreSQL
article
Proceedings of the VLDB Endowment (PVLDB), VLDB Endowment, 2018, 11 (12), pp.2034-2037. ⟨10.14778/3229863.3236253⟩
DOI
DOI : 10.14778/3229863.3236253
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01851538/file/p976-senellart.pdf BibTex
auteur
Thomas Williams, Didier Rémy
titre
A Principled Approach to Ornamentation in ML
article
Proceedings of the ACM on Programming Languages, ACM, 2018, pp.1-30. ⟨10.1145/3158109⟩
DOI
DOI : 10.1145/3158109
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01666104/file/ornaments-popl18-final.pdf BibTex

2017

auteur
Samson Abramsky, Rui Soares Barbosa, Giovanni Carù, Simon Perdrix
titre
A complete characterisation of All-versus-Nothing arguments for stabiliser states
article
Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, Royal Society, The, 2017, Second quantum revolution: foundational questions, 375 (2106), ⟨10.1098/rsta.2016.0385⟩
DOI
DOI : 10.1098/rsta.2016.0385
Accès au bibtex
https://arxiv.org/pdf/1705.08459 BibTex
auteur
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
titre
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (3), ⟨10.23638/LMCS-13(3:27)2017⟩
DOI
DOI : 10.23638/LMCS-13(3:27)2017
Accès au bibtex
https://arxiv.org/pdf/1611.09626v5 BibTex
auteur
Laurent Bienvenu, Mathieu Hoyrup, Alexander Shen
titre
Layerwise Computability and Image Randomness
article
Theory of Computing Systems, Springer Verlag, 2017, 61 (4), pp.1353-1375. ⟨10.1007/s00224-017-9791-8⟩
DOI
DOI : 10.1007/s00224-017-9791-8
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01650910/file/1607.04232.pdf BibTex
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
titre
Soundness and Completeness Proofs by Coinductive Methods
article
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. ⟨10.1007/s10817-016-9391-3⟩
DOI
DOI : 10.1007/s10817-016-9391-3
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643157/file/compl.pdf BibTex
auteur
Martin Bromberger, Christoph Weidenbach
titre
New Techniques for Linear Arithmetic: Cubes and Equalities
article
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.433-461. ⟨10.1007/s10703-017-0278-7⟩
DOI
DOI : 10.1007/s10703-017-0278-7
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656397/file/paper.pdf BibTex
auteur
Arthur Charguéraud, François Pottier
titre
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
article
Journal of Automated Reasoning, Springer Verlag, 2017, ⟨10.1007/s10817-017-9431-7⟩
DOI
DOI : 10.1007/s10817-017-9431-7
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652785/file/credits_jar.pdf BibTex
auteur
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
titre
Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (4), pp.1-54. ⟨10.23638/LMCS-13(4:16)2017⟩
DOI
DOI : 10.23638/LMCS-13(4:16)2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01479030/file/1705.08632v2.pdf BibTex
auteur
Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
titre
NP-completeness of small conflict set generation for congruence closure
article
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.533 - 544. ⟨10.1007/s10703-017-0283-x⟩
DOI
DOI : 10.1007/s10703-017-0283-x
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01908684/file/SMT.pdf BibTex
auteur
Mathieu Hoyrup, Cristóbal Rojas
titre
On the Information Carried by Programs About the Objects they Compute
article
Theory of Computing Systems, Springer Verlag, 2017, ⟨10.1007/s00224-016-9726-9⟩
DOI
DOI : 10.1007/s00224-016-9726-9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413066/file/revision.pdf BibTex
auteur
Mathieu Hoyrup
titre
Genericity of weakly computable objects
article
Theory of Computing Systems, Springer Verlag, 2017, Special Issue: Theoretical Aspects of Computer Science, 60 (3), ⟨10.1007/s00224-016-9737-6⟩
DOI
DOI : 10.1007/s00224-016-9737-6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01095864/file/revision.pdf BibTex
auteur
Jacques-Henri Jourdan, François Pottier
titre
A Simple, Possibly Correct LR Parser for C11
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2017, 39 (4), pp.1 - 36. ⟨10.1145/3064848⟩
DOI
DOI : 10.1145/3064848
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633123/file/jourdan2017simple.pdf BibTex
auteur
Atif Mashkoor, Jean-Pierre Jacquot
titre
Validation of Formal Specifications through Transformation and Animation
article
Requirements Engineering, Springer Verlag, 2017, 22 (4), pp.433-451. ⟨10.1007/s00766-016-0246-6⟩
DOI
DOI : 10.1007/s00766-016-0246-6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01262115/file/main.pdf BibTex
auteur
Dominique Méry
titre
Playing with State-Based Models for Designing Better Algorithms
article
Future Generation Computer Systems, Elsevier, 2017, 68, pp.445-455. ⟨10.1016/j.future.2016.04.019⟩
DOI
DOI : 10.1016/j.future.2016.04.019
Accès au bibtex
BibTex
auteur
Dominique Méry, Mike Poppleton
titre
Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
article
Software and Systems Modeling, Springer Verlag, 2017, 16 (4), pp.1083--1115
Accès au bibtex
BibTex
auteur
François Pottier
titre
Visitors unchained
article
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.1 - 28. ⟨10.1145/3110272⟩
DOI
DOI : 10.1145/3110272
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670735/file/fpottier-visitors-unchained.pdf BibTex
auteur
Denis Roegel
titre
Carries Stripped to the Bone: Episodes in the History of Coaxial Modular Digital Counters
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2017, 39 (3), pp.55-64
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Before Torchi and Schwilgué, there was White
article
ComputingEdge, IEEE Computer Society, 2017, pp.42-43. ⟨https://www.computer.org/web/computingedge⟩
Accès au bibtex
BibTex
auteur
Thomas Sturm
titre
A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
article
Mathematics in Computer Science, Springer, 2017, 11 (3-4), pp.483 - 502. ⟨10.1007/s11786-017-0319-z⟩
DOI
DOI : 10.1007/s11786-017-0319-z
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01648690/file/10.1007_s11786-017-0319-z.pdf BibTex

2016

auteur
Umut Acar, Arthur Charguéraud, Mike Rainey
titre
Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages
article
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, ⟨10.1017/S0956796816000101⟩
DOI
DOI : 10.1017/S0956796816000101
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409069/file/granularity_jfp16.pdf BibTex
auteur
Yamine Ait Ameur, Dominique Méry
titre
Making explicit domain knowledge in formal system development
article
Science of Computer Programming, Elsevier, 2016, 121 (100--127), ⟨10.1016/j.scico.2015.12.004⟩
DOI
DOI : 10.1016/j.scico.2015.12.004
Accès au bibtex
BibTex
auteur
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng Bono, Luca Padovani, Vasco Vasconcelos, Nobuko Yoshida
titre
Behavioral Types in Programming Languages
article
Foundations and Trends in Programming Languages, Now Publishers, 2016, 3 (2-3), pp.95-230. ⟨10.1561/2500000031⟩
DOI
DOI : 10.1561/2500000031
Accès au bibtex
BibTex
auteur
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco Vasconcelos, Nobuko Yoshida
titre
Behavioral Types in Programming Languages
article
Foundations and Trends in Programming Languages, Now Publishers, 2016, 3 (2-3), pp.95-230. ⟨10.1561/2500000031⟩
DOI
DOI : 10.1561/2500000031
Accès au bibtex
BibTex
auteur
Thibaut Balabonski, François Pottier, Jonathan Protzenko
titre
The Design and Formalization of Mezzo, a Permission-Based Programming Language
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
DOI
DOI : 10.1145/2837022
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246534/file/bpp-mezzo-journal.pdf BibTex
auteur
Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, Josef Urban
titre
Hammering towards QED
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (1), pp.101-148
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386988/file/h4qed-clean.pdf BibTex
auteur
Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
titre
A Learning-Based Fact Selector for Isabelle/HOL
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. ⟨10.1007/s10817-016-9362-8⟩
DOI
DOI : 10.1007/s10817-016-9362-8
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386986/file/paper.pdf BibTex
auteur
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
titre
Semi-intelligible Isar Proofs from Machine-Generated Proofs
article
Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩
DOI
DOI : 10.1007/s10817-015-9335-3
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01211748/file/paper.pdf BibTex
auteur
Guillaume Bonfante, Reinhard Kahle, Jean-Yves Marion, Isabel Oitavem
titre
Two function algebras defining functions in NC k boolean circuits
article
Journal of Information and Computation, Elsevier, 2016, ⟨10.1016/j.ic.2015.12.009⟩
DOI
DOI : 10.1016/j.ic.2015.12.009
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01113342/file/nc.pdf BibTex
auteur
Özgür Dagdelen, David Galindo, Pascal Véron, Sidi Mohamed El Yousfi Alaoui, Pierre-Louis Cayrel
titre
Extended security arguments for signature schemes
article
Designs, Codes and Cryptography, Springer Verlag, 2016, 78 (2), pp.441-461. ⟨10.1007/s10623-014-0009-7⟩
DOI
DOI : 10.1007/s10623-014-0009-7
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01313619/file/main.pdf BibTex
auteur
Stephane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Mery
titre
Separation Logic with One Quantified Variable
article
Theory of Computing Systems, Springer Verlag, 2016
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01258821/file/ToCS_SI_CSR14_demri_galmiche_larchey_mery.pdf BibTex
auteur
Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
titre
On the existence and decidability of unique decompositions of processes in the applied π-calculus
article
Theoretical Computer Science, Elsevier, 2016, 612, pp.102--125. ⟨10.1016/j.tcs.2015.11.033⟩
DOI
DOI : 10.1016/j.tcs.2015.11.033
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01238097/file/main.pdf BibTex
auteur
Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
titre
Testing Noninterference, Quickly
article
Journal of Functional Programming (JFP); Special issue for ICFP 2013, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
DOI
DOI : 10.1017/S0956796816000058
Accès au bibtex
https://arxiv.org/pdf/1409.0393 BibTex
auteur
Jean-Pierre Jacquot
titre
Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel
article
Technique et Science Informatiques, Hermès-Lavoisier, 2016, pp.25. ⟨10.3166/TSI.34.547-571⟩
DOI
DOI : 10.3166/TSI.34.547-571
Accès au bibtex
BibTex
auteur
G Kirstetter, J Hu, O Delestre, F Darboux, P-Y Lagrée, S Popinet, J.-M. Fullana, C Josserand
titre
Modeling rain-driven overland flow: Empirical versus analytical friction terms in the shallow water approximation
article
Journal of Hydrology, Elsevier, 2016, 536, pp.1 - 9. ⟨10.1016/j.jhydrol.2016.02.022⟩
DOI
DOI : 10.1016/j.jhydrol.2016.02.022
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01398120/file/ManuscriptFinal.pdf BibTex
auteur
Marek Košta, Thomas Sturm, Andreas Dolzmann
titre
Better answers to real questions
article
Journal of Symbolic Computation, Elsevier, 2016, 74, pp.255 - 275. ⟨10.1016/j.jsc.2015.07.002⟩
DOI
DOI : 10.1016/j.jsc.2015.07.002
Accès au bibtex
BibTex
auteur
Atif Mashkoor, Faqing Yang, Jean-Pierre Jacquot
titre
Refinement-based Validation of Event-B Specifications
article
Software and Systems Modeling, Springer Verlag, 2016, pp.33. ⟨10.1007/s10270-016-0514-4⟩
DOI
DOI : 10.1007/s10270-016-0514-4
Accès au bibtex
BibTex
auteur
Stephan Merz, Jun Pang
titre
Editorial
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. ⟨10.1007/s00165-016-0378-y⟩
DOI
DOI : 10.1007/s00165-016-0378-y
Accès au bibtex
BibTex
auteur
Stephan Merz, Jun Pang
titre
Editorial
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. ⟨10.1007/s00165-016-0390-2⟩
DOI
DOI : 10.1007/s00165-016-0390-2
Accès au bibtex
BibTex
auteur
Marie-Karelle Riviere, Jacques-Henri Jourdan, Sarah Zohar
titre
dfcomb: An R-package for phase I/II trials of drug combinations
article
Computer Methods and Programs in Biomedicine, Elsevier, 2016, 125, pp.117-133. ⟨10.1016/j.cmpb.2015.10.018⟩
DOI
DOI : 10.1016/j.cmpb.2015.10.018
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01297367/file/packages_CMPB.pdf BibTex
auteur
Marie-Karelle Riviere, Ying Yuan, Jacques-Henri Jourdan, Frédéric Dubois, Sarah Zohar
titre
Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization
article
Statistical Methods in Medical Research, SAGE Publications, 2016, ⟨10.1177/0962280216631763⟩
DOI
DOI : 10.1177/0962280216631763
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01298681/file/Riviere_2016_Phase_I-II.pdf BibTex
auteur
Denis Roegel
titre
A mechanical calculator for arithmetic sequences (1844-1852): part 2, working details
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2016, 38 (1), pp.80-88. ⟨10.1109/MAHC.2016.3 ⟩
DOI
DOI : 10.1109/MAHC.2016.3
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Before Torchi and Schwilgué, there was White
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2016, 38 (4), pp.92-93. ⟨10.1109/MAHC.2016.46⟩
DOI
DOI : 10.1109/MAHC.2016.46
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
A new early adding machine by Schwilgué (c. 1840?)
article
Bulletin of the Scientific Instrument Society, Scientific Instrument Society, 2016, 130, pp.24-27
Accès au bibtex
BibTex
auteur
Thomas Sturm, Erika Abraham, John Abbott, Bern W. Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler
titre
Satisfiability Checking and Symbolic Computation
article
ACM Communications in Computer Algebra, Association for Computing Machinery (ACM), 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
DOI
DOI : 10.1145/3055282.3055285
Accès au bibtex
BibTex

2015

auteur
Pablo Arrighi, Simon Perdrix
titre
L’ordinateur quantique pour simuler... la physique quantique
article
La Recherche : l'actualité des sciences, société d'éditions scientifiques, 2015
Accès au bibtex
BibTex
auteur
Paolo Ballarini, Marie Duflot
titre
Applications of an expressive statistical model checking approach to the analysis of genetic circuits
article
Theoretical Computer Science, Elsevier, 2015, 599, pp.30. ⟨10.1016/j.tcs.2015.05.018⟩
DOI
DOI : 10.1016/j.tcs.2015.05.018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01250521/file/TCS_CMSB12.pdf BibTex
auteur
Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
titre
HASL: A new approach for performance evaluation and model checking from concepts to experimentation
article
Performance Evaluation, Elsevier, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩
DOI
DOI : 10.1016/j.peva.2015.04.003
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01221815/file/main.pdf BibTex
auteur
Walid Belkhir, Yannick Chevalier, Michael Rusinowitch
titre
Parametrized automata simulation and application to service composition
article
Journal of Symbolic Computation, Elsevier, 2015, pp.21
Accès au bibtex
BibTex
auteur
Béatrice Bérard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, Nathalie Sznajder, Sébastien Tixeuil, Xavier Urbain
titre
[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems
article
International Journal of Informatics Society, Japan Informatics Society, 2015, 7 (3), pp.101-114. ⟨http://www.infsoc.org/journal/vol07/IJIS_07_3_101-114.pdf⟩
Accès au bibtex
BibTex
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
Verified Compilation of Floating-Point Computations
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
DOI
DOI : 10.1007/s10817-014-9317-x
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862689/file/floating-point-compcert.pdf BibTex
auteur
Guillaume Bonfante, Florian Deloup, Antoine Henrot
titre
Real or natural numbers interpretations and their effect on complexity
article
Theoretical Computer Science, Elsevier, 2015, 585, pp.25-40. ⟨10.1016/j.tcs.2015.03.004⟩
DOI
DOI : 10.1016/j.tcs.2015.03.004
Accès au bibtex
BibTex
auteur
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
titre
From Security Protocols to Pushdown Automata
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 17 (1), ⟨10.1145/2811262⟩
DOI
DOI : 10.1145/2811262
Accès au bibtex
BibTex
auteur
Philippe Collet, Lydie Du Bousquet, Laurence Duchien, Pierre-Etienne Moreau
titre
Défis 2025
article
Techniques et sciences informatique (TSI), 2015, 34 (3), pp.311-324. ⟨http://tsi.revuesonline.com/article.jsp?articleId=21482⟩. ⟨10.3166/TSI.34.293-306⟩
DOI
DOI : 10.3166/TSI.34.293-306
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Formal verification of e-voting: solutions and challenges
article
SigLog Newsletter, ACM Special Interest Group on Logic and Computation, 2015, 2, pp.25-34. ⟨10.1145/2728816.2728823⟩
DOI
DOI : 10.1145/2728816.2728823
Accès au bibtex
BibTex
auteur
Jean-René Courtault, Didier Galmiche
titre
A Modal Separation Logic for Resource Dynamics
article
Journal of Logic and Computation, Oxford University Press (OUP), 2015, ⟨10.1093/logcom/exv031⟩
DOI
DOI : 10.1093/logcom/exv031
Accès au bibtex
BibTex
auteur
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
titre
Impossibility of gathering, a certification
article
Information Processing Letters, Elsevier, 2015, 115 (3), pp.447-452. ⟨10.1016/j.ipl.2014.11.001⟩
DOI
DOI : 10.1016/j.ipl.2014.11.001
Accès au bibtex
https://arxiv.org/pdf/1405.5902 BibTex
auteur
Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam, Ghazi Maatoug, Michaël Rusinowitch
titre
Model-based mutation testing from security protocols in HLPSL
article
Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2015, pp.30. ⟨10.1002/stvr.1531⟩
DOI
DOI : 10.1002/stvr.1531
Accès au bibtex
BibTex
auteur
Jannik Dreier, Jean-Guillaume Dumas, Pascal Lafourcade
titre
Brandt's fully private auction protocol revisited
article
Journal of Computer Security, IOS Press, 2015, Special issue on security and high performance computing systems, 23 (5), pp.587-610. ⟨10.3233/JCS-150535⟩
DOI
DOI : 10.3233/JCS-150535
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01233555/file/main.pdf BibTex
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, Andreas Weber
titre
Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
article
Journal of Computational Physics, Elsevier, 2015, 291, pp.279-302. ⟨10.1016/j.jcp.2015.02.050⟩
DOI
DOI : 10.1016/j.jcp.2015.02.050
Accès au bibtex
BibTex
auteur
Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, Romain Péchoux
titre
Characterizing polynomial time complexity of stream programs using interpretations
article
Theoretical Computer Science, Elsevier, 2015, 585, pp.41-54. ⟨10.1016/j.tcs.2015.03.008⟩
DOI
DOI : 10.1016/j.tcs.2015.03.008
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01112160/file/FEREE_HAINRY_HOYRUP_PECHOUX.pdf BibTex
auteur
Henryk Fukś, Nazim Fatès
titre
Local structure approximation as a predictor of second order phase transitions in asynchronous cellular automata
article
Natural Computing, Springer Verlag, 2015, 14 (4), pp.507-522. ⟨10.1007/s11047-015-9521-6⟩
DOI
DOI : 10.1007/s11047-015-9521-6
Accès au bibtex
BibTex
auteur
Marco Gaboardi, Romain Péchoux
titre
On Bounding Space Usage of Streams Using Interpretation Analysis
article
Science of Computer Programming, Elsevier, 2015, pp.44
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01112161/file/main-submitted.pdf BibTex
auteur
Didier Galmiche, Yakoub Salhi
titre
Tree-sequent calculi and decision procedures for intuitionistic modal logics
article
Journal of Logic and Computation, Oxford University Press (OUP), 2015, ⟨10.1093/logcom/exv039⟩
DOI
DOI : 10.1093/logcom/exv039
Accès au bibtex
BibTex
auteur
Simon J. Gay, Nils Gesbert, António Ravara, Vasco Thudichum Vasconcelos
titre
Modular session types for objects
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 4 (12), pp.76. ⟨10.2168/LMCS-11(4:12)2015⟩
DOI
DOI : 10.2168/LMCS-11(4:12)2015
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00700635/file/main.pdf BibTex
auteur
Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert
titre
Efficiently Deciding µ-calculus with Converse over Finite Trees
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 16 (2), pp.41. ⟨10.1145/2724712⟩
DOI
DOI : 10.1145/2724712
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00868722/file/tree-calculus.pdf BibTex
auteur
Nils Gesbert, Pierre Genevès, Nabil Layaïda
titre
A Logical Approach To Deciding Semantic Subtyping
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2015, 38 (1), pp.31. ⟨10.1145/2812805⟩
DOI
DOI : 10.1145/2812805
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00848023/file/article.pdf BibTex
auteur
Sylvain Gravier, Jérôme Javelle, Mehdi Mhalla, Simon Perdrix
titre
On weak odd domination and graph-based quantum secret sharing
article
Theoretical Computer Science, Elsevier, 2015, 598, ⟨10.1016/j.tcs.2015.05.038⟩
DOI
DOI : 10.1016/j.tcs.2015.05.038
Accès au bibtex
BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Characterizations of periods of multidimensional shifts
article
Ergodic Theory and Dynamical Systems, Cambridge University Press (CUP), 2015, 35 (2), pp.431--460. ⟨10.1017/etds.2013.60⟩
DOI
DOI : 10.1017/etds.2013.60
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00798336/file/arxiv.pdf BibTex
auteur
Emmanuel Jeandel, Pascal Vanier
titre
Hardness of conjugacy, embedding and factorization of multidimensional subshifts
article
Journal of Computer and System Sciences, Elsevier, 2015, http://dx.doi.org/10.1016/j.jcss.2015.05.003. ⟨10.1016/j.jcss.2015.05.003⟩
DOI
DOI : 10.1016/j.jcss.2015.05.003
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01150419/file/jcss.pdf BibTex
auteur
Thibault Maillot, Ugo Boscain, Jean-Paul Gauthier, Ulysse Serres
titre
Lyapunov and Minimum-Time Path Planning for Drones
article
Journal of Dynamical and Control Systems, Springer Verlag, 2015, 21 (1), pp.1-34. ⟨10.1007/s10883-014-9222-y⟩
DOI
DOI : 10.1007/s10883-014-9222-y
Accès au bibtex
BibTex
auteur
Aurel Randolph, Hanifa Boucheneb, Abdessamad Imine, Alejandro Quintero
titre
On Synthesizing a Consistent Operational Transformation Approach
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2015, 64 (4), pp.16
Accès au bibtex
BibTex
auteur
Aurel Randolph, Abdessamad Imine, Hanifa Boucheneb, Alejandro Quintero
titre
Spécification et Analyse d’un Protocole de Contrôle d’Accès Optimiste pour Éditeurs Collaboratifs Répartis
article
Revue des Sciences et Technologies de l'Information - Série ISI : Ingénierie des Systèmes d'Information, Lavoisier, 2015, pp.1
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
A Mechanical Calculator for Arithmetic Sequences (1844-1852): Part 1, Historical Context and Structure
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2015, 37 (4), pp.90-96. ⟨10.1109/MAHC.2015.79⟩
DOI
DOI : 10.1109/MAHC.2015.79
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
An overview of Schwilgué's patented adding machines
article
Bulletin of the Scientific Instrument Society, Scientific Instrument Society, 2015, 126, pp.16-22
Accès au bibtex
BibTex
auteur
Elena Tushkanova, Alain Giorgetti, Christophe Ringeissen, Olga Kouchnarenko
titre
A rule-based system for automatic decidability and combinability
article
Science of Computer Programming, Elsevier, 2015, Selected Papers from the Ninth International Workshop on Rewriting Logic and its Applications (WRLA 2012), 99, pp.3-23. ⟨10.1016/j.scico.2014.02.005⟩
DOI
DOI : 10.1016/j.scico.2014.02.005
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102883/file/TGRK14.pdf BibTex
auteur
Noam Zeilberger, Alain Giorgetti
titre
A correspondence between rooted planar maps and normal planar lambda terms
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (3:22), pp.1-39. ⟨http://www.lmcs-online.org/ojs/viewarticle.php?id=1695&layout=abstract⟩. ⟨10.2168/LMCS-11(3:22)2015⟩
DOI
DOI : 10.2168/LMCS-11(3:22)2015
Accès au bibtex
https://arxiv.org/pdf/1408.5028 BibTex

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

2012

auteur
Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michael Rusinowitch
titre
Unification modulo Homomorphic Encryption
article
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.135-158. ⟨10.1007/s10817-010-9205-y⟩
DOI
DOI : 10.1007/s10817-010-9205-y
Accès au bibtex
BibTex
auteur
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
titre
String rewriting and security analysis: an extension of a result of Book and Otto
article
Journal of Automata Languages and Combinatorics, Otto-von-Guericke-Universität Magdeburg, 2012, 16 (2--4), pp.83--98
Accès au bibtex
BibTex
auteur
Andrew Appel, Robert Dockins, Xavier Leroy
titre
A list-machine benchmark for mechanized metatheory
article
Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩
DOI
DOI : 10.1007/s10817-011-9226-1
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00674176/file/listmachine-journal.pdf BibTex
auteur
Laurent Bienvenu, Adam Day, Mathieu Hoyrup, Ilya Mezhirov, Alexander Shen
titre
A constructive version of Birkhoff's ergodic theorem for Martin-Lof random points
article
Information and Computation, Elsevier, 2012, 210, pp.021-030. ⟨10.1016/j.ic.2011.10.006⟩
DOI
DOI : 10.1016/j.ic.2011.10.006
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00643629/file/ergodic-edited.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Fabrice Sabatier, Aurélien Thierry
titre
Code synchronization by morphological analysis
article
7th International Conference on Malicious and Unwanted Software (Malware 2012), IEEE Xplore, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00764286/file/malware2012.pdf BibTex
auteur
Yannick Chevalier, Michael Rusinowitch
titre
Decidability of Equivalence of Symbolic Derivations
article
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.263-292. ⟨10.1007/s10817-010-9199-5⟩
DOI
DOI : 10.1007/s10817-010-9199-5
Accès au bibtex
BibTex
auteur
Stefan Ciobaca, Stéphanie Delaune, Steve Kremer
titre
Computing knowledge in security protocols under convergent equational theories
article
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.219-262. ⟨10.1007/s10817-010-9197-7⟩
DOI
DOI : 10.1007/s10817-010-9197-7
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00636794/file/CDK-jar10.pdf BibTex
auteur
Cyril Cohen, Assia Mahboubi
titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8 (1:02) 2012⟩
DOI
DOI : 10.2168/LMCS-8 (1:02) 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTex
auteur
Véronique Cortier, Stéphanie Delaune
titre
Decidability and combination results for two notions of knowledge in security protocols.
article
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (October), pp.441-487. ⟨10.1007/s10817-010-9208-8⟩
DOI
DOI : 10.1007/s10817-010-9208-8
Accès au bibtex
BibTex
auteur
Frédéric Dadeau, Kalou Cabrera Castillos, Régis Tissot
titre
Scenario-Based Testing using Symbolic Animation of B Models
article
Software Testing, Verification and Reliability, Wiley, 2012, 6 (22), pp.407-434. ⟨10.1002/stvr.1467⟩
DOI
DOI : 10.1002/stvr.1467
Accès au bibtex
BibTex
auteur
Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
titre
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
article
Science of Computer Programming, Elsevier, 2012, 77 (10-11), pp.1122-1150
Accès au bibtex
BibTex
auteur
Lionel Droz-Bartholet, Jean-Christophe Lapayre, Fabrice Bouquet, Eric Garcia, Alexander Heinisch
titre
Ramos: Concurrent Writing and Reconfiguration for Collaborative Systems
article
Journal of Parallel and Distributed Computing, Elsevier, 2012, 72 (5), pp.637--649. ⟨10.1016/j.jpdc.2012.02.012⟩
DOI
DOI : 10.1016/j.jpdc.2012.02.012
Accès au bibtex
BibTex
auteur
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
titre
An Implicit Characterization of PSPACE
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2012, 13 (2), pp.Article 18. ⟨10.1145/2159531.2159540⟩
DOI
DOI : 10.1145/2159531.2159540
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00591868/file/main.pdf BibTex
auteur
Stefano Galatolo, Mathieu Hoyrup, Cristobal Rojas
titre
Statistical properties of dynamical systems - simulation and abstract computation.
article
Chaos, Solitons and Fractals, Elsevier, 2012, 45 (1), pp.1-14. ⟨10.1016/j.chaos.2011.09.011⟩
DOI
DOI : 10.1016/j.chaos.2011.09.011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00644790/file/CSF.pdf BibTex
auteur
Gregor Goessler, Dana Xu, Alain Girault
titre
Probabilistic contracts for component-based design
article
Formal Methods in System Design, Springer Verlag, 2012, 41 (2), pp.211-231. ⟨10.1007/s10703-012-0162-4⟩
DOI
DOI : 10.1007/s10703-012-0162-4
Accès au bibtex
BibTex
auteur
Walid Gomaa
titre
A Survey of Recursive Analysis and Moore's Notion of Real Computation
article
Natural Computing, Springer Verlag, 2012, 11 (1), pp.37-49. ⟨10.1007/s11047-011-9278-5⟩
DOI
DOI : 10.1007/s11047-011-9278-5
Accès au bibtex
BibTex
auteur
Pierre-Cyrille Heam, Vincent Hugot, Olga Kouchnarenko
titre
Loops and overloops for Tree Walking Automata
article
Theoretical Computer Science, Elsevier, 2012, Implementation and Application of Automata (CIAA 2011), 450, pp.43-53. ⟨10.1016/j.tcs.2012.04.026⟩
DOI
DOI : 10.1016/j.tcs.2012.04.026
Accès au bibtex
BibTex
auteur
Mathieu Hoyrup, Cristobal Rojas, Klaus Weihrauch
titre
Computability of the Radon-Nikodym derivative.
article
Computability, IOS Press, 2012, 1 (1), pp.3-13. ⟨http://iospress.metapress.com/content/966432503uw60884/⟩. ⟨10.3233/COM-2012-005⟩
DOI
DOI : 10.3233/COM-2012-005
Accès au bibtex
BibTex
auteur
Fairouz Kamareddine, Karim Nour, Vincent Rahli, J. B. Wells
titre
Challenges and solutions to realisability semantics for intersection types with expansion variables
article
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2012, 121, pp.153-184
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00937952/file/fund-inf-short.pdf BibTex
auteur
Steve Kremer, Antoine Mercier, Ralf Treinen
titre
Reducing Equational Theories for the Decision of Static Equivalence
article
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.197-217. ⟨10.1007/s10817-010-9203-0⟩
DOI
DOI : 10.1007/s10817-010-9203-0
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00636797/file/KMT-jar10.pdf BibTex
auteur
Jacques Lemordant, Jean-Dominique Gascuel, Isabelle Bellin
titre
L'émergence de la réalité augmentée, à la frontière du réel et du virtuel
article
Collection "20 ans d'avancées et de perspectives en sciences du numérique", INRIA, 2012, 3 p
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00813184/file/L_A_mergence_de_la_rA_alitA_augmentA_e_A_la_frontiA_re_du_rA_el_et_du_virtuel.pdf BibTex
auteur
Jean-Yves Marion
titre
Viruses in Turing's Garden
article
ERCIM News, ERCIM, 2012, 2012 (91), ⟨http://ercim-news.ercim.eu/en91/special/viruses-in-turings-garden⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00762918/file/ErcimVirus.pdf BibTex
auteur
Jean-Yves Marion, Thomas Schwentick
titre
Theoretical Aspects of Computer Science
article
Theory of Computing Systems, Springer Verlag, 2012, 51 (2), pp.123-124
Accès au bibtex
BibTex
auteur
Jean-Yves Marion
titre
Les Mac résistent-ils mieux aux virus que les PC ?
article
Pour la science, Pour la science, 2012
Accès au bibtex
BibTex
auteur
Jean-Yves Marion
titre
From Turing machines to computer viruses
article
Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, Royal Society, The, 2012, 370 (1971), pp.3319-3339. ⟨10.1098/rsta.2011.0332⟩
DOI
DOI : 10.1098/rsta.2011.0332
Accès au bibtex
BibTex
auteur
Romain Péchoux
titre
Synthesis of sup-interpretations: a survey
article
Theoretical Computer Science, Elsevier, 2012, pp.24. ⟨10.1016/j.tcs.2012.11.003⟩
DOI
DOI : 10.1016/j.tcs.2012.11.003
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00744915/file/main.pdf BibTex
auteur
Nicolas Pouillard, François Pottier
titre
A unified treatment of syntax with binders
article
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (4--5), pp.614--704. ⟨10.1017/S0956796812000251⟩
DOI
DOI : 10.1017/S0956796812000251
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772721/file/pouillard-pottier-unified.pdf BibTex
auteur
Didier Rémy, Boris Yakobowski
titre
A Church-Style Intermediate Language for MLF
article
Theoretical Computer Science, Elsevier, 2012, 435, pp.77--105. ⟨10.1016/j.tcs.2012.02.026⟩
DOI
DOI : 10.1016/j.tcs.2012.02.026
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093719/file/xmlf%40tcs2011.pdf BibTex
auteur
Denis Roegel
titre
The LOCOMAT Project: Recomputing Mathematical and Astronomical Tables
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2012, 34 (2), pp.74-79. ⟨10.1109/MAHC.2012.32⟩
DOI
DOI : 10.1109/MAHC.2012.32
Accès au bibtex
BibTex

2011

auteur
Mouhebeddine Berrima, Narjes Ben Rajeb, Véronique Cortier
titre
Deciding knowledge in security protocols under some e-voting theories
article
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2011, 45 (3), pp.269-299. ⟨10.1051/ita/2011119⟩
DOI
DOI : 10.1051/ita/2011119
Accès au bibtex
BibTex
auteur
Yves Bertot, Frédérique Guilhot, Assia Mahboubi
titre
A formal study of Bernstein coefficients and polynomials
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
DOI
DOI : 10.1017/S0960129511000090
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503017/file/check_version_Jan_2011.pdf BibTex
auteur
Laurent Bienvenu, Peter Gacs, Mathieu Hoyrup, Cristobal Rojas, Alexander Shen
titre
Algorithmic tests and randomness with respect to a class of measures
article
Proceedings of the Steklov Institute of Mathematics, MAIK Nauka/Interperiodica, 2011, 274 (1), pp.34-89. ⟨10.1134/S0081543811060058⟩
DOI
DOI : 10.1134/S0081543811060058
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00644785/file/classes.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Jean-Yves Moyen
titre
Quasi-interpretations a way to control resources
article
Theoretical Computer Science, Elsevier, 2011, 412 (25), pp.2776-2796. ⟨10.1016/j.tcs.2011.02.007⟩
DOI
DOI : 10.1016/j.tcs.2011.02.007
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00591862/file/tcs.pdf BibTex
auteur
Tony Bourdier
titre
Specification, analysis and transformation of security policies via rewriting techniques
article
Journal of Information Assurance and Security, Dynamic Publishers Inc., USA, 2011, 6 (5), pp.357-368. ⟨http://www.mirlabs.org/jias/secured/Volume6-Issue5/vol6-issue5.html⟩
Accès au bibtex
BibTex
auteur
Olivier Bournez, Walid Gomaa, Emmanuel Hainry
titre
Algebraic Characterizations of Complexity-Theoretic Classes of Real Functions
article
International Journal of Unconventional Computing, Old City Publishing, 2011, 7 (5), pp.331-351
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00644361/file/ijuc_h.pdf BibTex
auteur
Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand
titre
Scenario-based testing from UML/OCL behavioral models Application to POSIX compliance
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2011, VSTTE 2009, 13 (5), pp.431-448. ⟨10.1007/s10009-011-0189-7⟩
DOI
DOI : 10.1007/s10009-011-0189-7
Accès au bibtex
BibTex
auteur
Véronique Cortier, Steve Kremer, Bogdan Warinschi
titre
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems.
article
Journal of Automated Reasoning, Springer Verlag, 2011, 46 (3-4), pp.225-259. ⟨10.1007/s10817-010-9187-9⟩
DOI
DOI : 10.1007/s10817-010-9187-9
Accès au bibtex
BibTex
auteur
Germain Faure, Chantal Keller, Thery Laurent, Gregoire Benjamin, Werner Benjamin, Armand Mickael
titre
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
article
CERTIFIED PROGRAMS AND PROOFS, Springer, 2011
Accès au bibtex
BibTex
auteur
Peter Gacs, Mathieu Hoyrup, Cristobal Rojas
titre
Randomness on Computable Probability Spaces—A Dynamical Point of View
article
Theory of Computing Systems, Springer Verlag, 2011, 48 (3), pp.465--485. ⟨10.1007/s00224-010-9263-x⟩
DOI
DOI : 10.1007/s00224-010-9263-x
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00531640/file/TOCScorrected.pdf BibTex
auteur
Stefano Galatolo, Mathieu Hoyrup, Cristobal Rojas
titre
Dynamics and abstract computability: computing invariant measures
article
Discrete and Continuous Dynamical Systems - Series A, American Institute of Mathematical Sciences, 2011, 29 (1), pp.193-212. ⟨10.3934/dcds.2011.29.193⟩
DOI
DOI : 10.3934/dcds.2011.29.193
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00517367/file/galat_1876_10.pdf BibTex
auteur
Didier Galmiche, Yakoub Salhi
titre
Sequent Calculi and Decidability for Intuitionistic Hybrid Logic
article
Information and Computation, Elsevier, 2011, 209 (12), pp.1447-1463. ⟨10.1016/j.ic.2011.10.002⟩
DOI
DOI : 10.1016/j.ic.2011.10.002
Accès au bibtex
BibTex
auteur
Isabelle Gnaedig, Hélène Kirchner
titre
Proving Weak Properties of Rewriting
article
Theoretical Computer Science, Elsevier, 2011, 412, pp.4405-4438. ⟨10.1016/j.tcs.2011.04.028⟩
DOI
DOI : 10.1016/j.tcs.2011.04.028
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00592271/file/weak-tcs-revision2.pdf BibTex
auteur
Pierre-Cyrille Heam
titre
On the Complexity of Computing the Profinite Closure of a Rational Language
article
Theoretical Computer Science, Elsevier, 2011, 412 (41), pp.5808-5813. ⟨10.1016/j.tcs.2011.06.022⟩
DOI
DOI : 10.1016/j.tcs.2011.06.022
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00641554/file/PROBINFheam.pdf BibTex
auteur
Jonathan Lasalle, Fabrice Bouquet, Bruno Legeard, Fabien Peureux
titre
SysML to UML model transformation for test generation purpose
article
Software Engineering Notes, Association for Computing Machinery, 2011, 36 (1), pp.1-8. ⟨10.1145/1921532.1921560⟩
DOI
DOI : 10.1145/1921532.1921560
Accès au bibtex
BibTex
auteur
Xavier Leroy
titre
Safety First! (technical perspective)
article
Communications of the ACM, ACM, 2011, 54 (12), pp.122. ⟨10.1145/2043174.2043196⟩
DOI
DOI : 10.1145/2043174.2043196
Accès au bibtex
BibTex
auteur
Christopher Lynch, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran
titre
Automatic Decidability and Combinability
article
Information and Computation, Elsevier, 2011, 209 (7), pp.1026-1047. ⟨10.1016/j.ic.2011.03.005⟩
DOI
DOI : 10.1016/j.ic.2011.03.005
Accès au bibtex
BibTex
auteur
Jean-Yves Marion
titre
Informatique et société : Un laboratoire de haute sécurité en informatique : entretien avec Jean-Yves Marion
article
Les Cahiers de l'INRIA - La Recherche, INRIA, 2011, Les 10 découvertes de l'année
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00591075/file/Un_laboratoire_de_haute_sA_curite_en_informatique.pdf BibTex
auteur
Atif Mashkoor, Jean-Pierre Jacquot
titre
Utilizing Event-B for Domain Engineering: A Critical Analysis
article
Requirements Engineering, Springer Verlag, 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00590700/file/main.pdf BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
A generic framework: from modeling to code
article
Innovations in Systems and Software Engineering (ISSE), Springer London, 2011, pp.1-9. ⟨http://dx.doi.org/10.1007/s11334-011-0165-0⟩
Accès au bibtex
BibTex
auteur
Walid Taha, Paul Brauner, Robert Cartwright, Veronica Gaspes, Aaron Ames, Alexandre Chapoutot
titre
A core language for executable models of cyber physical systems: work in progress report
article
ACM SIGBED Review, Association for Computing Machinery (ACM), 2011, 8 (2), pp.39-43. ⟨10.1145/2000367.2000376⟩
DOI
DOI : 10.1145/2000367.2000376
Accès au bibtex
BibTex
auteur
Mohamed Tounsi, Mohamed Mosbah, Dominique Méry
titre
Proving Distributed Algorithms by Combining Refinement and Local Computations
article
Electronic Communications of the EASST, 2011, 35, pp.ISSN 1863-2122
Accès au bibtex
BibTex

2010

auteur
Tarek Abbes, Adel Bouhoula, Michael Rusinowitch
titre
Efficient Decision Tree for Protocol Analysis in Intrusion Detection
article
International Journal of Security and Networks, Inderscience, 2010, 5 (4), pp.220-235. ⟨10.1504/IJSN.2010.037661⟩
DOI
DOI : 10.1504/IJSN.2010.037661
Accès au bibtex
BibTex
auteur
Guillaume Banneau, Mickaël Guedj, Gaëtan Macgrogan, Isabelle de Mascarel, Valerie Velasco, Renaud Schiappa, Valérie Bonadona, Albert David, Catherine Dugast, Brigitte Gilbert-Dussardier, Olivier Ingster, Pierre Vabres, Frédéric Caux, Aurelien de Reynies, Richard Iggo, Nicolas Sevenet, Françoise Bonnet, Michel Longy
titre
Molecular apocrine differentiation is a common feature of breast cancer in patients with germline PTEN mutations.
article
Breast Cancer Research, BioMed Central, 2010, 12 (4), pp.R63. ⟨10.1186/bcr2626⟩
DOI
DOI : 10.1186/bcr2626
Accès au texte intégral et bibtex
https://www.hal.inserm.fr/inserm-00663724/file/bcr2626.pdf BibTex
auteur
Laurent Bienvenu, Mathieu Hoyrup
titre
Une brève introduction à la théorie effective de l'aléatoire
article
Gazette des Mathématiciens, Société Mathématique de France, 2010, 123, pp.35-47. ⟨http://smf.emath.fr/Publications/Gazette/Nouveautes/smf_gazette_123_35-47.pdf⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00449022/file/kolmogorov-smf.pdf BibTex
auteur
Tony Bourdier, Horatiu Cirstea, Daniel Dougherty, Hélène Kirchner
titre
Extensional and Intensional Strategies
article
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2010, Reduction Strategies in Rewriting and Programming, 15, pp.1-19. ⟨10.4204/EPTCS.15.1⟩
DOI
DOI : 10.4204/EPTCS.15.1
Accès au bibtex
BibTex
auteur
Guillaume Burel, Claude Kirchner
titre
Regaining Cut Admissibility in Deduction Modulo using Abstract Completion
article
Information and Computation, Elsevier, 2010, 208 (2), pp.140-164. ⟨10.1016/j.ic.2009.10.005⟩
DOI
DOI : 10.1016/j.ic.2009.10.005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00132964/file/gencomp_ic.pdf BibTex
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
titre
Combining decision procedures by (model-)equality propagation
article
Science of Computer Programming, Elsevier, 2010, 240 (2 July 2009), pp.113-128. ⟨10.1016/j.entcs.2009.05.048⟩
DOI
DOI : 10.1016/j.entcs.2009.05.048
Accès au bibtex
BibTex
auteur
Fahima Cheikh, Pierre-Cyrille Héam, Olga Kouchnarenko
titre
Composition of Services with Constraints
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2010, 236 (Special Issue, selected papers of FACS'09), pp.31--46. ⟨10.1016/j.entcs.2010.05.003⟩
DOI
DOI : 10.1016/j.entcs.2010.05.003
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00560496/file/bchk10_ij.pdf BibTex
auteur
Yannick Chevalier, Michael Rusinowitch
titre
Symbolic Protocol Analysis in the Union of Disjoint Intruder Theories: Combining Decision Procedures
article
Theoretical Computer Science, Elsevier, 2010, 411 (10), pp.1261-1282. ⟨10.1016/j.tcs.2009.10.022⟩
DOI
DOI : 10.1016/j.tcs.2009.10.022
Accès au bibtex
BibTex
auteur
Yannick Chevalier, Michael Rusinowitch
titre
Compiling and securing cryptographic protocols
article
Information Processing Letters, Elsevier, 2010, 110 (3), pp.116-122
Accès au bibtex
BibTex
auteur
Horatiu Cirstea, Claude Kirchner, Radu Kopetz, Pierre-Etienne Moreau
titre
Anti-patterns for Rule-based Languages
article
Journal of Symbolic Computation, Elsevier, 2010, 54 (5), pp.523-550. ⟨10.1016/j.jsc.2010.01.007⟩
DOI
DOI : 10.1016/j.jsc.2010.01.007
Accès au bibtex
BibTex
auteur
Hubert Comon-Lundh, Véronique Cortier, Eugen Zalinescu
titre
Deciding security properties for cryptographic protocols. Application to key cycles.
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2010, 11 (2), pp.Article 9. ⟨10.1145/1656242.1656244⟩
DOI
DOI : 10.1145/1656242.1656244
Accès au bibtex
BibTex
auteur
Gilles Dowek, Thierry Vieville, Jean-Pierre Archambault, Emmanuel Baccelli, Benjamin Wack
titre
Les ingrédients des algorithmes
article
Interstices, INRIA, 2010, ⟨https://interstices.info/jcms/c_43821/les-ingredients-des-algorithmes⟩
Accès au bibtex
BibTex
auteur
Gilles Dowek, Thierry Vieville, Jean-Pierre Archambault, Emmanuel Baccelli, Benjamin Wack
titre
Tout a un reflet numérique
article
Interstices, INRIA, 2010, ⟨https://interstices.info/jcms/c_43823/tout-a-un-reflet-numerique⟩
Accès au bibtex
BibTex
auteur
Frédéric Fondement, P-A. Muller, Brice Wittmann, Fabrice Ambert, Fabrice Bouquet, Jonathan Lasalle, Emilie Oudot, Fabien Peureux, Bruno Legeard, M. Alter, C. Scherrer
titre
VETESS : IDM, Test et SysML
article
Génie logiciel, C & S, 2010, pp.43--48
Accès au bibtex
BibTex
auteur
Stefano Galatolo, Mathieu Hoyrup, Cristobal Rojas
titre
Effective symbolic dynamics, random points, statistical behavior, complexity and entropy
article
Information and Computation, Elsevier, 2010, 208 (1), pp.23-41. ⟨10.1016/j.ic.2009.05.001⟩
DOI
DOI : 10.1016/j.ic.2009.05.001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00517382/file/final.pdf BibTex
auteur
Didier Galmiche, Yakoub Salhi
titre
Label-free Natural Deduction Systems for Intuitionistic and Classical Modal Logics
article
Journal of Applied Non-Classical Logics, Editions Hermes, 2010, 20 (4), pp.373-421. ⟨10.3166/jancl.20.373-421⟩
DOI
DOI : 10.3166/jancl.20.373-421
Accès au bibtex
BibTex
auteur
Didier Galmiche, Yakoub Salhi
titre
A Family of Gödel Hybrid Logics
article
Journal of Applied Logic, Elsevier, 2010, 8 (4), pp.371-385. ⟨10.1016/j.jal.2010.08.008⟩
DOI
DOI : 10.1016/j.jal.2010.08.008
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Mery
titre
Tableaux and Resource Graphs for Separation Logic
article
Journal of Logic and Computation, Oxford University Press (OUP), 2010, 20 (1), pp.189-231. ⟨10.1093/logcom/exn066⟩
DOI
DOI : 10.1093/logcom/exn066
Accès au bibtex
BibTex
auteur
Georges Gonthier, Assia Mahboubi
titre
An introduction to small scale reflection in Coq
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTex
auteur
Pierre-Cyrille Heam, Cyril Nicaud, Sylvain Schmitz
titre
Parametric Random Generation of Deterministic Tree Automata
article
Theoretical Computer Science, Elsevier, 2010, 411 (1), pp.3469--3480
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561274/file/hns10_ij.pdf BibTex
auteur
Pierre-Cyrille Heam, Olga Kouchnarenko, Jérôme Voinot
titre
Component Simulation-based Substitutivity Managing QoS and Composition Issues
article
Science of Computer Programming, Elsevier, 2010, 75 (10), pp.898-917. ⟨10.1016/j.scico.2010.02.004⟩
DOI
DOI : 10.1016/j.scico.2010.02.004
Accès au bibtex
BibTex
auteur
Pierre-Cyrille Héam, Olga Kouchnarenko, Jérôme Voinot
titre
Component Simulation-based Substitutivity Managing QoS and Composition Issues
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2010, 260, pp.109--123. ⟨10.1016/j.entcs.2009.12.034⟩
DOI
DOI : 10.1016/j.entcs.2009.12.034
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561275/file/hkv10a_ij.pdf BibTex
auteur
Jean-Pierre Jacquot, Régine Laleau, Hassan Mountassir, Vincent Poirriez
titre
Assemblage de composants digne de confiance : de l'expression des besoins aux spécifications formelles
article
Génie logiciel, C & S, 2010, pp.13-18
Accès au bibtex
BibTex
auteur
Liu Jing, Laurent Vigneron
titre
Design and Verification of a Non-repudiation Protocol Based on Receiver-Side Smart Card
article
IET Information Security, Institution of Engineering and Technology, 2010, 4 (1), pp.15-29
Accès au bibtex
BibTex
auteur
Xavier Leroy
titre
Comment faire confiance à un compilateur ?
article
Interstices, INRIA, 2010, ⟨https://interstices.info/jcms/n_52365/comment-faire-confiance-a-un-compilateur⟩
Accès au bibtex
BibTex
auteur
Xavier Leroy
titre
Comment faire confiance à un compilateur ?
article
Les Cahiers de l'INRIA - La Recherche, INRIA, 2010, Cancer la révolution
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00511377/file/inria-n440-avril10.pdf BibTex
auteur
Luigi Liquori, Arnaud Spiwack
titre
Extending FeatherTrait Java with Interfaces
article
Theoretical Computer Science, Elsevier, 2010, Theoretical Computer Science, 30 (1-3), pp.243-260. ⟨10.1016/j.tcs.2008.01.051⟩
DOI
DOI : 10.1016/j.tcs.2008.01.051
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432540/file/TCS-60.pdf BibTex
auteur
Jean-Yves Marion, Joanna Jongwane
titre
À propos de la virologie informatique
article
Interstices, INRIA, 2010
Accès au bibtex
BibTex
auteur
Jean-Yves Marion, Matthieu Kaczmarek
titre
Boulevard du cybercrime
article
Dossier Pour la Science, Dossier pour la Science, 2010, pp.78-85
Accès au bibtex
BibTex
auteur
Pierre-Alain Masson, Marie-Laure Potet, Jacques Julliand, Régis Tissot, Bruno Legeard, Boutheina Chetali, Fabrice Bouquet, Eddie Jaffuel, June Andronick, Amal Haddad
titre
An Access Control Model Based Testing Approach for Smart Card Applications: Results of the POSÉ Project
article
Journal of Information Assurance and Security, Dynamic Publishers Inc., USA, 2010, 5 (1), pp.335-351. ⟨http://www.mirlabs.org/jias/secured/Volume5-Issue1/Masson.pdf⟩
Accès au bibtex
BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Functional Behavior of a Cardiac Pacing System
article
International Journal of Discrete Event Control Systems (IJDECS), Dr. Mohamed Khalgui, 2010
Accès au bibtex
BibTex
auteur
Olfa Mosbahi, Jacques Jaray
titre
B événementiel et les propriétés de vivacité
article
Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2010, 44 (9-10), pp.1119-1163. ⟨10.3166/jesa.44.1119-1163⟩
DOI
DOI : 10.3166/jesa.44.1119-1163
Accès au bibtex
BibTex
auteur
Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch
titre
Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
article
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2010, 105 (1-2), pp.163--187. ⟨10.3233/FI-2010-362⟩
DOI
DOI : 10.3233/FI-2010-362
Accès au bibtex
BibTex
auteur
Joris Rehm
titre
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2010, Special Section On ISOLA 2007, 12 (1), pp.39-51. ⟨10.1007/s10009-009-0130-5⟩
DOI
DOI : 10.1007/s10009-009-0130-5
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00336624/file/rcp_sttt.pdf BibTex
auteur
Denis Roegel
titre
O rozboru jednoho makra
article
Zpravodaj (Československého sdružení uživatelů TeXu, ISSN 1211-6661), Groupe des utilisateurs de TeX tchèques, 2010, 20 (1-2), pp.68-76
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00548909/file/roegel-czech2.pdf BibTex
auteur
Denis Roegel
titre
Sudoku s vepsanými kandži: integrace čínských glyfů s grafikou na úrovni METAPOSTu
article
Zpravodaj (Československého sdružení uživatelů TeXu, ISSN 1211-6661), Groupe des utilisateurs de TeX tchèques, 2010, 20 (3), pp.220-226
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00548912/file/roegel-czech4.pdf BibTex
auteur
Denis Roegel
titre
Kulové plochy, hlavní kružnice a rovnoběžky
article
Zpravodaj (Československého sdružení uživatelů TeXu, ISSN 1211-6661), Groupe des utilisateurs de TeX tchèques, 2010, 20 (1-2), pp.23-38
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00548908/file/roegel-czech1.pdf BibTex
auteur
Denis Roegel
titre
Jednoduché makro suanpan na kreslení čínského a japonského abaku
article
Zpravodaj (Československého sdružení uživatelů TeXu, ISSN 1211-6661), Groupe des utilisateurs de TeX tchèques, 2010, 20 (3), pp.138-151
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00548910/file/roegel-czech3.pdf BibTex
auteur
Pierre Saqui-Sannes, Thierry Villemur, Benjamin Fontan, Sara del Socorro Mota Gonzalez, Mohamed Salah Bouassida, Najah Chridi, Isabelle Chrisment, Laurent Vigneron
titre
Formal Verification of Secure Group Communication Protocols Modelled in UML
article
Innovations in Systems and Software Engineering, Springer Verlag, 2010, Special Issue ICFEM'09, 6 (1-2), pp.125-133. ⟨10.1007/s11334-010-0122-3⟩
DOI
DOI : 10.1007/s11334-010-0122-3
Accès au bibtex
BibTex
auteur
Duc-Khanh Tran, Christophe Ringeissen, Silvio Ranise, Hélène Kirchner
titre
Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation
article
Journal of Symbolic Computation, Elsevier, 2010, Automated Deduction: Decidability, Complexity, Tractability, 45 (2), pp.261-286. ⟨10.1016/j.jsc.2008.10.006⟩
DOI
DOI : 10.1016/j.jsc.2008.10.006
Accès au bibtex
BibTex
auteur
Hehua Zhang, Stephan Merz, Ming Gu
titre
Specifying and Verifying PLC systems with TLA+: a case study
article
Computers and Mathematics with Applications, Elsevier, 2010, 60 (3), pp.695-705. ⟨10.1016/j.camwa.2010.05.017⟩
DOI
DOI : 10.1016/j.camwa.2010.05.017
Accès au bibtex
BibTex
auteur
Daniele Zucchelli, Enrica Nicolini
titre
A Decidability Result for the Model Checking of Infinite-State Systems
article
Journal of Automated Reasoning, Springer Verlag, 2010, (Online), ⟨10.1007/s10817-010-9192-z⟩
DOI
DOI : 10.1007/s10817-010-9192-z
Accès au bibtex
BibTex

2009

auteur
Humberto Abdelnur, Tigran Avanesov, Michael Rusinowitch, Radu State
titre
Abusing SIP authentication
article
Journal of Information Assurance and Security, Dynamic Publishers Inc., USA, 2009, Special Issue on Access Control and Protcols, 4 (4), pp.311-318
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00405356/file/jias-SIP.pdf BibTex
auteur
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz
titre
New results on rewrite-based satisfiability procedures
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (1), Article 4, 51 p. ⟨10.1145/1459010.1459014⟩
DOI
DOI : 10.1145/1459010.1459014
Accès au bibtex
BibTex
auteur
Dominique Barth, Johanne Cohen, Olivier Bournez, Octave Boussaton
titre
Distributed Learning of Equilibria in a Routing Game
article
Parallel Processing Letters, World Scientific Publishing, 2009, 19 (2), pp.189-204. ⟨10.1142/S012962640900016X⟩
DOI
DOI : 10.1142/S012962640900016X
Accès au bibtex
BibTex
auteur
Mathieu Baudet, Véronique Cortier, Steve Kremer
titre
Computationally Sound Implementations of Equational Theories against Passive Adversaries
article
Information and Computation, Elsevier, 2009, 207 (4), pp.496-520. ⟨10.1016/j.ic.2008.12.005⟩
DOI
DOI : 10.1016/j.ic.2008.12.005
Accès au bibtex
BibTex
auteur
Sandrine Blazy, Xavier Leroy
titre
Mechanized semantics for the Clight subset of the C language
article
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩
DOI
DOI : 10.1007/s10817-009-9148-3
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00352524/file/paper.pdf BibTex
auteur
Yohan Boichut, Roméo Courbis, Pierre-Cyrille Héam, Olga Kouchnarenko
titre
Handling Non Left-Linear Rules When Completing Tree Automata
article
International Journal of Foundations of Computer Science, World Scientific Publishing, 2009, 20 (5), pp.837--849. ⟨10.1142/S0129054109006917⟩
DOI
DOI : 10.1142/S0129054109006917
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561373/file/bchk09_ij.pdf BibTex
auteur
Yohan Boichut, Pierre-Cyrille Héam, Olga Kouchnarenko
titre
Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, 239, pp.57--72. ⟨10.1016/j.entcs.2009.05.030⟩
DOI
DOI : 10.1016/j.entcs.2009.05.030
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561374/file/bhk09_ij.pdf BibTex
auteur
Guillaume Bonfante, Yves Guiraud
titre
Polygraphic programs and polynomial-time functions
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2009, 5 (2:14), pp.1-37. ⟨10.2168/LMCS-5(2:14)2009⟩
DOI
DOI : 10.2168/LMCS-5(2:14)2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00122932/file/polypoly.pdf BibTex
auteur
Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion
titre
Architecture of a Morphological Malware Detector
article
Journal in Computer Virology, Springer Verlag, 2009, 5 (3), pp.263-270. ⟨10.1007/s11416-008-0102-4⟩
DOI
DOI : 10.1007/s11416-008-0102-4
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00330022/file/flowgraph.pdf BibTex
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
titre
Combining Decision Procedures by (Model-)Equality Propagation
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008), 240 (2), pp.113-128. ⟨10.1016/j.entcs.2009.05.048⟩
DOI
DOI : 10.1016/j.entcs.2009.05.048
Accès au bibtex
BibTex
auteur
Dominique Cansell, Dominique Méry, Cyril Proch
titre
System-on-chip design by proof-based refinement
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2009, 11 (3), pp.217-238. ⟨10.1007/s10009-009-0104-7⟩
DOI
DOI : 10.1007/s10009-009-0104-7
Accès au bibtex
BibTex
auteur
Bernadette Charron-Bost, Stephan Merz
titre
Formal Verification of a Consensus Algorithm in the Heard-Of Model
article
International Journal of Software and Informatics (IJSI), ISCAS, 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303
Accès au bibtex
BibTex
auteur
Véronique Cortier, Stéphanie Delaune
titre
Safely composing security protocols
article
Formal Methods in System Design, Springer Verlag, 2009, 34 (1), pp.1--36. ⟨10.1007/s10703-008-0059-4⟩
DOI
DOI : 10.1007/s10703-008-0059-4
Accès au bibtex
BibTex
auteur
Frédéric Dadeau, Amal Haddad, Thierry Moutet
titre
Test fonctionnel de conformité vis-à-vis d'une politique de contôle d'accès
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2009, Supervision et sécurité dans les grands réseaux, 28 (4), pp.533-563. ⟨10.3166/tsi.28.533-563⟩
DOI
DOI : 10.3166/tsi.28.533-563
Accès au bibtex
BibTex
auteur
Frédéric Dadeau, Pierre-Cyrille Héam, Jocelyn Levrey
titre
On the Use of Uniform Random Generation of Automata for Testing
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of Fifth Workshop on Model Based Testing (MBT 2009), 253 (2), pp.37-51. ⟨10.1016/j.entcs.2009.09.050⟩
DOI
DOI : 10.1016/j.entcs.2009.09.050
Accès au bibtex
BibTex
auteur
Frédéric Dadeau, Régis Tissot
titre
jSynoPSys - A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of Fifth Workshop on Model Based Testing (MBT 2009), 253 (2), pp.117-132. ⟨10.1016/j.entcs.2009.09.055⟩
DOI
DOI : 10.1016/j.entcs.2009.09.055
Accès au bibtex
BibTex
auteur
Zaynah Dargaye, Xavier Leroy
titre
A verified framework for higher-order uncurrying optimizations
article
Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (3), ⟨10.1007/s10990-010-9050-z⟩
DOI
DOI : 10.1007/s10990-010-9050-z
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499915/file/higher-order-uncurrying.pdf BibTex
auteur
Julien Dormoy, Olga Kouchnarenko, Hassan Mountassir
titre
Politiques d'adaptation pour la reconfiguration du composant de localisation
article
Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2009, 43 (7-8-9), pp.773-789
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00434482/file/dkm09-msr.pdf BibTex
auteur
Gilles Dowek, Joanna Jongwane
titre
À propos de l’enseignement de l’informatique
article
Interstices, INRIA, 2009
Accès au bibtex
BibTex
auteur
Didier Fass
titre
Design et ingénierie des systèmes homme-dans-la boucle
article
La revue des Ingénieurs, InterMines, 2009, R&D dans la santé: et demain ?, pp.50-51
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00437320/file/Fass.pdf BibTex
auteur
Isabelle Gnaedig, Hélène Kirchner
titre
Termination of Rewriting under Strategies
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (2), pp.1-52. ⟨10.1145/1462179.1462182⟩
DOI
DOI : 10.1145/1462179.1462182
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00182432/file/version-preli-tocl.pdf BibTex
auteur
Yves Guiraud, Philippe Malbos
titre
Higher-dimensional categories with finite derivation type
article
Theory and Applications of Categories, Mount Allison University, 2009, 22 (18), pp.420-478
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00326974/file/ntdf.pdf BibTex
auteur
Tom Hirschowitz, Xavier Leroy, J. B. Wells
titre
Compilation of extended recursion in call-by-value functional languages
article
Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (1), pp.3-66. ⟨10.1007/s10990-009-9042-z⟩
DOI
DOI : 10.1007/s10990-009-9042-z
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00359213/file/letrec.pdf BibTex
auteur
Claude Kirchner, Helene Kirchner, Anderson Santana de Oliveira
titre
Analysis of Rewrite-Based Access Control Policies
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Third International Workshop on Security and Rewriting Techniques (SecReT 2008), Pittsburgh, PA, USA, 22 June 2008, 234, pp.55-75. ⟨10.1016/j.entcs.2009.02.072⟩
DOI
DOI : 10.1016/j.entcs.2009.02.072
Accès au bibtex
BibTex
auteur
Dominique Larchey-Wendling, Didier Galmiche
titre
Exploring the relation between intuitionistic bi and boolean bi: An unexpected embedding
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2009, 19 (3), pp.435--500. ⟨10.1017/S0960129509007567⟩
DOI
DOI : 10.1017/S0960129509007567
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00577929/file/LarcheyGalmiche.pdf BibTex
auteur
Didier Le Botlan, Didier Rémy
titre
Recasting MLF
article
Information and Computation, Elsevier, 2009, Volume 207, Issue 6, June 2009, Pages 726-785, 207 (6), pp.726-785. ⟨10.1016/j.ic.2008.12.006⟩
DOI
DOI : 10.1016/j.ic.2008.12.006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00156628/file/recasting-mlf-RR.pdf BibTex
auteur
Xavier Leroy, Hervé Grall
titre
Coinductive big-step operational semantics
article
Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩
DOI
DOI : 10.1016/j.ic.2007.12.004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00309010/file/leroy-grall.pdf BibTex
auteur
Xavier Leroy
titre
A formally verified compiler back-end
article
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
DOI
DOI : 10.1007/s10817-009-9155-4
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00360768/file/paper2.pdf BibTex
auteur
Xavier Leroy
titre
Formal verification of a realistic compiler
article
Communications- ACM, Association for Computing Machinery, 2009, 52 (7), pp.107-115. ⟨10.1145/1538788.1538814⟩
DOI
DOI : 10.1145/1538788.1538814
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00415861/file/compcert-CACM.pdf BibTex
auteur
Jean-Yves Marion
titre
On tiered small jump operators
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2009, 5 (1), pp.1-19
Accès au bibtex
https://arxiv.org/pdf/0903.2410 BibTex
auteur
Jean-Yves Marion, Romain Péchoux
titre
Sup-interpretations, a semantic method for static analysis of program resources
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (4), 30 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00446057/file/333pechoux.pdf BibTex
auteur
Dominique Méry
titre
A Simple Refinement-based Method for Constructing Algorithms
article
ACM SIGCSE Bulletin, 2009, inroads — SIGCSE Bulletin, 41 (2), pp.51-59. ⟨10.1145/1595453.1595462⟩
DOI
DOI : 10.1145/1595453.1595462
Accès au bibtex
BibTex
auteur
Dominique Méry
titre
Refinement-Based Guidelines for Algorithmic Systems
article
International Journal of Software and Informatics (IJSI), ISCAS, 2009, 3 (2-3), pp.197-239
Accès au bibtex
BibTex
auteur
Fabrice Nahon, Claude Kirchner, Hélène Kirchner, Paul Brauner
titre
Inductive Proof Search Modulo
article
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2009, Special Issue on First-Order Theorem Proving / Guest Edited by Silvio Ranise and Ullrich Hustadt, 55 (1), pp.123-154. ⟨10.1007/s10472-009-9154-5⟩
DOI
DOI : 10.1007/s10472-009-9154-5
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00337380/file/ftp-amai.pdf BibTex
auteur
Vincent Pretre, Adrien de Kermadec, Fabrice Bouquet, Christophe Lang, Frédéric Dadeau
titre
Automated UML models merging for web services testing
article
International Journal of Web and Grid Services, Inderscience, 2009, 5 (2), pp.107--129. ⟨10.1504/IJWGS.2009.027569⟩
DOI
DOI : 10.1504/IJWGS.2009.027569
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00560822/file/pdkbl_09_ij.pdf BibTex
auteur
Denis Roegel
titre
Spheres, great circles and parallels
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.80-87
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
MetaPost macros for drawing Chinese and Japanese abaci
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.74-79
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Prototype Fragments from Babbage's First Difference Engine
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2009, 31 (2), pp.70-75
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
An introduction to nomography: Garrigues' nomogram for the computation of Easter
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.88-104
Accès au bibtex
BibTex
auteur
Benjamin Werner
titre
La vérité et la machine
article
Interstices, INRIA, 2009, ⟨https://interstices.info/jcms/c_42623/la-verite-et-la-machine⟩
Accès au bibtex
BibTex

2008

auteur
Boulbaba Ben Ammar, Mohamed Tahar Bhiri, Jeanine Souquières
titre
Incremental development of UML specifications using operation refinements
article
Innovations in Systems and Software Engineering, Springer Verlag, 2008, 4, pp.259-266. ⟨10.1007/s11334-008-0056-1⟩
DOI
DOI : 10.1007/s11334-008-0056-1
Accès au bibtex
BibTex
auteur
Boulbaba Ben Ammar, Mahamed Tahar Bhiri, Jeanine Souquières
titre
Modélisation événementielle pour la construction de diagrammes de classes
article
Revue des Sciences et Technologies de l'Information - Série ISI : Ingénierie des Systèmes d'Information, Lavoisier, 2008, 13 (3), pp.131-155
Accès au bibtex
BibTex
auteur
Jérôme Besombes, Jean-Yves Marion
titre
Learning discrete categorial grammars from structures
article
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2008, 42 (1), pp.165-182. ⟨10.1051/ita:2007055⟩
DOI
DOI : 10.1051/ita:2007055
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00342331/file/BesombesMarion.pdf BibTex
auteur
Yohan Boichut, Pierre-Cyrille Heam
titre
A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations
article
Information Processing Letters, Elsevier, 2008, 108 (1), pp.1-2. ⟨10.1016/j.ipl.2008.03.012⟩
DOI
DOI : 10.1016/j.ipl.2008.03.012
Accès au bibtex
BibTex
auteur
Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Approximation based tree regular model checking
article
Nordic Journal of Computing, Publishing Association Nordic Journal of Computing, 2008, 14, pp.216-241
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00429345/file/Haltreermc.pdf BibTex
auteur
Dominique Cansell, Paul Gibson, Dominique Méry
titre
Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 183, pp.39-55. ⟨10.1016/j.entcs.2007.01.060⟩
DOI
DOI : 10.1016/j.entcs.2007.01.060
Accès au bibtex
BibTex
auteur
Gérard Cécé, Pierre-Cyrille Héam, Yann Mainier
titre
Efficiency of Automata in Semi-Commutation Verification Techniques
article
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2008, 42 (2), pp.197--215. ⟨10.1051/ita:2007029⟩
DOI
DOI : 10.1051/ita:2007029
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00563430/file/chm08_ij.pdf BibTex
auteur
Yannick Chevalier, Ralf Kuesters, Michael Rusinowitch, Mathieu Turuani
titre
Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2008, 9 (4), pp.Article 24. ⟨10.1145/1380572.1380573⟩
DOI
DOI : 10.1145/1380572.1380573
Accès au bibtex
BibTex
auteur
Yannick Chevalier, Michael Rusinowitch
titre
Hierarchical combination of intruder theories
article
Information and Computation, Elsevier, 2008, 206 (2-4), pp.352-377. ⟨10.1016/j.ic.2007.07.004⟩
DOI
DOI : 10.1016/j.ic.2007.07.004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00329715/file/main.pdf BibTex
auteur
Johanne Cohen, Anurag Dasgupta, Sukumar Ghosh, Sébastien Tixeuil
titre
An Exercise in Selfish Stabilization
article
ACM Transactions on Autonomous and Adaptive Systems, Association for Computing Machinery (ACM), 2008, 3 (4), pp.Article 15. ⟨10.1145/1452001.1452005⟩
DOI
DOI : 10.1145/1452001.1452005
Accès au bibtex
BibTex
auteur
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
titre
Soft Linear Logic and Polynomial Complexity Classes
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 205 (6), pp.67-87. ⟨10.1016/j.entcs.2008.03.066⟩
DOI
DOI : 10.1016/j.entcs.2008.03.066
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00342320/file/GaboardiMarionRonchi08lsfa.pdf BibTex
auteur
Filipe Gama, Claire Bréhélin, Éric Gelhaye, Yves Meyer, Jean-Pierre Jacquot, Pascal Rey, Nicolas Rouhier
titre
Functional analysis and expression characteristics of chloroplastic Prx IIE
article
Physiologia Plantarum, Wiley, 2008, 133 (3), pp.599-610. ⟨10.1111/j.1399-3054.2008.01097.x⟩
DOI
DOI : 10.1111/j.1399-3054.2008.01097.x
Accès au bibtex
BibTex
auteur
Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
titre
A comprehensive combination framework
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2008, 9 (2), pp.Article n° 8. ⟨10.1145/1342991.1342992⟩
DOI
DOI : 10.1145/1342991.1342992
Accès au bibtex
BibTex
auteur
Alain Giorgetti, Julien Groslambert, Jacques Julliand, Olga Kouchnarenko
titre
Verification of class liveness properties with Java modeling language
article
IET Software, Institution of Engineering and Technology, 2008, 2 (6), pp.500--514. ⟨10.1049/iet-sen:20080008⟩
DOI
DOI : 10.1049/iet-sen:20080008
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561340/file/ggjk08_ij.pdf BibTex
auteur
Nawal Guermouche, Olivier Perrin, Christophe Ringeissen
titre
Timed Specification For Web Services Compatibility Analysis
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 200 (3), pp.155-170. ⟨10.1016/j.entcs.2008.04.098⟩
DOI
DOI : 10.1016/j.entcs.2008.04.098
Accès au bibtex
BibTex
auteur
Pierre-Cyrille Héam
titre
A Note on Partially Ordered Tree Automata
article
Information Processing Letters, Elsevier, 2008, 108 (4), pp.242--246. ⟨10.1016/j.ipl.2008.05.012⟩
DOI
DOI : 10.1016/j.ipl.2008.05.012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00561271/file/heam08_ij.pdf BibTex
auteur
Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron
titre
Tree automata with equality constraints modulo equational theories
article
Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pp.182-208. ⟨10.1016/j.jlap.2007.10.006⟩
DOI
DOI : 10.1016/j.jlap.2007.10.006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00329693/file/JacquemardRusinowitchVigneron-JLAP.pdf BibTex
auteur
Arnaud Lanoix, Jeanine Souquières
titre
Trustworthy Assembly of Components using B Refinement
article
e-Informatica Software Engineering Journal (ISEJ), 2008, 2 (1), 19 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00123997/file/e-informatica-submitted.pdf BibTex
auteur
Arnaud Lanoix, Samuel Colin, Jeanine Souquières
titre
Développement formel par composants : assemblage et vérification à l'aide de B
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2008, 27 (8), pp.1007-1032. ⟨10.3166/TSI.27.1007-1032⟩
DOI
DOI : 10.3166/TSI.27.1007-1032
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00180972/file/LanoixColinSouquieres_tsi08.pdf BibTex
auteur
Xavier Leroy, Sandrine Blazy
titre
Formal verification of a C-like memory model and its uses for verifying program transformations
article
Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩
DOI
DOI : 10.1007/s10817-008-9099-0
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289542/file/memory-model-journal.pdf BibTex
auteur
Luigi Liquori, Arnaud Spiwack
titre
FeatherTrait: A Modest Extension of Featherweight Java
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2008, ACM Transactions on Programming Languages and Systems (TOPLAS), 30 (2), pp.11:1--11:32. ⟨10.1145/1330017.1330022⟩
DOI
DOI : 10.1145/1330017.1330022
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432538/file/fjtraits.pdf BibTex
auteur
Inès Mouakher, Jeanine Souquières, Francis Alexandre
titre
Diagnostic et correction d'erreurs de spécifications : application à l'assemblage de composants
article
RTSI - L'Objet, 2008, 14, pp.11--42
Accès au bibtex
BibTex
auteur
Laurence Rideau, Bernard Serpette, Xavier Leroy
titre
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
article
Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩
DOI
DOI : 10.1007/s10817-007-9096-8
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289709/file/parallel-move.pdf BibTex
auteur
Denis Roegel
titre
Kanji-Sudokus: Integrating Chinese and Graphics
article
Tugboat, TeX Users Group, 2008, 29 (2), pp.317-319
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
An Early (1844) Key-Driven Adding Machine
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2008, 30 (1), pp.59-65. ⟨10.1109/MAHC.2008.1⟩
DOI
DOI : 10.1109/MAHC.2008.1
Accès au bibtex
BibTex
auteur
Jeanine Souquières
titre
A Component-Based Approach for the Specification and Verification of Safety Critical Software: Application to a Platoon of Vehicles
article
ERCIM News, ERCIM, 2008, 75, pp.33-34
Accès au bibtex
BibTex
auteur
Benjamin Wack, Clement Houtmann
titre
Strong Normalization in two Pure Pattern Type Systems
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, Rewriting calculi, higher-order reductions and patterns, 18 (3), pp.431-465. ⟨10.1017/S0960129508006749⟩
DOI
DOI : 10.1017/S0960129508006749
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00186815/file/sn42ppts.pdf BibTex

2007

auteur
Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu
titre
Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.321-341. ⟨10.1007/s00165-007-0027-6⟩
DOI
DOI : 10.1007/s00165-007-0027-6
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00097383/file/fac07.pdf BibTex
auteur
Dominique Barth, Johanne Cohen, Alain Denise, Romain Rivière
titre
Shuffling biological sequences with motif constraints.
article
Journal of Discrete Algorithms, Elsevier, 2007, ⟨10.1016/j.jda.2007.06.001⟩
DOI
DOI : 10.1016/j.jda.2007.06.001
Accès au bibtex
BibTex
auteur
Dominique Barth, Johanne Cohen, Taoufik Faik
titre
On the B-Continuity Property of Graphs
article
Discrete Applied Mathematics, Elsevier, 2007, 155 (13), pp.1761 - 1768. ⟨10.1016/j.dam.2007.04.011⟩
DOI
DOI : 10.1016/j.dam.2007.04.011
Accès au bibtex
BibTex
auteur
Gilles Barthe, Leonor Prensa Nieto
titre
Secure Information Flow for a Concurrent Language with Scheduling
article
Journal of Computer Security, IOS Press, 2007, Formal Methods in Security Engineering Workshop (FMSE 04), 16 (6), pp.647 - 689
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00097395/file/barthe_prensa.pdf BibTex
auteur
Philippe Beaucamps
titre
Polymorphisme Viral sous Linux (Viral Polymorphism in Linux)
article
GNU/Linux Magazine France, Diamond Editions, 2007, Hors Série 32
Accès au bibtex
BibTex
auteur
Philippe Beaucamps, Eric Filiol
titre
On the possibility of practically obfuscating programs - Towards a unified perspective of code protection
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (1), pp.3-21. ⟨10.1007/s11416-006-0029-6⟩
DOI
DOI : 10.1007/s11416-006-0029-6
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338074/file/beaucamps-filiol07-obfuscation.pdf BibTex
auteur
Jérôme Besombes, Jean-Yves Marion
titre
Learning tree languages from positive examples and membership queries
article
Theoretical Computer Science, Elsevier, 2007, 382 (3), pp.183-197
Accès au bibtex
BibTex
auteur
Nicolas Biri, Didier Galmiche
titre
Models and Separation Logics for Resource Trees
article
Journal of Logic and Computation, Oxford University Press (OUP), 2007, 17 (4), pp.687-726. ⟨10.1093/logcom/exm019⟩
DOI
DOI : 10.1093/logcom/exm019
Accès au bibtex
BibTex
auteur
Sandrine Blazy
titre
Comment gagner confiance en C ?
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩
DOI
DOI : 10.3166/TSI.26.1195-1200
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00292049/file/TSIchronique_sansentete.pdf BibTex
auteur
Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Vérifier automatiquement les protocoles de sécurité
article
Techniques de l'Ingenieur, Techniques de l'ingénieur, 2007, pp.1-9
Accès au bibtex
BibTex
auteur
Anne Bonfante, Jean-Yves Marion
titre
On the defence notion
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (4), pp.247-251. ⟨10.1007/s11416-007-0058-9⟩
DOI
DOI : 10.1007/s11416-007-0058-9
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00184985/file/bmg.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion
titre
Foreword of WTCV 06
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (1), pp.1-2. ⟨10.1007/s11416-007-0038-0⟩
DOI
DOI : 10.1007/s11416-007-0038-0
Accès au bibtex
BibTex
auteur
Mohamed Salah Bouassida, Najah Chridi, Isabelle Chrisment, Olivier Festor, Laurent Vigneron
titre
Automated Verification of a Key Management Architecture for Hierarchical Group Protocols
article
Annals of Telecommunications - annales des télécommunications, Springer, 2007, 62 (11-12), pp.1365-1387
Accès au bibtex
BibTex
auteur
Olivier Bournez, Manuel L. Campagnolo, Daniel S. Graça, Emmanuel Hainry
titre
Polynomial differential equations compute all real computable functions on computable compact intervals
article
Journal of Complexity, Elsevier, 2007, 23 (3), pp.317--335
Accès au texte intégral et bibtex
https://hal-polytechnique.archives-ouvertes.fr/inria-00102947/file/JOC.pdf BibTex
auteur
Dominique Cansell, Dominique Méry
titre
Incremental Parametric Development of Greedy Algorithms
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2007, roceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), 185, pp.47-62. ⟨10.1016/j.entcs.2007.05.028⟩
DOI
DOI : 10.1016/j.entcs.2007.05.028
Accès au bibtex
BibTex
auteur
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
titre
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
article
Journal of Automated Reasoning, Springer Verlag, 2007, Journal of Automated Reasoning, 39 (1), pp.1-47. ⟨10.1007/s10817-006-9061-y⟩
DOI
DOI : 10.1007/s10817-006-9061-y
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01148347/file/2007-jar-07.pdf BibTex
auteur
Thierry Coquand, Arnaud Spiwack
titre
A Proof of Strong Normalisation Using Domain Theory
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 16 p. ⟨10.2168/LMCS-3(4:12)2007⟩
DOI
DOI : 10.2168/LMCS-3(4:12)2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432448/file/sn4.pdf BibTex
auteur
Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu
titre
Relating two standard notions of secrecy
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 3 (3, paper 2), pp.1-29. ⟨10.2168/LMCS-3(3:2)2007⟩
DOI
DOI : 10.2168/LMCS-3(3:2)2007
Accès au bibtex
BibTex
auteur
Eric Filiol, Jean-Yves Marion
titre
La virologie informatique - les virus, ennemis utiles
article
Pour la science, Pour la science, 2007, pp.60-64
Accès au bibtex
BibTex
auteur
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
titre
Decision procedures for extensions of the theory of arrays
article
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2007, 50 (3-4), pp.231-254. ⟨10.1007/s10472-007-9078-x⟩
DOI
DOI : 10.1007/s10472-007-9078-x
Accès au bibtex
BibTex
auteur
Matthieu Kaczmarek
titre
ELF et virologie informatique
article
GNU Linux Magasine France, DIAMOND EDITIONS, 2007, Septembre - Octobre, pp.12--19
Accès au bibtex
BibTex
auteur
Fairouz Kamareddine, Karim Nour
titre
A completeness result for a realisability semantics for an intersection type system
article
Annals of Pure and Applied Logic, Elsevier Masson, 2007, 146, pp.180-198
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00380177/file/general7.pdf BibTex
auteur
Eunyoung Kang, Stephan Merz
titre
Predicate Diagrams for the Verification of Real-Time Systems
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.401-413. ⟨10.1007/s00165-007-0030-y⟩
DOI
DOI : 10.1007/s00165-007-0030-y
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00112065/file/0819.pdf BibTex
auteur
Dominique Larchey-Wendling
titre
Graph-based decision for Gödel-Dummett logics
article
Journal of Automated Reasoning, Springer Verlag, 2007, 38 (1-3), pp.201-225. ⟨10.1007/s10817-006-9047-9⟩
DOI
DOI : 10.1007/s10817-006-9047-9
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00105564/file/larchey_final.pdf BibTex
auteur
Thierry Lecomte, Dominique Méry, Dominique Cansell
titre
Patrons de conception prouvés
article
Génie Logiciel - Magazine de l'ingéniérie du logiciel et des systèmes, GL & IS - 8, rue du Parc - 92190 MEUDON, 2007, Ingénierie dirigée par les modèles, pp.14-18
Accès au bibtex
BibTex
auteur
Dominique Méry, Stephan Merz
titre
Specification and Refinement of Access Control
article
Journal of Universal Computer Science, Springer, 2007, 13 (8), pp.1073-1093
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
A complex drawing in descriptive geometry
article
Tugboat, TeX Users Group, 2007, 28 (2), pp.218-228
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Sphères, grands cercles et parallèles
article
Cahiers Gutenberg, Association GUTenberg, 2007, Avril 2007 (48), pp.7-22
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Review of ``Mathematical Illustrations: A Manual of Geometry and PostScript
article
Notices of the American Mathematical Society, American Mathematical Society, 2007, 54 (1), pp.38-42
Accès au bibtex
BibTex
auteur
Benjamin Werner
titre
Preuves formelles, preuves calculatoires
article
Interstices, INRIA, 2007, ⟨https://interstices.info/jcms/c_23115/preuves-formelles-preuves-calculatoires⟩
Accès au bibtex
BibTex

2006

auteur
Michael Backes, Anupam Datta, Ante Derek, John C. Mitchell, Mathieu Turuani
titre
Compositional Analysis of Contract Signing Protocols
article
Theoretical Computer Science, Elsevier, 2006, Theoretical Computer Science
Accès au bibtex
BibTex
auteur
Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion
titre
On Abstract Computer Virology from a Recursion-theoretic Perspective
article
Journal in Computer Virology, Springer Verlag, 2006, 1 (3-4), pp.45--54. ⟨10.1007/s11416-005-0007-4⟩
DOI
DOI : 10.1007/s11416-005-0007-4
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00115199/file/jcv06.pdf BibTex
auteur
Dominique Cansell, Dominique Méry
titre
Formal and Incremental Construction of Distributed Algorithms: On the Distributed Reference Counting Algorithm
article
Theoretical Computer Science, Elsevier, 2006
Accès au bibtex
BibTex
auteur
Samir Chouali, Maritta Heisel, Jeanine Souquières
titre
Proving Component Interoperability with B Refinement
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2006, 160, pp.157-172
Accès au bibtex
BibTex
auteur
Najah Chridi, Laurent Vigneron
titre
Sécurité des communications de groupe
article
La Revue de l'Electricité et de l'Electronique, Société de l'Électricité, de l'Électronique et des Technologies de l'Information et de la Communication, 2006, Risques et sécurité des réseaux et des systèmes à composante logicielle, pp.51-60
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Protocoles cryptographiques : analyse par méthodes formelles
article
Techniques de l'Ingenieur, Techniques de l'ingénieur, 2006
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Ces protocoles qui nous protègent
article
Tangente, Editions Pole, 2006
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Divers protocoles couramment utilisés en informatique
article
Tangente, Editions Pole, 2006
Accès au bibtex
BibTex
auteur
Véronique Cortier, Martin Abadi
titre
Deciding knowledge in security protocols under equational theories.
article
Theoretical Computer Science, Elsevier, 2006, 367 (1-2), pp.2-32
Accès au bibtex
BibTex
auteur
Véronique Cortier, Stéphanie Delaune, Pascal Lafourcade
titre
A Survey of Algebraic Properties Used in Cryptographic Protocols
article
Journal of Computer Security, IOS Press, 2006, 14 (1), pp.1-43
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000552/file/surveyCDL.pdf BibTex
auteur
Véronique Cortier, Xavier Goaoc, Mira Lee, Na Hyeon-Suk
titre
A note on maximally repeated sub-patterns of a point set
article
Discrete Mathematics, Elsevier, 2006, 306 (16), pp.1965-1968
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00097239/file/Repeated-sub-patterns.pdf BibTex
auteur
Gilles Dowek
titre
L’engagement des scientifiques
article
Interstices, INRIA, 2006, ⟨https://interstices.info/jcms/c_19051/l-engagement-des-scientifiques⟩
Accès au bibtex
BibTex
auteur
Abdessamad Imine, Michaël Rusinowitch, Gérald Oster, Pascal Molli
titre
Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence
article
Theoretical Computer Science, Elsevier, 2006, Algebraic Methodology and Software Technology, 351 (2), pp.167--183. ⟨10.1016/j.tcs.2005.09.066⟩
DOI
DOI : 10.1016/j.tcs.2005.09.066
Accès au bibtex
BibTex
auteur
Alexander Knapp, Stephan Merz, Martin Wirsing, Julia Zappe
titre
Specification and Refinement of Mobile Systems in MTLA and Mobile UML
article
Theoretical Computer Science, Elsevier, 2006, 351 (2), pp.184--202
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000754/file/final.pdf BibTex
auteur
Jean-Yves Marion, Anne Bonfante
titre
Les paradoxes de la défense virale : Le cas bradley
article
MISC - Le journal de la sécurité informatique, Lavoisier, 2006, 28, pp.4-7
Accès au bibtex
BibTex
auteur
Ninh Thuan Truong, Jeanine Souquières
titre
Verification of UML Model Elements Using B
article
Journal of Information Science and Engineering, Academia Sinica, 2006, 22, pp.357-373
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00097566/file/main.pdf BibTex

2005

auteur
Jean-Raymond Abrial, Dominique Cansell
titre
Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity)
article
Journal of Universal Computer Science, Springer, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770
Accès au bibtex
BibTex
auteur
Philippe Cabon, R. Rumin, J.Y. Salaün, Smail Triki, H. Des Abbayes
titre
Formation of anionic trifunctionalized metallalactones by nucleophilic addition at the β-carbonyl of a pyruvoyl ligand
article
Organometallics, 2005, 24 (7), pp.1709-1717. ⟨10.1021/om049030r⟩
DOI
DOI : 10.1021/om049030r
Accès au bibtex
BibTex
auteur
Dominique Cansell, Dominique Méry, Cyril Proch
titre
Un système d'analyse de la qualité: de la norme au produit en passant par le raffinement
article
Génie logiciel, C & S, 2005, pp.44-50
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000196/file/NeptuneCansellMeryProch.pdf BibTex
auteur
Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani
titre
An NP Decision Procedure for Protocol Insecurity with XOR
article
Theoretical Computer Science, Elsevier, 2005, Theoretical Computer Science, 338 (1-3), pp.247-274
Accès au bibtex
BibTex
auteur
Hubert Comon-Lundh, Véronique Cortier
titre
Tree automata with one memory, set constraints and cryptographic protocols
article
Theoretical Computer Science, Elsevier, 2005, 331 (1), pp.143-214
Accès au bibtex
BibTex
auteur
Véronique Cortier
titre
Vérifier les protocoles cryptographiques
article
Techniques et Sciences Informatiquess, Editions Hermès, 2005
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Méry, David Pym
titre
The semantics of BI and resource tableaux
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2005, 15, pp.1033-1088
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Mery
titre
Resource Graphs and Countermodels in Resource Logics
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2005, 125, pp.117-135
Accès au bibtex
BibTex
auteur
Tom Hirschowitz, Xavier Leroy
titre
Mixin modules in a call-by-value setting
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2005, 27 (5), pp.857 - 881. ⟨10.1145/1086642.1086644⟩
DOI
DOI : 10.1145/1086642.1086644
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310317/file/cmsv-long.pdf BibTex
auteur
Dominique Larchey-Wendling
titre
Gödel-Dummett counter-models through matrix computation
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2005, 125 (3), pp.12. ⟨10.1016/j.entcs.2004.07.022⟩
DOI
DOI : 10.1016/j.entcs.2004.07.022
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00008810/file/ENTCS2004.pdf BibTex
auteur
Dominique Méry, Dominique Cansell, Cyril Proch, Denis Abraham, Patrick Ditsch
titre
The challenge of QoS for digital television services
article
EBU Technical Review, European Broadcasting Union, 2005, 302 (Avril), 11 p
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Kissing Circles: A French Romance in METAPOST
article
Tugboat, TeX Users Group, 2005, 26 (1), pp.10-17
Accès au bibtex
BibTex

2004

auteur
Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch
titre
On the Fly Pattern Matching For Intrusion Detection with Snort
article
Annals of Telecommunications - annales des télécommunications, Springer, 2004, 59 (9-10), pp.941--967
Accès au bibtex
BibTex
auteur
Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch
titre
Unification Modulo ACUI Plus Distributivity Axioms
article
Journal of Automated Reasoning, Springer Verlag, 2004, 33 (1), pp.1-28
Accès au bibtex
BibTex
auteur
Dominique Cansell, Stefan Hallerstede, Yann Zimmermann
titre
Construction sûre de systèmes électroniques
article
Génie logiciel, C & S, 2004, pp.38-44
Accès au bibtex
BibTex
auteur
Yannick Chevalier, Laurent Vigneron
titre
Strategy for Verifying Security Protocols with Unbounded Message Size
article
Journal of Automated Software Engineering, Springer, 2004, 11 (2), pp.141-166
Accès au bibtex
BibTex
auteur
Hubert Comon-Lundh, Véronique Cortier
titre
Security properties: two agents are sufficient
article
Science of Computer Programming, Elsevier, 2004, 50 (1-3), pp.51-71
Accès au bibtex
BibTex
auteur
Dieu Donné Okalas Ossami, Jeanine Souquières, Jean-Pierre Jacquot
titre
Concepts importants à la construction de spécifications multi-vues UML et B
article
Informations, Savoirs, Décisions et Médiations [Informations, Sciences for Decisions Making ] , Laboratoire I3M - EA3820, Université du Sud Toulon-Var, 2004, 14 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107756/file/A04-R-004.pdf BibTex

2003

auteur
Dominique Cansell, Dominique Méry
titre
Foundations of the B method
article
Computers and Informatics, 2003, 22, 31 p
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Méry
titre
Semantic Labelled Tableaux for propositional BI (without bottom)
article
Journal of Logic and Computation, Oxford University Press (OUP), 2003, 13 (5), pp.707-753
Accès au bibtex
BibTex
auteur
François Laroussinie, Philippe Schnoebelen, Mathieu Turuani
titre
On the expressivity and complexity of quantitative branching-time temporal logics.
article
Theoretical Computer Science, Elsevier, 2003, Theoretical Computer Science, 1-3 (297), pp.297-315. ⟨10.1016/S0304-3975(02)00644-8⟩
DOI
DOI : 10.1016/S0304-3975(02)00644-8
Accès au bibtex
BibTex
auteur
Luigi Liquori
titre
Review: Formal Methods for Open Object-Based Distributed Systems V
article
The Computer Journal, Oxford University Press (UK), 2003, 46 (6), pp.661. ⟨10.1093/comjnl/46.6.661⟩
DOI
DOI : 10.1093/comjnl/46.6.661
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01149616/file/2003-tcj-book-review.pdf BibTex
auteur
Stephan Merz
titre
On the Logic of TLA+
article
Computers and Informatics, 2003, 22 (4), 27 p
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Solving Layout Problems Concurrently With TeX and Java
article
Tugboat, TeX Users Group, 2003, 8 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107696/file/A03-R-251.pdf BibTex
auteur
Michaël Rusinowitch, Mathieu Turuani
titre
Protocol insecurity with a finite number of sessions, composed keys is NP-complete.
article
Theoretical Computer Science, Elsevier, 2003, Theoretical Computer Science, 1-3 (299), pp.451-475. ⟨10.1016/S0304-3975(02)00490-5⟩
DOI
DOI : 10.1016/S0304-3975(02)00490-5
Accès au bibtex
BibTex

2001

auteur
Dominique Colnet, Olivier Zendra
titre
Global system analysis at work
article
Journal of Object Oriented Programming, 2001, 14 (1), pp.10--13
Accès au bibtex
BibTex
auteur
Didier Galmiche, Jean-Marie Notin
titre
Proof-search and Proof nets in Mixed Linear Logic
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2001, 37, pp.1-33
Accès au bibtex
BibTex

2000

auteur
Jean-Pierre Finance
titre
Entre rétrospective et prospective
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2000, 19 (1-2-3), pp.11-17
Accès au bibtex
BibTex
auteur
Didier Galmiche
titre
Connection Methods in Linear Logic and Proof nets Construction
article
Theoretical Computer Science, Elsevier, 2000, 232 (1-2), pp.231-272
Accès au bibtex
BibTex
auteur
Didier Galmiche, David Pym
titre
Proof-search in Type-theoretic Languages: An Introduction
article
Theoretical Computer Science, Elsevier, 2000, 232 (1-2), pp.5-53
Accès au bibtex
BibTex
auteur
Didier Galmiche, Dominique Larchey-Wendling
titre
Quantales as completions of ordered monoids: revised semantics for Intuitionistic Linear Logic
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2000, 35, 15 p
Accès au bibtex
BibTex

1999

auteur
Didier Galmiche, Giorgio Delzanno, Maurizio Martelli
titre
A Specification Logic for Concurrent Object-oriented Programming
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 1999, 9 (3), pp.253-286
Accès au bibtex
BibTex
auteur
Maritta Heisel, Jeanine Souquières
titre
De l'élicitation des besoins à la spécification formelle
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 1999, 18 (7), pp.777-801
Accès au bibtex
BibTex

1998

auteur
Didier Galmiche
titre
Connection proof search methods in Linear Logic and proof nets construction
article
Theoretical Computer Science, Elsevier, 1998, 30 p
Accès au bibtex
BibTex
auteur
Didier Galmiche, Dominique Larchey-Wendling
titre
Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets - extended abstract
article
Electronic Notes in Theoretical Computer Science, Elsevier, 1998, 17, pp.1-18
Accès au bibtex
BibTex
auteur
Didier Galmiche, Bruno Martin
titre
Proof nets Construction and Automated Deduction in Non-commutative Linear Logic - extended abstract
article
Electronic Notes in Theoretical Computer Science, Elsevier, 1998, 17, pp.1-20
Accès au bibtex
BibTex
auteur
Thomas Lambolais, Nicole Lévy, Jeanine Souquières
titre
Assistance au développement de spécifications de protocoles de communication
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 1998, 17 (9), pp.1061-1082
Accès au bibtex
BibTex

1997

auteur
Saleck Ould Mohammed, P. Bertuzzi, Ary Bruand, L. Raison, L. Bruckler
titre
Field Evaluation and Error Analysis of Soil Water Content Measurement using the Capacitance Probe Method
article
Soil Science Society of America, 1997, 61 (2), pp.399-408. ⟨10.2136/sssaj1997.03615995006100020006x⟩
DOI
DOI : 10.2136/sssaj1997.03615995006100020006x
Accès au bibtex
BibTex
auteur
Saleck Ould Mohammed, Ary Bruand, L. Bruckler, P. Bertuzzi, Bernard Guillet, L. Raison
titre
Estimating Long-Term Drainage at a Regional Scale Using a Deterministic Model
article
Soil Science Society of America Journal, Soil Science Society of America, 1997, 61 (5), pp.1473-1482. ⟨10.2136/sssaj1997.03615995006100050027x⟩
DOI
DOI : 10.2136/sssaj1997.03615995006100050027x
Accès au bibtex
BibTex

1992

auteur
Ary Bruand, Daniel Zimmer
titre
Relation entre la capacité d'échange cationique et le volume poral dans les sols argileux : incidences sur la morphologie de la phase argileuse à l'échelle des assemblages élémentaires
article
Comptes Rendus de l'Academie des Sciences Serie II, 1992, 315, pp.223-229
Accès au texte intégral et bibtex
https://hal-insu.archives-ouvertes.fr/insu-00862646/file/Bruand-1992-2CRAS.pdf BibTex
auteur
Ary Bruand, Saleck Ould Mohammed, Marcello Pagliai, Jean-Claude Begon
titre
Modifications structurales (assemblage élémentaire) liées à l'activité racinaire au sein de sols limono-argileux
article
Comptes rendus de l’Académie des sciences. Série IIa, Sciences de la terre et des planètes, Elsevier, 1992, 315, pp.757-764
Accès au texte intégral et bibtex
https://hal-insu.archives-ouvertes.fr/insu-00862447/file/Bruand-CRAS-1992-1.pdf BibTex

1990

auteur
J.C. Fiès, Ary Bruand
titre
Textural porosity analysis of a silty clay soil using pore volume balance estimation, mercury porosimetry and quantified backscattered electron scanning image (BESI)
article
Geoderma, Elsevier, 1990, 47 (3-4), pp.209-219. ⟨10.1016/0016-7061(90)90029-9⟩
DOI
DOI : 10.1016/0016-7061(90)90029-9
Accès au bibtex
BibTex

1988

auteur
Ary Bruand, Daniel Tessier, Denis Baize
titre
Contribution à l'étude des propriétés de rétention en eau des sols argileux : importance de la prise en compte de l'organisation de la phase argileuse.
article
Comptes rendus de l’Académie des sciences. Série IIa, Sciences de la terre et des planètes, Elsevier, 1988, 307, pp.1937-1941
Accès au texte intégral et bibtex
https://hal-insu.archives-ouvertes.fr/insu-00862570/file/Bruand-CRAS-1988.pdf BibTex

1984

auteur
Pierre Arpin, Jean-François Ponge, Bernard Dabin, Auguste Mori
titre
Utilisation des nématodes Mononchida et des collemboles pour caractériser des phénomènes pédobiologiques
article
Revue d'Ecologie et de Biologie du Sol, 1984, 21 (2), pp.243-268
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00507055/file/Arpin_et_al._1984.pdf BibTex

1976

auteur
Abdallah Droubi, Philippe Vieillard, Guilhem Bourrie, Bertrand Fritz, Yves Tardy
titre
Etude théorique de l'altération des plagioclases. Bilans et conditions de stabilité des minéraux secondaires en fonction de la pression partielle de CO2 et de la température (0 °C à 100 °C)
article
Sciences Géologiques Bulletin, 1976, 29 (1), pp.45-62
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01189767/file/Droubi_1976001_%7BC74286F9-6D6D-4948-98D2-B5D6604E2BAC%7D.pdf BibTex