Publications HAL du labo/EPI 206041;2357;140234;23092;107895

2019

titre
Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques
auteur
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat
article
Journal of Symbolic Computation, Elsevier, 2019, 90 (3--41)
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01590654/file/paper.pdf BibTex

2018

titre
HOπ in Coq
auteur
Sergueï Lenglet, Alan Schmitt
article
CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, 2018, 〈10.1145/3167083〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01614987/file/cpp18.pdf BibTex
titre
Revisiting Enumerative Instantiation
auteur
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
article
[Research Report] University of Iowa; Inria. 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01744956/file/rep.pdf BibTex
titre
A Machine-Checked Correctness Proof for Pastry
auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
article
Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. 〈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
titre
Encoding TLA+ into unsorted and many-sorted first-order logic
auteur
Stephan Merz, Hernán Vanzetto
article
Science of Computer Programming, Elsevier, 2018, 158, pp.3-20. 〈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
titre
SIAMESE-RELATED1 is regulated post-translationally and participates in repression of leaf growth under moderate drought.
auteur
Marieke Dubois, Katia Selden, Alexis Bediee, Gaelle Rolland, Nicolas Baumberger, Sandra Noir, Lien Bach, Geneviève Lamy, Christine Granier, Pascal Genschik
article
plant physiology, 2018, 〈10.1104/pp.17.01712〉
Accès au bibtex
BibTex
titre
Analyse comparative d’une activité d’apprentissage de la programmation en mode branché et débranché
auteur
Margarida Romero, Benjamin Lille, Thierry Viéville, Marie Duflot-Kremer, Cindy De Smet, David Belhassein
article
Educode - Conférence internationale sur l'enseignement au numérique et par le numérique, Aug 2018, Bruxelles, France. 2018, 〈https://educode.be/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01861732/file/Educode%20_UnPlugged-CDS06_soumis.pdf BibTex
titre
On the Importance of Explicit Domain Modelling in Refinement-Based Modelling Design. Experiments with Event-B
auteur
Yamine Ait Ameur, Idir Ait-Sadoune, Pierre Castéran, J. Paul Gibson, Kahina Hacid, Souad Kherroubi, Dominique Mery, Linda Mohand Oussaid, Neeraj Kumar Singh, Laurent Voisin
article
Michael Butler; Alexander Raschke; Thai Son Hoang; Klaus Reichl. ABZ 2018 - 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Jun 2018, Southampton, United Kingdom. Springer, 10817, pp.425--430, 2018, Lecture Notes in Computer Science. 〈https://link.springer.com/chapter/10.1007/978-3-319-91271-4_35〉. 〈10.1007/978-3-319-91271-4_35〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01797538/file/AmeurACGHKMMSV18-1.pdf BibTex
titre
Extracting Symbolic Transitions from $TLA+$ Specifications
auteur
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
article
Michael Butler; Alexander Raschke; Thai Son Hoang; Klaus Reichl. Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018, Jun 2018, Southampton, United Kingdom. 10817, pp.89-104, Lecture Notes in Computer Science. 〈https://www.southampton.ac.uk/abz2018/index.page〉. 〈10.1007/978-3-319-91271-4_7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01871131/file/camera.pdf BibTex
titre
Reachability in Parameterized Systems: All Flavors of Threshold Automata
auteur
Jure Kukovec, Igor Konnov, Josef Widder
article
CONCUR 2018 - 29th International Conference on Concurrency Theory, Sep 2018, Beijing, China. 〈10.4230/LIPIcs.CONCUR.2018.19〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01871142/file/LIPIcs-CONCUR-2018-19.pdf BibTex
titre
Positive Solutions of Systems of Signed Parametric Polynomial Inequalities
auteur
Hoon Hong, Thomas Sturm
article
CASC 2018 - International Workshop on Computer Algebra in Scientific Computing, Sep 2018, Lille, France. 11077, pp.238 - 253, 2018, LNCS. 〈10.1007/978-3-319-99639-4_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01889827/file/Hong-Sturm2018_Chapter_PositiveSolutionsOfSystemsOfSi.pdf BibTex
titre
Thirty Years of Virtual Substitution
auteur
Thomas Sturm
article
Proc. ISSAC 2018, Jul 2018, New York, United States. 18, 2018, 〈10.1145/3208976.3209030〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01889817/file/p11-sturm.pdf BibTex
titre
Revisiting Enumerative Instantiation
auteur
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
article
TACAS 2018 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2018, Thessaloniki, Greece
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01877055/file/conf.pdf BibTex
titre
Validating Back-links of FOLID Cyclic Pre-proofs
auteur
Sorin Stratulat
article
CL&C'18 - Seventh International Workshop on Classical Logic and Computation, Jul 2018, Oxford, United Kingdom. Electronic Proceedings in Theoretical Computer Science, 15 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01883826/file/Str__2018.pdf BibTex
titre
Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
auteur
Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
article
Automated Verification of Critical Systems (AVOCS 2018), Jul 2018, Oxford, United Kingdom
Accès au bibtex
BibTex
titre
Generation of SDN policies for protecting android environments based on automata learning
auteur
Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
article
NOMS 2018 - 2018 IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, France. IEEE, 〈10.1109/NOMS.2018.8406153〉
Accès au bibtex
BibTex
titre
Synaptic: A formal checker for SDN-based security policies
auteur
Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
article
NOMS 2018 - 2018 IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, France. IEEE, 〈10.1109/NOMS.2018.8406122〉
Accès au bibtex
BibTex

2017

titre
Virtual Environments Integrative Design - from Human in-the-Loop to Bio-Cyber-Physical-Systems
auteur
Didier Fass, Franck Gechter
article
AHFE 2017 - 8th International Conference on Applied Human Factors and Ergonomics, Jul 2017, Los Angeles, United States
Accès au bibtex
BibTex
titre
Transportation of Goods in Inner-City Centers: Can Autonomous Vehicles in Platoon Be a Suitable Solution?
auteur
Franck Gechter, El-Hassane Aglzim, Sidi Mohammed Senouci, Nathalie Rodet-Kroichvili, Cindy Cappelle, Didier Fass
article
IEEE Vehicle Power and Propulsion Conference, 2017, Belfort, France
Accès au bibtex
BibTex
titre
Scalable Fine-Grained Proofs for Formula Processing
auteur
Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine
article
[Research Report] Universite de Lorraine, CNRS, Inria, LORIA, Nancy, France; Universidade Federal do Rio Grande do Norte, Natal, Brazil; Vrije Universiteit Amsterdam, Amsterdam, The Netherlands; Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2017, pp.25
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01526841/file/rep.pdf BibTex
titre
Satisfiability Modulo Bounded Checking
auteur
Simon Cruanes
article
International Conference on Automated Deduction (CADE), Aug 2017, Gothenburg, Sweden. 26, pp.114-129, 2017, 〈10.1007/978-3-319-63046-5_8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01572531/file/paper.pdf BibTex
titre
Applying a Dependency Mechanism for Voting Protocol Models Using Event-B
auteur
Paul Gibson, Souad Kherroubi, Dominique Méry
article
Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2017), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.124-138, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_9〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658423/file/446833_1_En_9_Chapter.pdf BibTex
titre
Virtual Environments Integrative Design – From Human-in-the-Loop to Bio-Cyber-Physical Systems
auteur
Didier Fass, Franck Gechter
article
France. Springer International Publishing, 2017
Accès au bibtex
BibTex
titre
Automated Verification of Security Chains in Software-Defined Networks with Synaptic
auteur
Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
article
NetSoft 2017 - IEEE Conference on Network Softwarization, Jul 2017, Bologna, Italy. IEEE Computer Society, 9pp., 2017, 〈10.1109/NETSOFT.2017.8004195〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630806/file/camera-ready.pdf BibTex
titre
Satisfiability techniques for computing minimal tie sets in reliability assessment
auteur
Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
article
10th International Conference on Mathematical Methods in Reliability, MMR 2017, Jul 2017, Grenoble, France. pp.1-8, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630851/file/resubmission-Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf BibTex
titre
Contextualization and Dependency in State-Based Modelling - Application to Event-B
auteur
Souad Kherroubi, Dominique Méry
article
MEDI 2017 - International Conference on Model and Data Engineering, Oct 2017, Barcelona, Spain. Springer, 10563, pp.137--152, 2017, Lecture Notes in Computer Science. 〈http://dblp.org/rec/bib/conf/medi/KherroubiM17〉. 〈10.1007/978-3-319-66854-3_11〉
Accès au bibtex
BibTex
titre
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
auteur
Andreas Teucke, Christoph Weidenbach
article
de Moura, Leonardo. CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, Lecture Notes in Computer Science, 10395, pp.202-219, 2017, CADE 2017: Automated Deduction – CADE 26. 〈10.1007/978-3-319-63046-5_13〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01657026/file/authorcopy.pdf BibTex
titre
A Case Study on the Parametric Occurrence of Multiple Steady States
auteur
Russell Bradford, James Davenport, Matthew England, Hassan Errami, Vladimir Gerdt, Dima Grigoriev, Charles Hoyt, Marek Košta, Ovidiu Radulescu, Thomas Sturm, Andreas Weber
article
ISSAC 2017 - International Symposium on Symbolic and Algebraic Computation, Jul 2017, Kaiserslautern, Germany. ACM, pp.45-52, 〈10.1145/3087604.3087622〉
Accès au bibtex
BibTex
titre
Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
auteur
Matthew England, Hassan Errami, Dima Grigoriev, Ovidiu Radulescu, Thomas Sturm, Andreas Weber
article
Vladimir P. Gerdt; Wolfram Koepf; Werner M. Seiler; Evgenii V. Vorozhtsov. CASC 2017 - 19th International Workshop on Computer Algebra in Scientific Computing, Sep 2017, Beijing, China. Springer, 10490, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-66320-3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01648691/file/10.1007-978-3-319-66320-3_8.pdf BibTex
titre
Subtropical Satisfiability
auteur
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Vu
article
Clare Dixon; Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-319-66167-4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590899/file/10.1007-978-3-319-66167-4_11.pdf BibTex
titre
What did Napier invent?
auteur
Denis Roegel
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01465278/file/napier400introduction.pdf BibTex
titre
Satisfiability techniques for computing minimal tie sets in reliability assessment
auteur
Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
article
ISET. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01518920/file/Techreport%20-%20Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf BibTex
titre
Evaluation de la robustesse d'un ordonnancement par Automates Temporisés Stochastiques
auteur
Sara Himmiche, Pascale Marangé, Alexis Aubry, Marie Duflot, Jean-François Pétin
article
11ème Colloque sur la Modélisation des Systèmes Réactifs, MSR 2017, Nov 2017, Marseille, France. 〈http://www.lsis.org/msr2017〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652138/file/himmiche-al-msr2017-final.pdf BibTex
titre
Using statistical-model-checking-based simulation for evaluating the robustness of a production schedule
auteur
Sara Himmiche, Alexis Aubry, Pascale Marangé, Jean-François Pétin, Marie Duflot
article
7th Workshop on Service Orientation in Holonic and Multi-Agent Manufacturing, SOHOMA'17, Oct 2017, Nantes, France. 2017, 〈https://sohoma17.sciencesconf.org/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652140/file/Himmiche_et_al_Sohoma2017_vf.pdf BibTex
titre
Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
auteur
Dominique Méry, Mike Poppleton
article
Software and Systems Modeling (SoSyM), Springer, 2017, 16 (4), pp.1083--1115
Accès au bibtex
BibTex
titre
Before Torchi and Schwilgué, there was White
auteur
Denis Roegel
article
ComputingEdge, IEEE Computer Society, 2017, pp.42-43. 〈https://www.computer.org/web/computingedge〉
Accès au bibtex
BibTex
titre
Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
auteur
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
article
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Apr 2017, Uppsala, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599167/file/conf.pdf BibTex
titre
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
auteur
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
article
FSCD 2017: 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. 11, pp.1 - 11, 〈10.4230/LIPIcs.FSCD.2017.11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599176/file/paper.pdf BibTex
titre
A Formal Proof of the Expressiveness of Deep Learning
auteur
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
article
ITP 2017: 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/3-540-48256-3_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599172/file/paper.pdf BibTex
titre
Foundational nonuniform (Co)datatypes for higher-order logic
auteur
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
article
LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005071〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599174/file/conf.pdf BibTex
titre
Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016, Limassol, Cyprus, November 8, 2016
auteur
Catherine Dubois, Paolo Masci, Dominique Méry
article
Nov 2016, Cyprus. 240, 2017, 〈10.4204/EPTCS.240〉
Accès au bibtex
BibTex
titre
Metadata of the chapter that will be visualized in SpringerLink
auteur
Didier Fass
article
8th International Conference on Applied Human Factors and Ergonomics, 2017, Los Angeles - Etats-Unis d'Amérique, Unknown Region. 2017
Accès au bibtex
BibTex
titre
Modélisation & Intégration du système
auteur
Didier Fass
article
5th European workshop on surgical simulation, Nancy, 12-30 June 2017, 2017, Nancy -, Unknown Region. 2017
Accès au bibtex
BibTex
titre
Transportation of goods in inner-city centers : can autonomous vehicles in platoon be a suitable solution
auteur
Franck Gechter, Didier Fass
article
IEEE-VPPC 2017, 2017, Belfort -, Unknown Region. 2017
Accès au bibtex
BibTex
titre
Auxiliary Variables in TLA+
auteur
Leslie Lamport, Stephan Merz
article
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01488617/file/auxiliary.pdf BibTex
titre
Scalable Fine-Grained Proofs for Formula Processing
auteur
Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine
article
Leonardo de Moura. Proc. Conference on Automated Deduction (CADE), 2017, Gotenburg, Sweden. Springer, 10395, pp.398 - 412, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02959-2_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590922/file/Barbosa2.pdf BibTex
titre
New techniques for instantiation and proof production in SMT solving
auteur
Haniel Barbosa
article
Artificial Intelligence [cs.AI]. Université de Lorraine, 2017. English. 〈NNT : 2017LORR0091〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01591108/file/DDOC_T_2017_0091_MOREIRA_BARBOSA.pdf BibTex
titre
Congruence Closure with Free Variables
auteur
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
article
Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2017, Uppsala, Sweden. 205, pp.220 - 230, 2017, 〈10.1007/10721959_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590918/file/Barbosa1.pdf BibTex
titre
Superposition: Types and Induction
auteur
Daniel Wand
article
Computer Science [cs]. Saarland University, 2017. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01592497/file/thesis_wand.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
auteur
Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach
article
Carles Sierra. 26th International Joint Conference on Artificial Intelligence, Aug 2017, Melbourne, Australia. pp.4786-4790, 〈10.24963/ijcai.2017/667〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592164/file/BlanchetteFleuryWeidenbachIJCAI.pdf BibTex
titre
The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable
auteur
Marco Voigt
article
Clare Dixon and Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.244-261, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592169/file/VoigtFroCoS.pdf BibTex
titre
Congruence Closure with Free Variables
auteur
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
article
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01442691/file/main.pdf BibTex
titre
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
auteur
Heiko Becker, Jasmin Blanchette, Uwe Waldmann, Daniel Wand
article
Leonardo de Moura. CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.432-453, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592186/file/BeckerBlanchetteWaldmannWandCADE.pdf BibTex
titre
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
auteur
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
article
Clare Dixon and Marcelo Finger. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.3-21, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592196/file/BiendarraBlanchetteEtAl-FroCos.pdf BibTex
titre
On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic
auteur
Matthias Horbach, Marco Voigt, Christoph Weidenbach
article
Leonardo de Moura. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.77-94, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_6〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592160/file/HorbachVoigtWeidenbachCADE.pdf BibTex
titre
A fine-grained hierarchy of hard problems in the separated fragment
auteur
Marco Voigt
article
Joël Ouaknine. LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. IEEE Computer Society, pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005094〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592172/file/VoigtLICS.pdf BibTex
titre
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
auteur
Matthias Horbach, Marco Voigt, Christoph Weidenbach
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592177/file/HorbachVoigtWeidenbachCoRR.pdf BibTex
titre
A Formal Approach for Maintaining Forest Topologies in Dynamic Networks
auteur
Faten Fakhfakh, Mohamed Tounsi, Mohamed Mosbah, Ahmed Hadj Kacem, Dominique Méry
article
ICIS 2017 - 16th IEEE/ACIS International Conference on Computer and Information Science, May 2017, Wuhan, China. 719, pp.123-137, Studies in Computational Intelligence. 〈10.1007/978-3-319-60170-0_9〉
Accès au bibtex
BibTex
titre
A Lambda-Free Higher-Order Recursive Path Order
auteur
Jasmin Blanchette, Uwe Waldmann, Daniel Wand
article
Javier Esparza and Andrzej S. Murawski. Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. Springer, 10203, pp.461-479, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-662-54458-7_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592189/file/BlanchetteWaldmannWandFoSSaCS.pdf BibTex
titre
Playing with State-Based Models for Designing Better Algorithms
auteur
Dominique Méry
article
Future Generation Computer Systems, Elsevier, 2017, 68, pp.445-455. 〈ELSEVIER〉
Accès au bibtex
BibTex
titre
New Techniques for Linear Arithmetic: Cubes and Equalities
auteur
Martin Bromberger, Christoph Weidenbach
article
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.433-461. 〈10.1007/s10703-017-0278-7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656397/file/paper.pdf BibTex
titre
Carries Stripped to the Bone: Episodes in the History of Coaxial Modular Digital Counters
auteur
Denis Roegel
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2017, 39 (3), pp.55-64. 〈http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=85〉
Accès au bibtex
BibTex
titre
Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems
auteur
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
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〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01479030/file/1705.08632v2.pdf BibTex
titre
Soundness and Completeness Proofs by Coinductive Methods
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
article
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (1), pp.149 - 179. 〈10.1007/s10817-016-9391-3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643157/file/compl.pdf BibTex
titre
Cyclic Proofs with Ordering Constraints
auteur
Sorin Stratulat
article
TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Sep 2017, Brasilia, Brazil. 12, pp.311 - 327, 2017, Automated Reasoning with Analytic Tableaux and Related Methods
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01590651/file/Str_10501_2017a.pdf BibTex
titre
A Framework for Evaluating Schedulability Analysis Tools
auteur
Lijun Shan, Susanne Graf, Sophie Quinton, Loïc Fejoz
article
Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Aug 2017, Aalborg, Denmark
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01674731/file/KimFest17.pdf BibTex
titre
A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
auteur
Thomas Sturm
article
Mathematics in Computer Science, Springer, 2017, 11 (3-4), pp.483 - 502. 〈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

titre
Intégration des savoirs et préservation des spécificités
auteur
Rémi Nazin
article
Journée Internationale des Jeunes Chercheurs 2016, Jun 2016, Nancy, France. 〈http://jijc2016.event.univ-lorraine.fr/jijc_accueil.php〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01718230/file/Article_NAZIN_Remi.pdf BibTex
titre
A Rigorous Correctness Proof for Pastry
auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.86-101, 2016, 〈10.1007/978-3-319-33600-8_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322342/file/Main.pdf BibTex
titre
Proving Determinacy of the PharOS Real-Time Operating System
auteur
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. Springer, 9675, pp.70-85, 2016, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-33600-8_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322335/file/final.pdf BibTex
titre
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
auteur
Thomas Sturm, Marco Voigt, Christoph Weidenbach
article
LICS 2016, Jul 2016, New York, United States. pp.86 - 95, 2016, 〈10.1145/2933575.2934532〉
Accès au bibtex
BibTex
titre
A note on the complexity of Bürgi's algorithm for the computation of sines
auteur
Denis Roegel
article
[Research Report] LORIA. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01284671/file/roegel2016buergi-complexity.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
auteur
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
article
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. 2016, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. 〈10.1007/978-3-319-40229-1_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01336074/file/main.pdf BibTex
titre
Interactive Theorem Proving
auteur
Jasmin Christian Blanchette, Stephan Merz
article
Nancy, France. 9807, Springer, 2016, Lecture Notes in Computer Science, 〈10.1007/978-3-319-43144-4〉
Accès au bibtex
BibTex
titre
Satisfiability Checking and Symbolic Computation
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
article
ACM Communications in Computer Algebra, Association for Computing Machinery (ACM), 2016, 50 (4), pp.145-147. 〈10.1145/3055282.3055285〉
Accès au bibtex
BibTex
titre
SC2: Satisfiability Checking Meets Symbolic Computation (Project Paper)
auteur
Thomas Sturm, Erika Ábrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler
article
Proc. CICM 2016, Jul 2016, Bialystok, Poland. pp.28 - 43, 2016, 〈10.1007/978-3-319-42547-4〉
Accès au bibtex
BibTex
titre
SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
auteur
Eriká Abrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler, Thomas Sturm
article
Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland. 〈http://www.cicm-conference.org/2016/cicm.php〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377655/file/SCSC-CICM16.pdf BibTex
titre
Compliance, Functional Safety and Fault Detection by Formal Methods
auteur
Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski
article
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016), 2016, Corfu, Greece. Springer, 9953, pp.626 - 632, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-47169-3_48〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403190/file/mypaper.pdf BibTex
titre
Fast Cube Tests for LIA Constraint Solving
auteur
Martin Bromberger, Christoph Weidenbach
article
Nicola Olivetti and Ashish Tiwari. Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. Springer, 9706, pp.116-132, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-40229-1_9〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403200/file/IJCAR2016.pdf BibTex
titre
Ordered Resolution with Straight Dismatching Constraints
auteur
Andreas Teucke, Christoph Weidenbach
article
Pascal Fontaine and Stephan Schulz and Josef Urban. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, Coimbra, Portugal. 1635, pp.95-109, 2016, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403206/file/paar.pdf BibTex
titre
Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
auteur
Martin Bromberger, Christoph Weidenbach
article
Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. 1617, pp.15-30, 2016, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403214/file/SMT2016.pdf BibTex
titre
Extending Nunchaku to Dependent Type Theory
auteur
Simon Cruanes, Jasmin Blanchette
article
Hammers for Type Theories (HaTT 2016), Jul 2016, Coimbra, Portugal. EPTCS, 210, pp.3 - 12, 2016, Proceedings First International Workshop on Hammers for Type Theories 〈http://eptcs.web.cse.unsw.edu.au/content.cgi?HaTT2016〉. 〈10.4204/EPTCS.210.3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401696/file/nunchaku_tt.pdf BibTex
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
auteur
Andrew Reynolds, Jasmin Blanchette
article
IJCAI 2016, Jul 2016, New York City, United States. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01397082/file/sister.pdf BibTex
titre
Incremental Proof-Based Development for Resilient Distributed Systems
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Trustworthy Cyber-Physical Systems Engineering, Taylor and Francis Group, 2016, Trustworthy Cyber-Physical Systems Engineering
Accès au bibtex
BibTex
titre
A reconstruction of Bauschinger and Peters's eight-place table of logarithms (volume 2, 1911)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357801/file/bauschinger1911doc.pdf BibTex
titre
A reconstruction of Bauschinger and Peters's eight-place table of logarithms (volume 1, 1910)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357798/file/bauschinger1910doc.pdf BibTex
titre
A reconstruction of Peters's table of logarithms to 7 places (1921)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357822/file/peters1921siebenstellige-doc.pdf BibTex
titre
A reconstruction of Peters’s ten-place table of logarithms (volume 1, 1922)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357823/file/peters1922zehnstellige-doc.pdf BibTex
titre
A reconstruction of Peters's table of products (1909)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357793/file/peters1909rechentafeln-doc.pdf BibTex
titre
A reconstruction of Peters's seven-place table of logarithms of trigonometric functions (1911)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357804/file/peters1911siebenstellige-doc.pdf BibTex
titre
A reconstruction of Peters's six-place table of trigonometric functions for the new division (1938)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357835/file/peters1938sechsstellige-doc.pdf BibTex
titre
A reconstruction of Peters's table of 7-place logarithms (volume 2, 1940)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357842/file/peters1940siebenstellige2-doc.pdf BibTex
titre
A reconstruction of Peters's 3-place tables (1913)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357809/file/peters1913dreistellige-doc.pdf BibTex
titre
A reconstruction of Peters's seven-place table of trigonometric functions (1918)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357811/file/peters1918siebenstellige-doc.pdf BibTex
titre
The genealogy of Johann Theodor Peters's great mathematical tables
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357846/file/roegel2016genealogy-peters.pdf BibTex
titre
A reconstruction of Peters's five-place table of logarithms of trigonometric functions (1912)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357806/file/peters1912fuenfstellige-doc.pdf BibTex
titre
A reconstruction of Peters's table of 7-place trigonometrical values for the new division(1941)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357844/file/peters1941siebenstellige-doc.pdf BibTex
titre
A reconstruction of Peters's auxiliary tables to his ten-place logarithms (1919)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357814/file/peters1919hilfstafeln-doc.pdf BibTex
titre
A reconstruction of Peters's ten-place table of logarithms (volume 2, 1919)
auteur
Denis Roegel
article
[Research Report] LORIA. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357818/file/peters1919zehnstellige-doc.pdf BibTex
titre
A reconstruction of Peters's table of logarithms to 6 places (1921)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357820/file/peters1921sechsstellige-doc.pdf BibTex
titre
A reconstruction of Peters's table of involutes (1937).
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357834/file/peters1937involutes-doc.pdf BibTex
titre
A reconstruction of Peters's table of 7-place logarithms (volume 1, 1940)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357840/file/peters1940siebenstellige1-doc.pdf BibTex
titre
A reconstruction of Peters's six-place table of trigonometric functions (1929)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357826/file/peters1929sechsstellige-doc.pdf BibTex
titre
A reconstruction of Peters's multiplication and interpolation tables (1930)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357828/file/peters1930multiplikation-doc.pdf BibTex
titre
A reconstruction of Peters's eight-place table of trigonometric functions (1939)
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357837/file/peters1939achtstellige-doc.pdf BibTex
titre
A reconstruction of Peters's six-place table of trigonometric functions for the new division (1930).
auteur
Denis Roegel
article
[Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01357831/file/peters1930sechsstellige-doc.pdf BibTex
titre
A preliminary note on Bürgi's computation of the sine of the first minute
auteur
Denis Roegel
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316358/file/roegel2016buergi-sine1minute.pdf BibTex
titre
A reconstruction of Bürgi’s sine table at 1' intervals (ca. 1587)
auteur
Denis Roegel
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316359/file/roegel2016buergi-sine-table1.pdf BibTex
titre
A tentative reconstruction of Bürgi’s sine table at 2'' intervals (ca. 1600)
auteur
Denis Roegel
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316360/file/roegel2016buergi-sine-table2.pdf BibTex
titre
Better answers to real questions
auteur
Marek Košta, Thomas Sturm, Andreas Dolzmann
article
Journal of Symbolic Computation, Elsevier, 2016, 74, pp.255 - 275. 〈10.1016/j.jsc.2015.07.002〉
Accès au bibtex
BibTex
titre
Projet de mise en place d'un cadran solaire géant sur le parvis haut de la place Thiers à Nancy
auteur
Denis Roegel
article
[Rapport de recherche] LORIA - Université de Lorraine. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01262611/file/roegel2015projet-thiers.pdf BibTex
titre
Some remarks on Bürgi’s interpolations
auteur
Denis Roegel
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316361/file/roegel2016buergi-5400-10interpolations.pdf https://hal.inria.fr/hal-01316361/file/roegel2016buergi-5400-9interpolations.pdf https://hal.inria.fr/hal-01316361/file/roegel2016buergi-interpolation2.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)
auteur
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
article
Isabellle Workshop 2016, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401807/file/sat_abs.pdf BibTex
titre
Friends with Benefits
auteur
Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
article
Isabelle Workshop 2016, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401812/file/amico_abs.pdf BibTex
titre
On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin
auteur
Dominique Méry, Rosemary Monahan, Cheng Zheng
article
Bernhard Steffen and Tiziana Margaria. ISOLA 2016 , Oct 2016, CORFU, Greece. Springer, I (9952), pp.18, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_57〉
Accès au bibtex
BibTex
titre
Making explicit domain knowledge in formal system development
auteur
Yamine Ait Ameur, Dominique Méry
article
Science of Computer Programming, Elsevier, 2016, 121 (100--127), 〈ELSEVIER〉. 〈10.1016/j.scico.2015.12.004〉
Accès au bibtex
BibTex
titre
Encoding TLA+ into Many-Sorted First-Order Logic
auteur
Stephan Merz, Hernán Vanzetto
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.54-69, 2016, 〈10.1007/978-3-319-33600-8_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322328/file/tla2smt.pdf BibTex
titre
Model Finding for Recursive Functions in SMT
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
article
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. 〈10.1007/978-3-319-40229-1_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01336082/file/conf.pdf BibTex
titre
Efficient Instantiation Techniques in SMT (Work In Progress)
auteur
Haniel Barbosa
article
PAAR 2016 - 5th Workshop on Practical Aspects of Automated Reasoning co-located with IJCAR 2016 - 8th International Joint Conference on Automated Reasoning, Jul 2016, Coimbra, Portugal. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 1635, pp.1-10, 2016, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01388976/file/paper-01.pdf BibTex
titre
Editorial
auteur
Stephan Merz, Jun Pang
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. 〈10.1007/s00165-016-0390-2〉
Accès au bibtex
BibTex
titre
Editorial
auteur
Stephan Merz, Jun Pang
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. 〈10.1007/s00165-016-0390-2〉
Accès au bibtex
BibTex
titre
A new early adding machine by Schwilgué (c. 1840?)
auteur
Denis Roegel
article
Bulletin of the Scientific Instrument Society, Scientific Instrument Society, 2016, 130, pp.24-27
Accès au bibtex
BibTex
titre
A mechanical calculator for arithmetic sequences (1844-1852): part 2, working details
auteur
Denis Roegel
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2016, 38 (1), pp.80-88. 〈http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7419814〉. 〈10.1109/MAHC.2016.3 〉
Accès au bibtex
BibTex
titre
Before Torchi and Schwilgué, there was White
auteur
Denis Roegel
article
IEEE Annals of the History of Computing, Institute of Electrical and Electronics Engineers, 2016, 38 (4), pp.92-93
Accès au bibtex
BibTex
titre
Semi-intelligible Isar Proofs from Machine-Generated Proofs
auteur
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
article
Journal of Automated Reasoning, Springer Verlag, 2016, 〈10.1007/s10817-015-9335-3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01211748/file/paper.pdf BibTex
titre
A Learning-Based Fact Selector for Isabelle/HOL
auteur
Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. 〈10.1007/s10817-016-9362-8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386986/file/paper.pdf BibTex
titre
Ensuring Correctness of Model Transformations While Remaining Decidable
auteur
Jon Haël Brenas, Rachid Echahed, Martin Strecker
article
Theoretical Aspects of Computing - ICTAC, Oct 2016, Taipei, Taiwan. pp.315 - 332, 2016, Theoretical Aspects of Computing – ICTAC 2016 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings. 〈10.1007/978-3-319-46750-4_18〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01403585/file/paper61-procversion.pdf BibTex
titre
Hammering towards QED
auteur
Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, Josef Urban
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
titre
DNA DAMAGE BINDING PROTEIN2 Shapes the DNA Methylation Landscape
auteur
Catherine Schalk, Stéphanie Drevensek, Amira Kramdi, Mohamed Kassam, Ikhlak Ahmed, Valerie Cognat, Stefanie Graindorge, Marc Bergdoll, Nicolas Baumberger, Dimitri Heintz, Chris Bowler, Pascal Genschik, Fredy Barneche, Vincent Colot, Jean Molinier
article
Plant Cell, American Society of Plant Biologists, 2016, 28 (9), pp.2043-2059. 〈10.1105/tpc.16.00474〉
Accès au bibtex
BibTex
titre
Fragile X Mental Retardation Protein (FMRP) controls diacylglycerol kinase activity in neurons
auteur
Ricardos Tabet, Enora Moutin, Jérôme Becker, Dimitri Heintz, Laetitia Fouillen, Eric Flatter, Wojciech Krężel, Violaine Alunni, Pascale Koebel, Doulaye Dembélé, Flora Tassone, Barbara Bardoni, Jean-Louis Mandel, Nicolas Vitale, Dominique Muller, Julie Le Merrer, Hervé Moine
article
Proceedings of the National Academy of Sciences of the United States of America , National Academy of Sciences, 2016, 113 (26 ), pp.E3619-E3628. 〈10.1073/pnas.1522631113 〉
Accès au bibtex
BibTex

2015

titre
Tests and Proofs
auteur
Jasmin Christian Blanchette, Nikolai Kosmatov
article
Jasmin Christian Blanchette; Nikolai Kosmatov. Tests and Proofs, Jul 2015, L’Aquila, Italy. 9154, Springer Verlag, 2015, 9783319212142. 〈10.1007/978-3-319-21215-9〉
Accès au bibtex
BibTex
titre
Jost Bürgi's skillful computation of sines
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01220160/file/roegel2015buergi-sines.pdf BibTex
titre
When sharing computer science with everyone also helps avoiding digital prejudices.
auteur
Marie Duflot, Martin Quinson, Florent Masseglia, Didier Roy, Julien Vaubourg, Thierry Viéville
article
Scratch2015AMS, Aug 2015, Amsterdam, Netherlands. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01154767/file/When%20sharing%20computer%20science%20with%20everyone%20also%20helps%20avoiding%20digital%20prejudices%20%281%29.pdf BibTex
titre
Software Component Design with the B Method — A Formalization in Isabelle/HOL
auteur
David Déharbe, Stephan Merz
article
Christiano Braga and Peter Csaba Ölveczky. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. Springer, 9539, pp.31-47, 2016, 〈10.1007/978-3-319-28934-2_2〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01305026/file/paper.pdf BibTex
titre
Modal Satisfiability via SMT Solving
auteur
Carlos Areces, Pascal Fontaine, Stephan Merz
article
Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, 〈10.1007/978-3-319-15545-6_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01127966/file/main.pdf BibTex
titre
Encoding TLA+ set theory into many-sorted first-order logic
auteur
Stephan Merz, Hernán Vanzetto
article
2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244627/file/sets2015.pdf BibTex
titre
Beagle – A Hierarchic Superposition Prover
auteur
Peter Baumgartner, Joshua Bax, Uwe Waldmann
article
Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. Springer, 9195, pp.367-377, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_25〉
Accès au bibtex
BibTex
titre
Modal Tableau Systems with Blocking and Congruence Closure
auteur
Renate Schmidt, Uwe Waldmann
article
de Nivelle, Hans. 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wroclaw, Poland. Springer, 9323, pp.38-53, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24312-2_4〉
Accès au bibtex
BibTex
titre
Analyzing Requirements Using Environment Modelling
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference, DHM 2015, Aug 2015, Los Angeles, United States. Springer, Lecture Notes in Computer Science 9185,, 2015, Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference, DHM 2015, Held as Part of HCI International 2015,. 〈http://link.springer.com/book/10.1007%2F978-3-319-21070-4〉
Accès au bibtex
BibTex
titre
Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study
auteur
Dominique Méry, Sawant Rushikesh, Anton Tarasyuk
article
Ladjel Bellatreche; Yannis Manolopoulos. Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. springer, lncs 9344, pp.89-102, 2015, Model and Data Engineering - 5th International Conference, MEDI 2015. 〈http://link.springer.com/book/10.1007%2F978-3-319-23781-7〉
Accès au bibtex
BibTex
titre
System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
auteur
Marion Guthmuller, Martin Quinson, Gabriel Corona
article
Formal Approaches to Parallel and Distributed Systems (4PAD) - Special Session of Parallel, Distributed and network-based Processing (PDP), Mar 2015, Turku, Finland. 2015
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01097204/file/paper.pdf BibTex
titre
Adapting Real Quantifier Elimination Methods for Conflict Set Computation
auteur
Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
article
Carsten Lutz; Silvio Ranise. Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. Springer, 9322, pp.151-166, 2015, LNCS. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240343/file/article.pdf BibTex
titre
Congruence Closure with Free Variables (Work in Progress)
auteur
Haniel Barbosa, Pascal Fontaine
article
Quantify 2015 : 2nd International Workshop on Quantification, 2015, Berlin, Germany. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246036/file/BarbosaFontaine-QUANTIFY2015.pdf BibTex
titre
Second International Workshop on Formal Integrated Development Environment
auteur
Catherine Dubois, Paolo Masci, Dominique Méry
article
Jun 2015, France. EPTCS, 2015, EPTCS 〈10.4204/EPTCS.187〉
Accès au bibtex
BibTex
titre
A reconstruction of Zimmermann's table of products (1889)
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246797/file/zimmermann1889rechentafel-doc.pdf BibTex
titre
A Teaching System To Learn Programming: the Programmer's Learning Machine
auteur
Martin Quinson, Gérald Oster
article
ACM Conference on Innovation and Technology in Computer Science Education 2015, Jul 2015, Vilnius, Lithuania. ACM, 〈http://www.iticse2015.mii.vu.lt/〉. 〈10.1145/2729094.2742626〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238377/file/plm-iticse-HAL.pdf BibTex
titre
Towards a Theory for Bio - Cyber Physical Systems Modelling
auteur
Didier Fass, Franck Gechter
article
HCI International 2015, Aug 2015, Los Angeles, United States. LNCS 9184, 2015, LNCS - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management: Human Modelling (Part I). 〈10.1007/978-3-319-21073-5_25〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01248069/file/FassGechter.pdf BibTex
titre
Editing ancient technical and mathematical figures: Tools and traps
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01198446/file/roegel2015editing-figures.pdf BibTex
titre
A concise yet complete description of Schwilgué's series calculator
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01198448/file/roegel2015schwilgue-concise.pdf BibTex
titre
Affordances and Safe Design of Assistance Wearable Virtual Environment of Gesture
auteur
Didier Fass
article
Tared Ahram, Waldemar Karwowski, Dylan Schmorrow. Human Factors and Egonomics (AHFE 2015), Jul 2015, Las Vegas, United States. Elsivier, Procedia Manufacturing, pp.8, 2015, 6th International Conference on Applied Human Factors and Ergonomics (AHFE 2015) and the Affiliated Conferences, AHFE 2015. 〈10.1016/j.promfg.2015.07.343〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01248046/file/FASS%20D.%20AHFE2015.pdf BibTex
titre
Better Answers to Real Questions
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
article
2015
Accès au bibtex
https://arxiv.org/pdf/1501.05098 BibTex
titre
Human Machine Epistemology Survey
auteur
Rémi Nazin, Didier Fass
article
Vincent G. Duffy. HCI Interantional 2016, Aug 2015, Los Angeles, United States. Springer, LNCS 9184, pp.12, 2015, Digital Human Modeling. Applications in Health, Safety, Ergonomics and Risk Management: Human Modeling. 〈10.1007/978-3-319-21073-5_35〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01248062/file/NAZIN%20FASS%20HCII2015.pdf BibTex
titre
Chebyshev's continuous adding machine
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01198445/file/roegel2015chebyshev.pdf BibTex
titre
Napier's bones and Genaille-Lucas's rods
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01198447/file/roegel2015genaille.pdf BibTex
titre
A new milestone: the first 7-8 places 2000 meters logarithmic slide cylinder
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01198444/file/roegel2015billeter.pdf https://hal.inria.fr/hal-01198444/file/base2000.pdf https://hal.inria.fr/hal-01198444/file/base24.pdf https://hal.inria.fr/hal-01198444/file/over2000.pdf https://hal.inria.fr/hal-01198444/file/over24.pdf BibTex
titre
{NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment
auteur
Gábor Alagi, Christoph Weidenbach
article
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), 2015, Wroclaw, Poland. Springer, Lecture Notes in Computer Science, 9322, pp.69-84, 〈10.1007/978-3-319-24246-0_5〉
Accès au bibtex
BibTex
titre
A Rewriting Approach to the Combination of Data Structures with Bridging Theories
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.275--290, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01206187/file/ds-bridging.pdf BibTex
titre
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction, CADE-25, Aug 2015, Berlin, Germany. Springer, 9195, pp.419-433, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_29〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01157898/file/bridging-nd-compact.pdf BibTex
titre
System-Level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
auteur
Marion Guthmuller, Gabriel Corona, Martin Quinson
article
2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01558049/file/journal.pdf BibTex
titre
Développement d'algorithmes répartis corrects par construction
auteur
Manamiary Bruno Andriamiarina
article
Modélisation et simulation. Université de Lorraine, 2015. Français. 〈NNT : 2015LORR0181〉
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01752149/file/these-Andriamiarina-Manamiary-Bruno.pdf BibTex
titre
Witnessing (Co)datatypes
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
article
ESOP 2015, Apr 2015, London, United Kingdom. Lecture Notes in Computer Science, 2015, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 〈10.1007/978-3-662-46669-8_15〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212587/file/wit.pdf BibTex
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
auteur
Andrew Reynolds, Jasmin Christian Blanchette
article
CADE-25, Aug 2015, Berlin, Germany. Lecture Notes in Computer Science, 2015, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. 〈10.1007/978-3-319-21401-6_13〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212585/file/conf.pdf BibTex
titre
Foundational Extensible Corecursion: A Proof Assistant Perspective
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
article
ICFP 2015, Aug 2015, Vancouver, Canada. 2015, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. 〈10.1145/2784731.2784732〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212589/file/fouco.pdf BibTex
titre
Mining the Archive of Formal Proofs
auteur
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow
article
CICM 2015, Jul 2015, Washington DC, United States. Lecture Notes in Computer Science, 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 〈10.1007/978-3-319-20615-8_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212594/file/paper.pdf BibTex
titre
Model Finding for Recursive Functions in SMT
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli
article
SMT Workshop 2015, Jul 2015, San Francisco, United States. 2015, 〈http://smt2015.csl.sri.com〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242509/file/shortv.pdf BibTex
titre
Applications of an expressive statistical model checking approach to the analysis of genetic circuits
auteur
Paolo Ballarini, Marie Duflot
article
Theoretical Computer Science, Elsevier, 2015, 599, pp.30. 〈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
titre
Congruence Closure with Free Variables (Work in Progress)
auteur
Haniel Barbosa, Pascal Fontaine
article
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France). 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01235912/file/main.pdf BibTex
titre
Linear Integer Arithmetic Revisited
auteur
Martin Bromberger, Thomas Sturm, Christoph Weidenbach
article
25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. Springer, 9195, pp.623-637
Accès au bibtex
BibTex
titre
Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
auteur
Marco Voigt, Christoph Weidenbach
article
preprint. 2015
Accès au bibtex
https://arxiv.org/pdf/1501.07209 BibTex
titre
Automated Reasoning Building Blocks
auteur
Christoph Weidenbach
article
Roland Meyer and André Platzer and Heike Wehrheim. Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog, 9360, Springer, pp.172-188, 2015, 〈10.1007/978-3-319-23506-6_12〉
Accès au bibtex
BibTex
titre
A Generalized Framework for Virtual Substitution
auteur
Marek Kosta, Thomas Sturm
article
preprint. 2015, pp.17
Accès au bibtex
https://arxiv.org/pdf/1501.05826 BibTex
titre
Foreword to the Special Focus on Constraints and Combinations
auteur
Pascal Fontaine, Thomas Sturm, Uwe Waldmann
article
Dongming Wang. Switzerland. 9 (3), Springer, 2015, Mathematics in Computer Science, 〈10.1007/s11786-015-0239-8〉
Accès au bibtex
BibTex
titre
Subtropical Real Root Finding
auteur
Thomas Sturm
article
Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, Jul 2015, Bath, United Kingdom
Accès au bibtex
BibTex
titre
Vérification dynamique formelle de propriétés temporelles sur des applications distribuées réelles
auteur
Marion Guthmuller
article
Informatique [cs]. Université de Lorraine, 2015. Français. 〈NNT : 2015LORR0090〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01751786/file/manuscrit.pdf https://tel.archives-ouvertes.fr/tel-01751786/file/annexe-soutenance.pdf BibTex
titre
An overview of Schwilgué's patented adding machines
auteur
Denis Roegel
article
Bulletin of the Scientific Instrument Society, Scientific Instrument Society, 2015, 126, pp.16-22
Accès au bibtex
BibTex
titre
A Mechanical Calculator for Arithmetic Sequences (1844-1852): Part 1, Historical Context and Structure
auteur
Denis Roegel
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〉
Accès au bibtex
BibTex
titre
Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, Andreas Weber
article
Journal of Computational Physics, Elsevier, 2015, 291, pp.279-302. 〈10.1016/j.jcp.2015.02.050〉
Accès au bibtex
BibTex
titre
HASL: A new approach for performance evaluation and model checking from concepts to experimentation
auteur
Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
article
Performance Evaluation, Elsevier, 2015, 90, pp.53 - 77. 〈10.1016/j.peva.2015.04.003〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01817517/file/main.pdf BibTex
titre
HASL: A new approach for performance evaluation and model checking from concepts to experimentation
auteur
Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
article
Performance Evaluation, Elsevier, 2015, 90, pp.53-77. 〈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
titre
Three BUB1 and BUBR1/MAD3-related spindle assembly checkpoint proteins are required for accurate mitosis in Arabidopsis
auteur
Laetitia Paganelli, Marie-Cécile Caillaud, Michael Quentin, Isabelle Damiani, Benjamin Govetto, Philippe Lecomte, Pavel A Karpov, Pierre Abad, Marie Edith Chabouté, Bruno Favery
article
New Phytologist, Wiley, 2015, 205 (1), pp.202-215. 〈10.1111/nph.13073〉
Accès au bibtex
BibTex

2014

titre
Easter-based walks on a sphere
auteur
Denis Roegel
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01009458/file/roegel2014easter-walks.pdf BibTex
titre
Easter bracelets for 5700000 years
auteur
Denis Roegel
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01009457/file/roegel2014easter-bracelets.pdf BibTex
titre
Science of Computer Programming Special Issue: Automated Verification of Critical Systems
auteur
Gerald Lüttgen, Stephan Merz
article
Netherlands. 96 (3), Elsevier, 2014, Science of Computer Programming
Accès au bibtex
BibTex
titre
Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Computer Science and Information Systems, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. 〈http://www.comsis.org/archive.php?show=pprpdcat1〉. 〈10.2298/CSIS130122007A〉
Accès au bibtex
BibTex
titre
Proceedings 1st Workshop on Formal Integrated Development Environment
auteur
Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry
article
Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. France. 149, EPTCS, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, 〈10.4204/EPTCS.149〉
Accès au bibtex
BibTex
titre
Finite Quantification in Hierarchic Theorem Proving
auteur
Peter Baumgartner, Joshua Bax, Uwe Waldmann
article
Stéphane Demri and Deepak Kapur and Christoph Weidenbach. 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. Springer, 8562, pp.152-167, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
The "Villarceau circles" in Uhlberger's staircase (ca. 1580)
auteur
Denis Roegel
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00941465/file/roegel2014staircase-ond.pdf BibTex
titre
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
auteur
Jingshu Chen, Marie Duflot, Stephan Merz
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
titre
Towards Conflict-Driven Learning for Virtual Substitution
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Jul 2014, Vienna, Austria. CEUR Workshop Proceedings
Accès au bibtex
BibTex
titre
Towards Conflict-Driven Learning for Virtual Substitution
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
article
Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov. Computer Algebra in Scientific Computing - 16th International Workshop, CASC 2014, 2014, Warsaw, Poland. Springer, 8660, pp.256-270, 2014, Lecture Notes in Computer Science. 〈http://dx.doi.org/10.1007/978-3-319-10515-4_19〉
Accès au bibtex
BibTex
titre
Better Answers to Real Questions
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Jul 2014, Vienna, Austria. pp.69, CEUR Workshop Proceedings
Accès au bibtex
BibTex
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
Christoph Benzmüller and Jens Otten. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. 33, pp.1-16, 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf BibTex
titre
Proof automation and type synthesis for set theory in the context of TLA+
auteur
Hernán Vanzetto
article
Computer Science [cs]. Université de Lorraine, 2014. English. 〈NNT : 2014LORR0208〉
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01751181/file/thesis.pdf BibTex
titre
The (re)discovery of an early specialized mechanical calculating machine (ca. 1850)
auteur
Denis Roegel
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096153/file/roegel2014series.pdf BibTex
titre
The (re)discovery of one of the oldest modular digital mechanical counters (1844)
auteur
Denis Roegel
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096151/file/roegel2014counter.pdf BibTex
titre
Event B (english version)
auteur
Neeraj Kumar Singh, Dominique Méry
article
Jean-Louis Boulanger. Formal Methods Applied to Complex Systems, Wiley, 2014, Formal Methods Applied to Complex Systems, 9781119002727. 〈10.1002/9781119002727.ch10〉
Accès au bibtex
BibTex
titre
Formal Evaluation of Landing Gear System
auteur
Dominique Méry, Neeraj Kumar Singh
article
Ngo Hong Son; Yves Deville; Marc Bui. SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam. ACM, 2014, SoICT 2014 fifth symposium on Information and Communication Technology
Accès au bibtex
BibTex
titre
On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
auteur
Yamine Aït Ameur, J. Paul Gibson, Dominique Méry
article
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium,, Oct 2014, Corfu, Greece. Springer, 8803, pp.604-618, 2014, Lectures Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉
Accès au bibtex
BibTex
titre
Playing with State-Based Models for Designing Better Algorithms
auteur
Dominique Méry
article
Yamine Aït Ameur; Ladjel Bellatreche; George A. Papadopoulos. Model and Data Engineering - 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. Springer, 8748, pp.1-3, 2014, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉
Accès au bibtex
BibTex
titre
Theoretical Aspects of Computing – ICTAC 2014
auteur
Gabriel Ciobanu, Dominique Méry
article
Gabriel Ciobanu; Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, Sep 2014, Bucharest, Romania. 8687, Springer, 2014, Lecture Notes in Computer Science, 〈10.1007%2F978-3-319-10882-7〉
Accès au bibtex
BibTex
titre
Automated Reasoning – Seventh International Joint Conference (IJCAR 2014)
auteur
Stéphane Demri, Deepak Kapur, Christoph Weidenbach
article
Stéphane Demri; Deepak Kapur; Christoph Weidenbach. 7th International Joint Conference - IJCAR 2014, Jun 2014, Vienna, Austria. 8562, Springer, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-08586-9. 〈10.1007/978-3-319-08587-6〉. 〈http://link.springer.com/book/10.1007%2F978-3-319-08587-6〉
Accès au bibtex
BibTex
titre
The (re)discovery of some of the oldest key-driven adding machines (1844)
auteur
Denis Roegel
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096468/file/roegel2014adding-machine.pdf BibTex
titre
Polymorphic+Typeclass Superposition
auteur
Daniel Wand
article
Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01098078/file/draft.pdf BibTex
titre
A reconstruction of Arnaudeau’s table of triangular numbers (ca. 1896)
auteur
Denis Roegel
article
[Research Report] LORIA - Université de Lorraine. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01098344/file/arnaudeau1896doc.pdf BibTex
titre
Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014)
auteur
Stephan Merz, Jun Pang
article
Stephan Merz; Jun Pang. 16th International Conference on Formal Engineering Methods - ICFEM 2014, Nov 2014, Luxembourg, Luxembourg. 8829, Springer, pp.460, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-11737-9. 〈10.1007/978-3-319-11737-9〉
Accès au bibtex
BibTex
titre
Analysis of Self-* and P2P Systems using Refinement
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Yamine AIT AMEUR and Klaus-Dieter SCHEWE. ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Jun 2014, Toulouse, France. Springer, 8477, pp.117-123, 2014, LNCS. 〈10.1007/978-3-662-43652-3_9〉
Accès au bibtex
BibTex
titre
Analysis of Self-* and P2P Systems using Refinement (Full Report)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01018162/file/paperv1.pdf BibTex
titre
Quels fondements épistémologiques pour l’humain machine ?
auteur
Rémi Nazin
article
Sciences cognitives. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01107316/file/m%C3%A9moire.pdf BibTex
titre
Constructing a single cell in cylindrical algebraic decomposition
auteur
Christopher W. Brown, Marek Kosta
article
Journal of Symbolic Computation, Elsevier, 2014, pp.35. 〈http://dx.doi.org/10.1016/j.jsc.2014.09.024〉
Accès au bibtex
BibTex
titre
Refinement Types for TLA+
auteur
Stephan Merz, Hernán Vanzetto
article
Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp.143-157, 2014, LNCS. 〈10.1007/978-3-319-06200-6_11〉
Accès au bibtex
BibTex
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf BibTex
titre
Reclaiming human machine nature
auteur
Didier Fass
article
V. DUFFY. HCI International 2014, Jul 2014, Heraklion, Greece. Springer, 20 (8529), pp.588-589, 2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01069481/file/HCII2014-FASS.pdf BibTex
titre
Modelling an Aircraft Landing System in Event-B (Full Report)
auteur
Dominique Méry, Neeraj Kumar Singh
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00971787/file/full.pdf BibTex
titre
Integrating SMT solvers in Rodin
auteur
David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
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
titre
Editorial: Special Issue of Automated Verification of Critical Systems
auteur
Gerald Lüttgen, Stephan Merz
article
Science of Computer Programming, Elsevier, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
Accès au bibtex
BibTex
titre
The strange beauty of the twilight flower
auteur
Denis Roegel
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00978237/file/roegel2014twilight-flower.pdf BibTex
titre
Modeling an Aircraft Landing System in Event-B
auteur
Dominique Méry, Neeraj Kumar Singh
article
Frédéric Boniol. ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. Springer, 433, pp.154-159, 2014, CCIS
Accès au bibtex
BibTex
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
[Research Report] RR-8529, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00985135/file/RR-8529.pdf BibTex
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. Springer, 8562, pp.122-136, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08587-6_9〉
Accès au bibtex
BibTex
titre
Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
titre
The Semantics of Refinement Chart
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. HCI International, Jun 2014, Heraklion, Greece. Springer, 8529, pp.415-426, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-07725-3_42〉
Accès au bibtex
BibTex
titre
Proofs in satisfiability modulo theories
auteur
Clark Barrett, Leonardo De Moura, Pascal Fontaine
article
APPA (All about Proofs, Proofs for All), Jul 2014, Vienna, Austria. 2014
Accès au bibtex
BibTex
titre
Flip-Pushdown Automata with k Pushdown Reversals and E0L Systems are Incomparable
auteur
Marek Kosta, Pavol Duris
article
Information Processing Letters, Elsevier, 2014, 114 (8), pp.417-420
Accès au bibtex
BibTex
titre
Bounding messages for free in security protocols – extension to various security properties
auteur
Myrto Arapinis, Marie Duflot
article
Information and Computation, Elsevier, 2014, pp.34. 〈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
titre
The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
auteur
Dominique Méry, Bernhard Schätz, Alan Wassyng
article
Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2014, 4 (2), pp.17--37
Accès au bibtex
BibTex
titre
BDI: a new decidable clause class
auteur
Manuel Lamotte-Schubert, Christoph Weidenbach
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (6), pp.28. 〈http://logcom.oxfordjournals.org/content/early/2014/12/08/logcom.exu074〉
Accès au bibtex
BibTex
titre
RoKSN, a floral repressor, forms protein complexes with RoFD and RoFT to regulate vegetative and reproductive development in rose
auteur
Marie Randoux, Jean-Michel Daviere, Julien Jeauffre, Tatiana Thouroude, Sandrine Pierre, Youness Toualbia, Justine Perrotte, Jean-Paul Reynoird, Marie-José Jammes, Laurence Hibrand-Saint Oyant, Fabrice Foucher
article
New Phytologist, Wiley, 2014, 202 (1), pp.161-173
Accès au bibtex
BibTex

2013

titre
Transforming EVENT B Models into Verified C# Implementations
auteur
Dominique Méry, Monahan Rosemary
article
Alexei Lisitsa and Andrei Nemytykh. VPT 2013 - First International Workshop on Verification and Program Transformation, Jul 2013, Saint Petersburg, Russia. 16, pp.57-73, 2013, EPIC. 〈http://www.easychair.org/publications/?page=692335489〉
Accès au bibtex
BibTex
titre
Ideal Mode Selection of a Cardiac Pacing System
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. 4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. Springer, 8025, pp.258-267, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39173-6_31〉
Accès au bibtex
BibTex
titre
Formal Modelling and Verification of Population Protocols
auteur
Dominique Méry, Mike Poppleton
article
Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 2013, LNCS
Accès au bibtex
BibTex
titre
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
auteur
Ralf Karrenberg, Marek Kosta, Thomas Sturm
article
Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems. 〈10.1007/978-3-642-40885-4_5〉
Accès au bibtex
BibTex
titre
SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
auteur
Marek Kosta
article
Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), 2013, Nanning, China. 2013
Accès au bibtex
BibTex
titre
Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner Seiler, Thomas Sturm, Andreas Weber
article
Vladimir P. Gerdt and Wolfram Koepf and Ernst W. Mayr and Evgenii V. Vorozhtsov. CASC 2013 - 15th International Workshop on Computer Algebra in Scientific Computing, Sep 2013, Berlin, Germany. Springer, LNCS, 8136, pp.88-99, 2013, CASC 2013: Computer Algebra in Scientific Computing. 〈10.1007/978-3-319-02297-0_7〉
Accès au bibtex
BibTex
titre
Computing Tiny Clause Normal Forms
auteur
Noran Azmy, Christoph Weidenbach
article
Maria-Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.109-125, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_7〉
Accès au bibtex
BibTex
titre
Hierarchic Superposition With Weak Abstraction
auteur
Peter Baumgartner, Uwe Waldmann
article
Maria Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.39-57, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_3〉
Accès au bibtex
BibTex
titre
A reconstruction of Centnerschwer's table of quarter-squares (1825)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880833/file/centnerschwer1825doc.pdf BibTex
titre
A reconstruction of Laundy's table of quarter-squares (1856)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880835/file/laundy1856doc.pdf BibTex
titre
A reconstruction of Herwart's table of multiplication (1610)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880842/file/herwart1610doc.pdf BibTex
titre
A reconstruction of Ludolfs's Tetragonometria tabularia (1690)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880845/file/ludolf1690doc.pdf BibTex
titre
A reconstruction of Goldberg's table of factors (1862)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880840/file/goldberg1862doc.pdf BibTex
titre
A reconstruction of Joncourt's table of triangular numbers (1762)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880843/file/joncourt1762doc.pdf BibTex
titre
A reconstruction of Shortrede's traverse tables (1864)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880847/file/shortrede1864doc.pdf BibTex
titre
A reconstruction of Voisin's table of quarter-squares (1817)
auteur
Denis Roegel
article
[Research Report] 2013, pp.133
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00812834/file/voisin1817doc.pdf BibTex
titre
Towards Certifying Network Calculus
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
article
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.484-489, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_37〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904796/file/final.pdf BibTex
titre
Certifying Network Calculus in a Proof Assistant
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
article
EUCASS - 5th European Conference for Aeronautics and Space Sciences, Jul 2013, Munich, Germany. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904817/file/submission.pdf BibTex
titre
Formal Verification of Distributed Algorithms
auteur
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
article
Bernadette Charron-Bost and Stephan Merz and Andrey Rybalchenko and Josef Widder. 3, Dagstuhl, pp.16, 2013, Dagstuhl Reports, 〈10.4230/DagRep.3.4.1〉
Accès au bibtex
BibTex
titre
Putting in perspective human-machine system theory and modeling: from theoretical biology to artifacts integrative design and organization.
auteur
Didier Fass
article
4th International Conference - DHM 2013, Held as Part of HCI International 2013, Jul 2013, Las Vegas, United States. Springer, 8025, pp.316-325, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39173-6_37〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00867070/file/FASS_HCII2013.pdf BibTex
titre
Spécification d'exigences physico-physiologiques d'interaction homme-machine en ingénierie système
auteur
Gérard Morel, Jean-Marc Dupont, Romain Lieber, Fabien Bouffaron, Dominique Méry, Frédérique Mayer, Jean-Luc Marty
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
titre
Computing prime implicant
auteur
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
article
FMCAD - Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. IEEE, pp.46-52, 2013, 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings/54418_IEEE%20FMCAD_Complete%20Book.pdf〉
Accès au bibtex
BibTex
titre
Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. 2013
Accès au bibtex
BibTex
titre
From Event-B Specifications to Programs for Distributed Algorithms
auteur
Mohammed Tounsi, Mohammed Mosbah, Dominique Méry
article
Sumitra Reddy and Mohammed Jmaiel. WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. IEEE, 2013, 22nd IEEE WETICE Conference. 〈10.1109/WETICE.2013.44〉
Accès au bibtex
BibTex
titre
SyMT: finding symmetries in SMT formulas
auteur
Carlos Areces, David Déharbe, Pascal Fontaine, Orbe Ezequiel
article
11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland. 2013
Accès au bibtex
BibTex
titre
Frontiers of Combining Systems
auteur
Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
article
Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. 8152, Springer, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
Accès au bibtex
BibTex
titre
Viral and cellular factors involved in phloem transport of plant viruses
auteur
Clémence Hipper, Veronique Brault, Véronique Ziegler-Graff, Frederic Revers
article
Frontiers in Plant Science, Frontiers, 2013, 4, pp.1-24. 〈10.3389/fpls.2013.00154〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01123342/file/Cl%C3%A9mence%20Hipper%202013%20-%20Viral%20and%20cellular%20factors%20involved%20in%20phloem%20transport%20of%20plant%20viruses_%7B88C42548-C127-4AA9-8017-80EC22CC5A0F%7D.pdf BibTex
titre
Event B
auteur
Dominique Méry, Neeraj Kumar Singh
article
Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7
Accès au bibtex
BibTex
titre
A reconstruction of Plassmann's table of quarter-squares (1933)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880838/file/plassmann1933doc.pdf BibTex
titre
A reconstruction of Kulik's table of multiplication (1851)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654436/file/kulik1851doc.pdf BibTex
titre
A reconstruction of Bürger's table of quarter-squares (1817)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880832/file/buerger1817doc.pdf BibTex
titre
A reconstruction of Lifchitz's table of primes (1971)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880841/file/lifchitz1971doc2.pdf https://hal.inria.fr/hal-00880841/file/lifchitz1971doc1.pdf BibTex
titre
A reconstruction of Magini's Tabula tetragonica (1592)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880844/file/magini1592doc.pdf BibTex
titre
A reconstruction of Schiereck's table of squares (1827)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880846/file/schiereck1827doc.pdf BibTex
titre
A reconstruction of Ulbrich's table of factors (1791-1800)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880839/file/ulbrich1800doc1.pdf https://hal.inria.fr/hal-00880839/file/ulbrich1800doc2.pdf https://hal.inria.fr/hal-00880839/file/ulbrich1800doc3.pdf BibTex
titre
A reconstruction of Merpaut's table of quarter-squares (1832)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880834/file/merpaut1832doc.pdf BibTex
titre
A reconstruction of Blater's table of quarter-squares (1887)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880836/file/blater1887doc.pdf BibTex
titre
A reconstruction of Bojko's table of quarter-squares (1909)
auteur
Denis Roegel
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880837/file/bojko1909doc.pdf BibTex
titre
Hierarchic Superposition: Completeness without Compactness
auteur
Peter Baumgartner, Uwe Waldmann
article
Marek Kosta and Thomas Sturm. MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12, 〈http://resources.mpi-inf.mpg.de/conferences/macis2013/program.html〉
Accès au bibtex
BibTex
titre
Formal Specification of Medical Systems by Proof-Based Refinement
auteur
Dominique Méry, Neeraj Kumar Singh
article
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.15. 〈10.1145/2406336.2406351〉
Accès au bibtex
BibTex

2012

titre
Le corps d'une " prophétesse " ?
auteur
Didier Fass, Francis Janot
article
FLORENCE CALAMENT - RICARDO EICHMANN - CHRISTOPHE VENDRIES. Le luth dans l'Égypte byzantine. La tombe de la " Prophétesse d'Antinoé " au Musée de Grenoble, Verlag Marie Leidorf GmbH * Rahden/Westf., pp.190, 2012, DEUTSCHES ARCHÄOLOGISCHES INSTITUT ORIENT-ABTEILUNG Orient-Archäologie Band 26, ISBN 978-3-86757-656-3
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00744977/file/grenoblefin.pdf BibTex
titre
Augmented Human Engineering: A Theoretical and Experimental Approach to Human Systems Integration
auteur
Didier Fass
article
Boris Cogan. Systems Engineering - Practice and Theory, InTech Open Access Publisher, pp.257-276, 2012, Computer and Information Science - "Numerical Analysis and Scientific Computing", 978-953-51-0322-6. 〈10.5772/2121〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00744225/file/InTech-Augmented_human_engineering_a_theoretical_and_experimental_approach_to_human_systems_integration.pdf BibTex
titre
Stuttering Equivalence
auteur
Stephan Merz
article
[Research Report] 2012
Accès au bibtex
BibTex
titre
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. Springer, 7180, pp.289-303, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28717-6_23〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760570/file/tla2smt.pdf BibTex
titre
Harnessing SMT Solvers for TLA+ Proofs
auteur
Stephan Merz, Hernán Vanzetto
article
Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, 53, 2012, ECEASST
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760579/file/avocs2012.pdf BibTex
titre
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
auteur
Henri Debrat, Stephan Merz
article
[Research Report] 2012
Accès au bibtex
BibTex
titre
Formal Verification Of Pastry Using TLA+
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Leslie Lamport and Stephan Merz. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00768812/file/paper.pdf BibTex
titre
Spécification d'un Processus Technico-Physiologique de Perception de Fermeture et Verrouillage d'un capot moteur en situation de maintenance aéronautique
auteur
Jean-Marc Dupont, Romain Lieber, Gérard Morel, Dominique Méry, Fabien Bouffaron
article
2012
Accès au bibtex
BibTex
titre
Revisiting Snapshot Algorithms by Refinement-based Techniques
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
PDCAT 2012 : The Thirteenth International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2012, Beijing, China. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00734131/file/pdcat2012v14.pdf BibTex
titre
More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification
auteur
Jasmin Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
article
Lennart Beringer and Amy Felty. Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. Springer, 7406, pp.345-360, 2012, LNCS
Accès au bibtex
BibTex
titre
Automatic Generation of Invariants for Circular Derivations in SUP(LA)
auteur
Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach
article
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mar 2012, Mérida, Venezuela. Springer, 7180, pp.197-211, 2012, LNCS
Accès au bibtex
BibTex
titre
Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
auteur
Martin Bromberger
article
Logic in Computer Science [cs.LO]. 2012
Accès au bibtex
BibTex
titre
Formalization of Heart Models Based on the Conduction of Electrical Impulses and Cellular Automata
auteur
Dominique Méry, Neeraj Kumar Singh
article
Liu, Zhiming and Wassyng, Alan. Foundations of Health Informatics Engineering and Systems}, 7151, Springer Berlin Heidelberg, pp.140-159, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. 〈10.1007/978-3-642-32355-3_9〉
Accès au bibtex
BibTex
titre
Medical Protocol Diagnosis Using Formal Methods
auteur
Dominique Méry, Neeraj Kumar Singh
article
Liu, Zhiming and Wassyng, Alan. Foundations of Health Informatics Engineering and Systems, 7151, Springer Berlin Heidelberg, pp.1-20, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. 〈10.1007/978-3-642-32355-3_1〉
Accès au bibtex
BibTex
titre
Formal Verification of Fault Tolerant NoC-based Architecture
auteur
Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, Camel Tanougast
article
First International Workshop on Mathematics and Computer Science (IWMCS2012), Dec 2012, Tiaret, Algeria. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00763092/file/iwmcsv5.pdf BibTex
titre
Formal Verification of Distributed Algorithms using PlusCal-2
auteur
Sabina Akhtar
article
Data Structures and Algorithms [cs.DS]. Université de Lorraine, 2012. English. 〈NNT : 2012LORR0014〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01749162/file/ThA_se-Sabina_AKHTAR.pdf BibTex
titre
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
auteur
Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
article
Science of Computer Programming, Elsevier, 2012, 77 (10-11), pp.1122-1150
Accès au bibtex
BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32759-9_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., 2012, 〈http://arxiv.org/abs/1208.5933〉
Accès au bibtex
BibTex
titre
Handling Heterogeneity in Formal Developments of Hardware and Software Systems
auteur
Yamine Ait Ameur, Dominique Méry
article
Tiziana Margaria and Bernhard Steffen. ISoLA - 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - 2012, Oct 2012, Amirandes, Heraklion, Greece. Springer, 7610, pp.327-328, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34032-1_33〉
Accès au bibtex
BibTex
titre
FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings
auteur
Dimitra Giannakopoulou, Dominique Méry
article
Dimitra Giannakopoulou and Dominique Méry. Springer, 7436, pp.488, 2012, LNCS - Lecture Notes in Computer Science, 978-3-642-32758-2. 〈10.1007/978-3-642-32759-9〉
Accès au bibtex
BibTex
titre
Combination of disjoint theories: beyond decidability
auteur
Pascal Fontaine, Stephan Merz, Christoph Weidenbach
article
Bernhard Gramlich and Dale Miller and Uli Sattler. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.256-270, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31365-3_21〉
Accès au bibtex
BibTex
titre
SMT solvers for Rodin
auteur
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
article
John Derrick and John A. Fitzgerald and Stefania Gnesi and Sarfraz Khurshid and Michael Leuschel and Steve Reeves and Elvinia Riccobene. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. Springer, 7316, pp.194-207, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-30885-7_14〉
Accès au bibtex
BibTex
titre
Critical systems development methodology using formal techniques
auteur
Dominique Méry, Neeraj Kumar Singh
article
3rd International Symposium on Information and Communication Technology - SoICT 2012, Aug 2012, Ha Long, Vietnam. ACM, pp.3-12, 2012, SoICT '12 - Proceedings of the Third Symposium on Information and Communication Technology. 〈10.1145/2350716.2350720〉
Accès au bibtex
BibTex
titre
The LOCOMAT Project: Recomputing Mathematical and Astronomical Tables
auteur
Denis Roegel
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〉
Accès au bibtex
BibTex

2011

titre
Stepwise Development Of Distributed Vertex Coloring Algorithms (Full Report)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry
article
[Technical Report] LORIA - Université de Lorraine. 2011, pp.90
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606254/file/Rapport_v0.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.pdf BibTex
titre
Combining theories: the Ackerman and Guarded Fragments
auteur
Carlos Areces, Pascal Fontaine
article
Cesare Tinelli and Viorica Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Oct 2011, Saarbrücken, Germany. Springer Verlag, 6989, pp.40--54, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24364-6_4〉
Accès au bibtex
BibTex
titre
Quantifier Inference Rules for SMT proofs
auteur
David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642535/file/paper2.pdf BibTex
titre
Fragments de l'arithmétique dans une combinaison de procédures de décision
auteur
Diego Caminha Barbosa de Oliveira
article
Génie logiciel [cs.SE]. Université Nancy II, 2011. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00578254/file/thesis_full.pdf BibTex
titre
Formal Development and Automatic Code Generation : Cardiac Pacemaker
auteur
Dominique Méry, Neeraj Kumar Singh
article
International Conference on Computers and Advanced Technology in Education (ICCATE, 2011), Nov 2011, Beijing, China. 2011
Accès au bibtex
BibTex
titre
Automatic Code Generation from Event-B Models
auteur
Dominique Méry, Neeraj Kumar Singh
article
SoICT 2011, Oct 2011, Hanoi, Vietnam. ACM ICPS, 2011
Accès au bibtex
BibTex
titre
Formalisation of the Heart based on Conduction of Electrical Impulses and Cellular-Automata
auteur
Dominique Méry, Neeraj Kumar Singh
article
Zhiming Liu and Alan Wassyng. International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa. 2011, 〈http://www.iist.unu.edu/ICTAC/FHIES2011/Files/fhies2011_8_17.pdf〉
Accès au bibtex
BibTex
titre
EB2J : Code Generation from Event-B to Java
auteur
Dominique Méry, Neeraj Kumar Singh
article
SBMF - Brazilian Symposium on Formal Methods, Sep 2011, São Paulo, Brazil. 2011
Accès au bibtex
BibTex
titre
Medical Protocol Diagnosis using Formal Methods
auteur
Dominique Méry, Neeraj Kumar Singh
article
Zhiming Liu and Alan Wassyng. International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa. 2011, 〈http://www.iist.unu.edu/ICTAC/FHIES2011/Files/fhies2011_8_17.pdf〉
Accès au bibtex
BibTex
titre
A generic framework: from modeling to code
auteur
Dominique Méry, Neeraj Kumar Singh
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
titre
Analysis of DSR Protocol in Event-B
auteur
Dominique Méry, Neeraj Kumar Singh
article
Défago, Xavier and Petit, Franck and Villain, Vincent. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer Berlin / Heidelberg, 6976, pp.401-415, 2011, Stabilization, Safety, and Security of Distributed Systems. 〈http://dx.doi.org/10.1007/978-3-642-24550-3_30〉
Accès au bibtex
BibTex
titre
Mouton's table of logarithms and its extensions (ca. 1670)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654572/file/moutondoc.pdf BibTex
titre
Top modèle et Top simulation : la momie de Lunéville Observation, Modélisation, Simulation et Validation
auteur
Dominique Méry, Didier Fass
article
Francis JANOT. La Dame d'Antinoé : une "momie" au Château de Lunéville, Presse universitaire de Nancy, pp.132, 2011, Archéologie, Espaces, Patrimoines, 978-2-8143-0088-0
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00744242/file/papier-fassmery.pdf BibTex
titre
A reconstruction of Vega's table of primes and factors (1797)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654456/file/vega1797doc.pdf BibTex
titre
A reconstruction of Viète's Canonion triangvlorvm (1579)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654459/file/viete1579doc2.pdf BibTex
titre
Tissot's table of logarithms (ca. 1880)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654454/file/tissotdoc.pdf BibTex
titre
A reconstruction of Smogulecki and Xue's table of trigonometrical logarithms (ca. 1653)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654452/file/smogulecki1653doc2.pdf BibTex
titre
A reconstruction of the tables of Thompson's Logarithmetica Britannica (1952)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654453/file/thompson1952doc.pdf BibTex
titre
A reconstruction of the tables of the Shuli Jingyun (1713-1723)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654450/file/shuli1723intro.pdf BibTex
titre
A reconstruction of Vega's table of primes and factors (1821)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654457/file/vega1821doc.pdf BibTex
titre
A reconstruction of Viète's Canon Mathematicus (1579)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654458/file/viete1579doc1.pdf BibTex
titre
A reconstruction of Kulik's "Magnus Canon Divisorum" (ca. 1825-1863)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654460/file/kulik1863intro.pdf BibTex
titre
A reconstruction of Smogulecki and Xue's table of logarithms of numbers (ca. 1653)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654451/file/smogulecki1653doc1.pdf BibTex
titre
A reconstruction of Vega's table of primes and factors (1782)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654455/file/vega1782doc.pdf BibTex
titre
Technical Report on Formalisation of the Heart using Analysis of Conduction Time and Velocity of the Electrocardiography and Cellular-Automata
auteur
Dominique Méry, Neeraj Kumar Singh
article
[Technical Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00600339/file/Version1.pdf BibTex
titre
Stepwise Development of Distributed Vertex Colouring Algorithms (Abstract)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606201/file/_MERY-ANDRIAMIARINA_Abstract_Grande_Region_SECDAY_2011_v2.pdf BibTex
titre
Stepwise Development of Distributed Algorithms (Research Abstract)
auteur
Manamiary Bruno Andriamiarina
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606204/file/_ANDRIAMIARINA_Abstract_FME_Symposium_FM2011_v4.pdf BibTex
titre
A reconstruction of Gingerich's table of regular sexagesimals and a cuneiform version of the table (1965)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654428/file/gingerich1965doc.pdf BibTex
titre
A reconstruction of Beeger's table of primes (1951)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654416/file/beeger1951doc.pdf BibTex
titre
A reconstruction of Hinkley's tables of primes and factors (1853)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654429/file/hinkley1853doc.pdf BibTex
titre
A reconstruction of Inghirami's table of factors (1841)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654430/file/inghirami1841doc.pdf BibTex
titre
A reconstruction of Kaván's table of factors (1937)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654432/file/kavan1937doc.pdf BibTex
titre
A reconstruction of Kulik's table of factors (1825)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654434/file/kulik1825doc.pdf BibTex
titre
A reconstruction of Kulik's table of squares and cubes (1848)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654435/file/kulik1848doc.pdf BibTex
titre
A reconstruction of Brancker's Table of incomposits (1668)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654419/file/brancker1668doc.pdf BibTex
titre
A reconstruction of Schenmark's table of factors (ca. 1780)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654449/file/schenmark1780doc.pdf BibTex
titre
A reconstruction of Lambert and Felkel's table of factors (1798)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654441/file/lambert1798doc.pdf BibTex
titre
A reconstruction of Lehmer's table of primes (1914)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654443/file/lehmer1914doc.pdf BibTex
titre
A reconstruction of Lambert's table of factors (1770)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654439/file/lambert1770doc.pdf BibTex
titre
A reconstruction of the table of factors of Peters, Lodge, Ternouth, and Gifford (1935)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654448/file/peters1935doc.pdf BibTex
titre
A reconstruction of Chernac's Cribrum arithmeticum (1811)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654421/file/chernac1811doc.pdf BibTex
titre
A reconstruction of Krause's table of factors (1804)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654433/file/krause1804doc.pdf BibTex
titre
A reconstruction of Merritt's Brocot table (1947)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654446/file/merritt1947doc2.pdf BibTex
titre
A reconstruction of Neville's Farey series of order 1025 (1950)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654447/file/neville1950doc.pdf BibTex
titre
A reconstruction of Gifford's table of primes and factors (1931)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654427/file/gifford1931doc.pdf BibTex
titre
A reconstruction of the tables of factors of Burckhardt, Dase, and Glaisher (1814-1883), and their extension to the tenth million
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654420/file/vol01.pdf https://hal.inria.fr/hal-00654420/file/vol02.pdf https://hal.inria.fr/hal-00654420/file/vol03.pdf https://hal.inria.fr/hal-00654420/file/vol04.pdf https://hal.inria.fr/hal-00654420/file/vol05.pdf https://hal.inria.fr/hal-00654420/file/vol06.pdf https://hal.inria.fr/hal-00654420/file/vol07.pdf https://hal.inria.fr/hal-00654420/file/vol08.pdf https://hal.inria.fr/hal-00654420/file/vol09.pdf https://hal.inria.fr/hal-00654420/file/vol10.pdf BibTex
titre
A reconstruction of Crelle's Rechentafeln (1820)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654422/file/crelle1820doc.pdf BibTex
titre
A reconstruction of Crelle's Erleichterungstafel (1836)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654423/file/crelle1836doc.pdf BibTex
titre
A reconstruction of Felkel's tables of primes and factors (1776)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654425/file/felkel1776doc1.pdf https://hal.inria.fr/hal-00654425/file/felkel%2Ffelkel1776doc2.pdf https://hal.inria.fr/hal-00654425/file/felkel%2Ffelkel1776doc3.pdf BibTex
titre
A reconstruction of Jones' table of factors (1896)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654431/file/jones1896doc.pdf BibTex
titre
Vlacq's tables in Chinese - Introduction to Chinese and Japanese tables of logarithms, with a review of secondary sources (second edition)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654438/file/clogdoc.pdf https://hal.inria.fr/hal-00654438/file/clog1.pdf https://hal.inria.fr/hal-00654438/file/clog2.pdf https://hal.inria.fr/hal-00654438/file/clog3.pdf BibTex
titre
A reconstruction of Lehmer's table of factors (1909)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654442/file/lehmer1909doc.pdf BibTex
titre
A reconstruction of Merritt's table of "useful numbers" (1947)
auteur
Denis Roegel
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00654445/file/merritt1947doc1.pdf BibTex
titre
Human systems integration design: which generalized rationale?
auteur
Romain Lieber, Didier Fass
article
Masaaki Kurosu. 14th International Conference on Human-Computer Interaction, HCI International 2011, Jul 2011, Orlando, Florida, United States. Springer, 6776, pp.101-109, 2011, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/q61rn5u18342305p/〉. 〈10.1007/978-3-642-21753-1_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00609649/file/HCII2011LIEBER_and_Fass.pdf BibTex
titre
Compression of Propositional Resolution Proofs via Partial Regularization
auteur
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. Springer, 6803, pp.237-251, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-22438-6_19〉
Accès au bibtex
BibTex
titre
Exploiting Symmetry in SMT Problems
auteur
David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. Springer, 6803, pp.222-236, 2011, 〈10.1007/978-3-642-22438-6_18〉
Accès au bibtex
BibTex
titre
Refinement-based Verification of Local Synchronization Algorithms
auteur
Dominique Méry, Mohamed Mosbah, Mohamed Tounsi
article
17TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS, Jun 2011, Limerick, Ireland. Springer, à paraître, 2011, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Technical Report on Interpretation of the Electrocardiogram (ECG) Signal using Formal Methods
auteur
Dominique Méry, Neeraj Kumar Singh
article
[Technical Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00584177/file/TechRepoECG2011.pdf BibTex
titre
Towards Verification of the Pastry Protocol using TLA+
auteur
Stephan Merz, Tianxiang Lu, Christoph Weidenbach
article
R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. 6722, 2011, FMOODS/FORTE 2011
Accès au bibtex
BibTex
titre
Formal Verification of Consensus Algorithms Tolerating Malicious Faults
auteur
Bernadette Charron-Bost, Henri Debrat, Stephan Merz
article
Xavier Défago and Franck Petit and Vincent Villain. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer, 6976, pp.120-134, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24550-3_11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00639048/file/main.pdf BibTex
titre
Proving Distributed Algorithms by Combining Refinement and Local Computations
auteur
Mohamed Tounsi, Mohamed Mosbah, Dominique Méry
article
Electronic Communications of the EASST, 2011, 35, pp.ISSN 1863-2122
Accès au bibtex
BibTex
titre
Towards certification of TLA+ proof obligations with SMT solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00645458/file/tla2smt.pdf BibTex
titre
SimGrid MC: Verification Support for a Multi-API Simulation Platform
auteur
Stephan Merz, Martin Quinson, Cristian Rosa
article
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.274-288, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_18〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf BibTex
titre
Towards Verification of the Pastry Protocol Using TLA +
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.244-258, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_16〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf BibTex

2010

titre
A reconstruction of the tables of Pitiscus' Thesaurus Mathematicus (1613)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543933/file/pitiscus1613doc.pdf BibTex
titre
Napier's ideal construction of the logarithms
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543934/file/napier1619construction.pdf BibTex
titre
A reconstruction of Briggs' Logarithmorum chilias prima (1617)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543935/file/briggs1617doc.pdf BibTex
titre
Bürgi's Progress Tabulen (1620): logarithmic tables without logarithms
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543936/file/buergi1620doc.pdf BibTex
titre
B événementiel et les propriétés de vivacité
auteur
Olfa Mosbahi, Jacques Jaray
article
Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2010, 44 (9-10), pp.1119-1163. 〈10.3166/jesa.44.1119-1163〉
Accès au bibtex
BibTex
titre
Formal Verification of Consensus Algorithms in a Proof Assistant
auteur
Henri Debrat, Bernadette Charron-Bost, Stephan Merz
article
Michael Backes and Ralf Küsters. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00539899/file/sho-isabelle.pdf BibTex
titre
Functional Behavior of a Cardiac Pacing System
auteur
Dominique Méry, Neeraj Kumar Singh
article
International Journal of Discrete Event Control Systems (IJDECS), Dr. Mohamed Khalgui, 2010
Accès au bibtex
BibTex
titre
Model Checking the Pastry Routing Protocol
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Jens Bendisposto and Michael Leuschel and Markus Roggenbach. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. Universität Düsseldorf, pp.19-21, 2010, 10th International Workshop Automated Verification of Critical Systems
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540811/file/article-new.pdf BibTex
titre
EB2C : A Tool for Event-B to C Conversion Support
auteur
Dominique Méry, Neeraj Kumar Singh
article
Poster and Tool Demo submission, and published in a CNR Technical Report. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540006/file/cameraready-sefm2010.pdf BibTex
titre
Real-Time Animation for Formal Specification
auteur
Dominique Méry, Neeraj Kumar Singh
article
Marc Aiguier and Francis Bretaudeau and Daniel Krob. Complex Systems Design & Management 2010, Oct 2010, Paris, France. Springer, pp.49-60, 2010, Proceedings of the First International Conference on Complex System Design & Management CSDM 2010. 〈10.1007/978-3-642-15654-0_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540005/file/Animator_CSDM2010.pdf BibTex
titre
Trustable Formal Specification for Software Certification
auteur
Dominique Méry, Neeraj Kumar Singh
article
T. Margaria and B. Ste. 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, Oct 2010, Heraklion, Crete, Greece. Springer, 6416, pp.312-326, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-16561-0_31〉
Accès au bibtex
BibTex
titre
Integrated Formal Methods
auteur
Dominique Méry, Stephan Merz
article
Dominique Méry and Stephan Merz. 6396, Springer, pp.335, 2010, Lecture Notes in Computer Science, 978-3-642-16264-0. 〈10.1007/978-3-642-16265-7〉
Accès au bibtex
BibTex
titre
Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms
auteur
Sabina Akhtar, Stephan Merz, Martin Quinson
article
Eric Cariou, Laurence Duchien, Yves Ledru. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00544137/file/GDR-GDL_Sabina.pdf BibTex
titre
A reconstruction of Henri Andoyer's trigonometric tables (1915-1918)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543955/file/andoyer1915doc.pdf https://hal.inria.fr/inria-00543955/file/andoyer1916doc.pdf https://hal.inria.fr/inria-00543955/file/andoyer1918doc.pdf BibTex
titre
A reconstruction of Charles Babbage's table of logarithms (1827)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543948/file/babbage1827doc.pdf BibTex
titre
A construction of Edward Sang's projected table of nine-place logarithms to one million (1872)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543950/file/sang1872doc.pdf BibTex
titre
A reconstruction of the "Tables des logarithmes à huit décimales'' from the French "Service géographique de l'armée'' (1891)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543952/file/sga1891doc.pdf BibTex
titre
A sketch of Mendizábal y Tamborrel's table of logarithms (1891)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543953/file/mendizabal1891doc.pdf BibTex
titre
A reconstruction of Henri Andoyer's table of logarithms (1911)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543954/file/andoyer1911doc.pdf BibTex
titre
A reconstruction of Edward Sang's table of logarithms (1871)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543949/file/sang1871doc.pdf BibTex
titre
The great logarithmic and trigonometric tables of the French Cadastre: a preliminary investigation
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543946/file/analysis.pdf BibTex
titre
Exploring and Exploiting Algebraic and Graphical Properties of Resolution
auteur
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00544658/file/AlgebraicPropertiesOfResolution.pdf BibTex
titre
Proof Compression with the CIRes Method [Abstract]
auteur
Bruno Woltzenlogel Paleo
article
Computability in Europa, Jun 2010, Ponta Delgada, Portugal
Accès au bibtex
BibTex
titre
Physics and Proof Theory
auteur
Bruno Woltzenlogel Paleo
article
International Workshop on Physics and Computation, Aug 2010, Luxor, Egypt
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545462/file/PhysicsAndProofTheory_Elsevier_.pdf BibTex
titre
Atomic Cut Introduction by Resolution: Proof Structuring and Compression
auteur
Bruno Woltzenlogel Paleo
article
Edmund M. Clarke and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Apr 2010, Dakar, Senegal. Springer, 6355, pp.463-480, 2011, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-17511-4_26〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545473/file/AtomicCutIntroduction_-_Submitted_Version.pdf BibTex
titre
Using Proofs to Compute Implicatures [Abstract]
auteur
Bruno Woltzenlogel Paleo, Ekaterina Lebedeva
article
Computability in Europe, Jun 2010, Ponta Delgada, Portugal
Accès au bibtex
BibTex
titre
System Description: The Proof Transformation System CERES
auteur
Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo
article
Jürgen Giesl and Reiner Hähnle. International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.427-433, 2010, Lecture Notes in Computer Science / Lecture Notes in ArtificiaI Intelligence. 〈10.1007/978-3-642-14203-1_36〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545482/file/CEResSystemDescription.pdf BibTex
titre
A High-Level Language for Modeling Algorithms and their Properties
auteur
Sabina Akhtar, Stephan Merz, Martin Quinson
article
13th Brazilian Symposium on Formal Methods - SBMF'2010, Nov 2010, Natal, Brazil. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537779/file/final.pdf BibTex
titre
Verifying Safety Properties With the TLA+ Proof System
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-14203-1_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534821/file/tlaps.pdf BibTex
titre
Sudoku s vepsanými kandži: integrace čínských glyfů s grafikou na úrovni METAPOSTu
auteur
Denis Roegel
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
titre
Technical Report on Formal Development of Two-Electrode Cardiac Pacing System
auteur
Dominique Méry, Neeraj Kumar Singh
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00465061/file/Report_2electrode.pdf BibTex
titre
A reconstruction of Henri Andoyer's table of logarithms (1922)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00551097/file/andoyer1922doc.pdf BibTex
titre
Proving Distributed Algorithms by Combining Refinement and Local Computations
auteur
Dominique Méry, Mohammed Mosbah, Mohammed Tounsi
article
Jens Bendisposto, Michael Leuschel, Markus Roggenbach. AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Sep 2010, Dusseldorf, Germany. 2010
Accès au bibtex
BibTex
titre
O rozboru jednoho makra
auteur
Denis Roegel
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
titre
Kulové plochy, hlavní kružnice a rovnoběžky
auteur
Denis Roegel
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
titre
Jednoduché makro suanpan na kreslení čínského a japonského abaku
auteur
Denis Roegel
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
titre
Specifying and Verifying PLC systems with TLA+: a case study
auteur
Hehua Zhang, Stephan Merz, Ming Gu
article
Computers and Mathematics with Applications, Elsevier, 2010, 60 (3), pp.695-705. 〈10.1016/j.camwa.2010.05.017〉
Accès au bibtex
BibTex
titre
The TLA+ Proof System: Building a Heterogeneous Verification Platform
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, 6255, pp.44, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14808-8_3〉
Accès au bibtex
BibTex
titre
La composition des protocoles de sécurité avec la méthode B événementielle
auteur
Nazim Benaissa
article
Modélisation et simulation. Université Henri Poincaré - Nancy 1, 2010. Français. 〈NNT : 2010NAN10034〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01748202/file/SCD_T_2010_0034_BENAISSA.pdf BibTex
titre
A Simple Model of Communication APIs ­ - Application to Dynamic Partial-order Reduction
auteur
Cristian Rosa, Stephan Merz, Martin Quinson
article
10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Sep 2010, Düsseldorf, Germany. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00532889/file/avocs.pdf BibTex
titre
Combining decision procedures by (model-)equality propagation
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
article
Science of Computer Programming, Elsevier, 2010, 240 (2 July 2009), pp.113-128. 〈10.1016/j.entcs.2009.05.048〉
Accès au bibtex
BibTex
titre
Proof-Based Design of Security Protocols
auteur
Nazim Benaissa, Dominique Méry
article
Ernst W. Mayr. 5th International Computer Science Symposium in Russia, CSR 2010, Jun 2010, KAZAN, Russia. Springer, 6072, pp.25-36, 2010, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
A reconstruction of the tables of Briggs' Arithmetica logarithmica (1624)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543939/file/briggs1624doc.pdf BibTex
titre
A reconstruction of Gunter's Canon triangulorum (1620)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543938/file/gunter1620doc.pdf BibTex
titre
A reconstruction of the tables of Briggs and Gellibrand's Trigonometria Britannica (1633)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543943/file/briggs1633doc.pdf BibTex
titre
A reconstruction of Adriaan Vlacq's tables in the Trigonometria artificialis (1633)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543944/file/vlacq1633doc.pdf BibTex
titre
Introduction to Chinese and Japanese tables of logarithms, with a review of secondary sources
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543945/file/clogdoc.pdf BibTex
titre
A reconstruction of De Decker-Vlacq's tables in the Arithmetica logarithmica (1628)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543941/file/vlacq1628doc.pdf BibTex
titre
GridTPT: a distributed platform for Theorem Prover Testing
auteur
Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
article
2nd Workshop on Practical Aspects of Automated Reasoning (PAAR), Jul 2010, Edinburgh, United Kingdom. 2010
Accès au bibtex
BibTex
titre
A reconstruction of the tables of Rheticus' Canon doctrinæ triangulorum (1551)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543931/file/rheticus1551doc.pdf BibTex
titre
A reconstruction of the tables of Rheticus' Opus Palatinum (1596)
auteur
Denis Roegel
article
[Research Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00543932/file/rheticus1596doc.pdf BibTex
titre
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method
auteur
Joris Rehm
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〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00336624/file/rcp_sttt.pdf BibTex

2009

titre
An introduction to nomography: Garrigues' nomogram for the computation of Easter
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.88-104
Accès au bibtex
BibTex
titre
Design et ingénierie des systèmes homme-dans-la boucle
auteur
Didier Fass
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
titre
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
auteur
Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
article
Tobias Nipkow and Christian Urban. 22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009, Aug 2009, Munich, Germany. Springer Berlin / Heidelberg, 5674, pp.424-439, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-03359-9_29〉
Accès au bibtex
BibTex
titre
A Refinement Approach for Proving Distributed Algorithms : Examples of Spanning Tree Problems
auteur
Mohamed Tounsi, Ahmed Hadj Kacem, Mohamed Mosbah, Dominique Méry
article
Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Feb 2009, Düsseldorf, Germany
Accès au bibtex
BibTex
titre
Cryptologic protocols analysis using proof-based patterns
auteur
Nazim Benaissa, Dominique Méry
article
Seventh International Andrei Ershov Memorial Conference "PERSPECTIVES OF SYSTEM INFORMATICS" - PSI 2009, Jun 2009, Novosibirsk, Russia. Springer-Verlag, 2009, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Combining Decision Procedures by (Model-)Equality Propagation
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
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〉
Accès au bibtex
BibTex
titre
Model-checking Distributed Applications with GRAS
auteur
Cristian Rosa, Martin Quinson, Stephan Merz
article
Exploiting Concurrency Efficiently and Correctly - EC2 workshop associated to CAV 2009, Jun 2009, Grenoble, France. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00378374/file/modelcheck_ec2-RR.pdf BibTex
titre
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
auteur
Francisco López Fraguas, Stephan Merz, Juan Rodríguez Hortalá
article
22nd International Conference on Theorem Proving in Higher-Order Logics : emerging trends session - TPHOLs 2009, Aug 2009, Munich, Germany. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00408964/file/trends09final.pdf BibTex
titre
A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
auteur
Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz
article
Olivier Bournez and Igor Potapov. Reachability Problems 2009, Sep 2009, Palaiseau, France. Springer Berlin / Heidelberg, 5797, pp.93-106, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04420-5_10〉
Accès au bibtex
BibTex
titre
Pacemaker's Functional Behaviors in Event-B
auteur
Dominique Méry, Neeraj Kumar Singh
article
[Research Report] 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00419973/file/Pacemaker.pdf BibTex
titre
Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm
auteur
Joris Rehm
article
Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Feb 2009, Düsseldorf, Germany. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00362715/file/2009_rehm_simpson2slots.pdf BibTex
titre
Cryptographic Protocols Analysis in Event B
auteur
Nazim Benaissa, Dominique Méry
article
Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Jun 2009, Novosibisrk, Russia. Springer-Verlag, 2009, Lectures Notes in Computer Science
Accès au bibtex
BibTex
titre
A Rodin plugin for quantitative timed models
auteur
Joris Rehm
article
Michael Butler and Stefan Hallerstede and Laurent Voisin. Rodin User and Developer Workshop, Jul 2009, Southampton, United Kingdom. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00431246/file/time_plugin.pdf BibTex
titre
veriT: an open, trustable and efficient SMT-solver
auteur
Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
article
Renate A. Schmidt. 22nd International Conference on Automated Deduction - CADE 22, Aug 2009, Montreal, Canada. Springer Berlin / Heidelberg, 5663, pp.151-156, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02959-2_12〉
Accès au bibtex
BibTex
titre
Automating model-based software engineering
auteur
David Déharbe, Pascal Fontaine, Anamaria Martins Moreira, Stephan Merz, Anderson Santana de Oliveira
article
Colloque d'Informatique: Brésil/INRIA (COLIBRI), Jul 2009, Bento Gonçalves, Brazil. pp.22-27, 2009
Accès au bibtex
BibTex
titre
Combinations of theories for decidable fragments of first-order logic
auteur
Pascal Fontaine
article
Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium, FroCoS 2009, Sep 2009, Trento, Italy. Springer Verlag, 5749, pp.263-278, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04222-5_16〉
Accès au bibtex
BibTex
titre
Model-checking Distributed Applications with GRAS
auteur
Cristian Rosa, Martin Quinson, Stephan Merz
article
[Research Report] RR-7052, INRIA. 2009, pp.11
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00422159/file/main-RR.pdf BibTex
titre
AA4MM coordination model and event-B specification
auteur
Julien Siebert, Joris Rehm, Vincent Chevrier, Laurent Ciarletta, Dominique Méry
article
[Research Report] RR-7081, INRIA. 2009, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00435569/file/RR-7081.pdf BibTex
titre
Développement combiné et prouvé de systèmes transactionnels cryptologiques
auteur
Nazim Benaissa, Dominique Méry
article
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2009, Jan 2009, Toulouse, France. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00426405/file/soumissionbenaissamery.pdf BibTex
titre
A Simple Refinement-based Method for Constructing Algorithms
auteur
Dominique Méry
article
ACM SIGCSE Bulletin, 2009, inroads — SIGCSE Bulletin, 41 (2), pp.51-59. 〈10.1145/1595453.1595462〉
Accès au bibtex
BibTex
titre
Spheres, great circles and parallels
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.80-87
Accès au bibtex
BibTex
titre
MetaPost macros for drawing Chinese and Japanese abaci
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2009, 30 (1), pp.74-79
Accès au bibtex
BibTex
titre
Rationale for human modelling in human in the loop systems design
auteur
Didier Fass, Romain Lieber
article
3rd Annual IEEE International Systems Conference, SysCon 2009, Mar 2009, Vancouver, Canada. IEEE, pp.27-30, 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00394608/file/Rationale_for_human_modeling_in_human_in_the_loop_systems_design.pdf BibTex
titre
Gestion du temps par le raffinement
auteur
Joris Rehm
article
Informatique [cs]. Université Henri Poincaré - Nancy 1, 2009. Français. 〈NNT : 2009NAN10101〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01748288/file/these_Joris-Rehm.pdf BibTex
titre
Prototype Fragments from Babbage's First Difference Engine
auteur
Denis Roegel
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
titre
System-on-chip design by proof-based refinement
auteur
Dominique Cansell, Dominique Méry, Cyril Proch
article
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2009, 11 (3), pp.217-238. 〈10.1007/s10009-009-0104-7〉
Accès au bibtex
BibTex
titre
Formal Verification of a Consensus Algorithm in the Heard-Of Model
auteur
Bernadette Charron-Bost, Stephan Merz
article
International Journal of Software and Informatics (IJSI), ISCAS, 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303. 〈http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=273&flag=1〉
Accès au bibtex
BibTex
titre
Refinement-Based Guidelines for Algorithmic Systems
auteur
Dominique Méry
article
International Journal of Software and Informatics (IJSI), ISCAS, 2009, 3 (2-3), pp.197-239. 〈http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=197&flag=1〉
Accès au bibtex
BibTex

2008

titre
Développement prouvé de structures de données sans verrou
auteur
Loïc Fejoz
article
Modélisation et simulation. Université Henri Poincaré - Nancy I, 2008. Français. 〈NNT : 2009NAN10022〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00594978/file/SCD_T_2009_0022_FEJOZ.pdf BibTex
titre
An introduction to model checking
auteur
Stephan Merz
article
Stephan Merz and Nicolas Navet. Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, ISTE Publishing, pp.81-116, 2008, 9781847040244
Accès au bibtex
BibTex
titre
A TLA+ Proof System
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338299/file/main.pdf BibTex
titre
Formal Verification of Distributed Algorithms in +CAL 2.0
auteur
Sabina Akhtar
article
Master thesis, Master Informatique de Nancy. 2008
Accès au bibtex
BibTex
titre
The Specification Language TLA+
auteur
Stephan Merz
article
Dines Bjørner and Martin Henson. Logics of specification languages, Springer, pp.401-452, 2008, Monographs in Theoretical Computer Science, 978-3-540-74106-0
Accès au bibtex
BibTex
titre
Teaching programming methodology using Event B
auteur
Dominique Méry
article
Henri Habrias. The B Method: from Research to Teaching, Jul 2008, Nantes, France. APCB, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00287231/file/entcsmery.pdf BibTex
titre
Modeling and Verification of Real-Time Systems - Formalisms and Software Tools
auteur
Stephan Merz, Nicolas Navet
article
Stephan Merz and Nicolas Navet. ISTE Publishing, pp.400, 2008, 9781847040244
Accès au bibtex
BibTex
titre
Modelling Attacker's Knowledge for Cascade Cryptographic Protocols
auteur
Nazim Benaissa
article
Egon Börger and Michael Butler and Jonathan P. Bowen and Paul Boca. First International Conference on Abstract State Machines, B and Z - ABZ 2008, Sep 2008, London, United Kingdom. Springer, 5238, pp.251-264, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-87603-8_20〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00336641/file/ABZ2008benaissa.pdf BibTex
titre
Développement incrémental prouvé de systèmes répartis : le cas Mondex
auteur
Nazim Benaissa, Dominique Méry
article
[Rapport de recherche] 2008, pp.13
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00336655/file/benaissamery.pdf BibTex
titre
An Extension of Al-Khalīlī's Qibla Table to the Entire World
auteur
Denis Roegel
article
[Research Report] 2008, pp.781
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00336090/file/khalili-ext.pdf BibTex
titre
Kanji-Sudokus: Integrating Chinese and Graphics
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2008, 29 (2), pp.317-319
Accès au bibtex
BibTex
titre
A Duration Pattern for Event-B Method
auteur
Joris Rehm
article
2nd Junior Researcher Workshop on Real-Time Computing - JRWRTC 2008, Oct 2008, Rennes, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00336320/file/article.pdf BibTex
titre
Combining decision procedures by (model-)equality propagation
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
article
Machado, P. and Andrade, A. and Duran, A. Brazilian Symposium on Formal Methods - SBMF 2008, Aug 2008, Salvador, Bahia, Brazil. 2008
Accès au bibtex
BibTex
titre
Journal of Automated Reasoning Special Issue: Formal Modeling and Verification of Critical Systems
auteur
Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow
article
Tobias Nipkow. 41, Springer, pp.209, 2008, Journal of Automated Reasoning
Accès au bibtex
BibTex
titre
Temporal Logic and State Systems
auteur
Fred Kröger, Stephan Merz
article
Springer, pp.436, 2008, Texts in Theoretical Computer Science. An EATCS Series, 978-3-540-67401-6
Accès au bibtex
BibTex
titre
Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface
auteur
Dominique Cansell, Paul Gibson, Dominique Méry
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 183, pp.39-55. 〈10.1016/j.entcs.2007.01.060〉
Accès au bibtex
BibTex
titre
From Absolute-Timer to Relative-Countdown: Patterns for Model-Checking
auteur
Joris Rehm
article
2008
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00319104/file/Rehm_-_From_Absolute-Timer_to_Relative-Countdown_Patterns_for_Model-Checking.pdf BibTex
titre
The Event-B Modelling Method - Concepts and Case Studies
auteur
Dominique Cansell, Dominique Méry
article
Dines Bjoerner and Martin Henson. Logics of Specification Languages, Springer, pp.33-140, 2008, Monographs in Theoretical Computer Science
Accès au bibtex
BibTex
titre
Intégration de contraintes temps-réel au sein d'un processus de développement incrémental basé sur la preuve (Livrable 2)
auteur
Dominique Cansell, Dominique Méry, Joris Rehm
article
[Rapport de recherche] 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593372/file/RIMEL_Livrable_2.pdf BibTex
titre
Towards automatic proofs of lock-free algorithms
auteur
Loïc Fejoz, Stephan Merz
article
Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00285752/file/ec2-08-fejoz-merz.pdf BibTex
titre
An Early (1844) Key-Driven Adding Machine
auteur
Denis Roegel
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〉
Accès au bibtex
BibTex
titre
A MYB transcription factor regulates very-long-chain fatty acid biosynthesis for activation of the hypersensitive cell death response in Arabidopsis
auteur
Sylvain Raffaele, Fabienne Vailleau, Amandine Leger, Jérôme Joubès, Otto Miersch, Carine Chauveau, Elisabeth Blée, Sébastien Mongrand, Frédéric Domergue, Dominique Roby
article
Plant Cell, American Society of Plant Biologists, 2008, 20 (3), pp.752-767. 〈10.1105/tpc.107.054858〉
Accès au bibtex
BibTex

2007

titre
Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)
auteur
Stephan Merz, Tobias Nipkow
article
Michael Mislove. 185, Elsevier, pp.151, 2007, Electronic Notes in Theoretical Computer Science
Accès au bibtex
BibTex
titre
Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions
auteur
Clément Hurlin, Amine Chaib, Pascal Fontaine, Stephan Merz, Tjark Weber
article
Lucas Dixon, Moa Johansson. The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13, 2007, The 21st Conference on Automated Deduction - CADE-21
Accès au bibtex
BibTex
titre
haRVey : satisfaisabilité et théories
auteur
Diego Caminha B. De Oliveira, David Déharbe, Pascal Fontaine
article
Marie-Laure Potet, Pierre-Yves Schobbens, Hubert Toussaint, Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. pp.287-288, 2007, Actes de la 8e conférence - AFADL Approches Formelles dans l'Assistance au
Accès au bibtex
BibTex
titre
Patrons de conception prouvés
auteur
Thierry Lecomte, Dominique Méry, Dominique Cansell
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
titre
Formal verification of tamper-evident storage for e-voting
auteur
Dominique Cansell, Paul Gibson, Dominique Méry
article
Mike Hinchey and Tiziana Margaria. 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. IEEE, pp.329-338, 2007, Fifth IEEE International Conference on Software Engineering and Formal Methods, 2007. SEFM 2007. 〈10.1109/SEFM.2007.21〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00184833/file/mery-e-voting.pdf BibTex
titre
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method
auteur
Joris Rehm, Dominique Cansell
article
Yamine Aït-Ameur, Frederic Boniol and Virginie Wiels. ISoLA 2007 Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Dec 2007, Poitiers-Futuroscope, France. Cépaduès, RNTI-SM-1, pp.179-190, 2007
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00184837/file/article.pdf BibTex
titre
Vérification formelle d'algorithmes distribués en +CAL
auteur
Sebti Mouelhi
article
Mémoire de master recherche en informatique de Lorraine. 2007
Accès au bibtex
BibTex
titre
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class
auteur
Pascal Fontaine
article
Bernhard Beckert. 4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. 259, pp.37-54, 2007, CEUR Workshop Proceedings
Accès au bibtex
BibTex
titre
Spécification et vérification des propriétés de vivacité en B événementiel
auteur
Olfa Mosbahi, Jacques Jaray, Samir Ben Ahmed
article
6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2007, Oct 2007, Lyon, France. 16 p., 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00172417/file/MSR2007.pdf BibTex
titre
Three dials, and a few more: a practical introduction to accurate gnomonics
auteur
Denis Roegel
article
[Technical Report] 2007, pp.70
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00172407/file/article-sundials.pdf BibTex
titre
Validating and Animating Higher-Order Recursive Functions in B
auteur
Michael Leuschel, Dominique Cansell, Michael Butler
article
Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS
Accès au bibtex
BibTex
titre
Designing old and new distributed algorithms by replaying an incremental proof-based development
auteur
Dominique Cansell, Dominique Méry
article
Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS
Accès au bibtex
BibTex
titre
The LaTeX Graphics Companion, Second Edition - Tools and Techniques for Computer Typesetting
auteur
Michel Goossens, Frank Mittelbach, Sebastian Rahtz, Denis Roegel, Herbert Voss
article
Addison-Wesley, pp.976, 2007, ISBN-10: 0321508920 / ISBN-13: 978-0321508928
Accès au bibtex
BibTex
titre
A complex drawing in descriptive geometry
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2007, 28 (2), pp.218-228
Accès au bibtex
BibTex
titre
Développement formel de circuits électroniques par la méthode B
auteur
Yann Zimmermann
article
Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, pp.181-198, 2007, Actes de la 8e conférence AFADL - Approches Formelles dans l'Assistance au Développement de Logiciels
Accès au bibtex
BibTex
titre
Incremental Parametric Development of Greedy Algorithms
auteur
Dominique Cansell, Dominique Méry
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〉
Accès au bibtex
BibTex
titre
Tool supported real-time system verification with combination of abstraction/deduction and model checking
auteur
Eunyoung Kang
article
Software Engineering [cs.SE]. Université Henri Poincaré - Nancy I, 2007. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00195096/file/thesis.pdf BibTex
titre
Dérivation d'algorithmes sans verrou à partir d'une spécification atomique
auteur
Loïc Fejoz, Stephan Merz
article
Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, 2007, pp.213-226, 2007, Actes de la 8e conférence AFADL Approches Formelles dans l'Assistance au Développement de Logiciels
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00162146/file/afadl07-fejoz-merz.pdf BibTex
titre
Modelling and Proof Analysis of Interrupt Driven Scheduling
auteur
Bill Stoddart, Dominique Cansell, Frank Zeyda
article
Jacques Jullian et Olga Kouchnarenko. The 7th International B Conference - B 2007, Jan 2007, Besançon/France, Springer, 4355/2006, pp.155-170, 2007, LNCS. 〈10.1007/11955757_14〉
Accès au bibtex
BibTex
titre
Specification and Proof of Liveness Properties in B Event Systems
auteur
Olfa Mosbahi, Jacques Jaray
article
Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.25-34, 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00158906/file/mosbahi_381.pdf BibTex
titre
A Formal Approach for the Development of Automated Systems
auteur
Olfa Mosbahi, Leila Jemni, Jacques Jaray
article
Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.304-310, 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00158908/file/paper_382.pdf BibTex
titre
Sphères, grands cercles et parallèles
auteur
Denis Roegel
article
Cahiers Gutenberg, Association GUTenberg, 2007, Avril 2007 (48), pp.7-22
Accès au bibtex
BibTex
titre
Proved-Patterns-Based Development for Structured Programs.
auteur
Dominique Cansell, Dominique Méry
article
Volker Diekert and Mikhail V. Volkov and Andrei Voronkov. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Sep 2007, Ekaterinburg, Russia. Springer Berlin / Heidelberg, 4649, pp.104-114, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74510-5_13〉
Accès au bibtex
BibTex
titre
Secure Information Flow for a Concurrent Language with Scheduling
auteur
Gilles Barthe, Leonor Prensa Nieto
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
titre
Specification and Refinement of Access Control
auteur
Dominique Méry, Stephan Merz
article
Journal of Universal Computer Science, Springer, 2007, 13 (8), pp.1073-1093
Accès au bibtex
BibTex
titre
Integration of Security Policy into System Modeling
auteur
Nazim Benaissa, Dominique Cansell, Dominique Mery
article
The 7th International B Conference - B2007, Jan 2007, Besançon, France, 2007
Accès au bibtex
BibTex
titre
Time Constraint Patterns for Event B Development
auteur
Dominique Cansell, Dominique Méry, Joris Rehm
article
Jacques Julliand, Olga Kouchnarenko. 7th International Conference of B Users, January 17-19, 2007, 2007, Besançon, France. Springer-Verlag, 4355, pp.140-154, 2007, Lecture Notes in Computer Science. 〈10.1007/11955757_13〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00149163/file/B2007cansellmeryrehm.pdf BibTex
titre
Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools
auteur
Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.321-341. 〈10.1007/s00165-007-0027-6〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00097383/file/fac07.pdf BibTex
titre
Predicate Diagrams for the Verification of Real-Time Systems
auteur
Eunyoung Kang, Stephan Merz
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.401-413. 〈10.1007/s00165-007-0030-y〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00112065/file/0819.pdf BibTex
titre
Review of ``Mathematical Illustrations: A Manual of Geometry and PostScript
auteur
Denis Roegel
article
Notices of the American Mathematical Society, American Mathematical Society, 2007, 54 (1), pp.38-42
Accès au bibtex
BibTex

2006

titre
Model checking : éléments de base
auteur
Stephan Merz
article
Nicolas Navet. Systèmes Temps Réel - techniques de description et de vérification, Hermes-Science Lavoisier, pp.89-120, 2006, 2-7462-1303-6
Accès au bibtex
BibTex
titre
How to Verify and Exploit a Refinement of Component-based Systems
auteur
Olga Kouchnarenko, Arnaud Lanoix
article
[Research Report] RR-5898, INRIA. 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071369/file/RR-5898.pdf BibTex
titre
Formal specification of safe manufacturing machines using the B method : application to a mechanical press
auteur
Dominique Evrot, Jean-François Pétin, Dominique Méry
article
IFAC. May 2006, Elsevier, pp.CDROM, 2006
Accès au bibtex
BibTex
titre
Proof reconstruction for first-order logic and set-theoretical constructions
auteur
Clément Hurlin
article
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.157-162, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00091811/file/p.pdf BibTex
titre
haRVey: combining reasoners
auteur
David Déharbe, Pascal Fontaine
article
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00091662/file/avocs.pdf BibTex
titre
A method to refine time constraints in event B framework
auteur
Joris Rehm
article
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.173-177, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00091665/file/avocs.pdf BibTex
titre
Incremental Parametric Development of Greedy Algorithms
auteur
Dominique Cansell, Dominique Méry
article
Stephan Merz and Tobias Nipkow. 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00089497/file/canselmeryavocs.pdf BibTex
titre
Tutorial on the event-based B method
auteur
Dominique Cansell, Dominique Méry
article
IFIP FORTE 2006 Paris, 2006
Accès au texte intégral et bibtex
https://cel.archives-ouvertes.fr/inria-00092846/file/tutorialforte2006mery.pdf BibTex
titre
Event B
auteur
Dominique Cansell, Dominique Méry
article
Henri Habrias and Marc Frappier. Software Specification Methods, HERMES, 2006, 1-905209-34-7
Accès au bibtex
BibTex
titre
B Method
auteur
Dominique Cansell
article
Freek Wiedijk. The Seventeen Provers of the World, 3600 (3600), Springer Berlin / Heidelberg, pp.142-150, 2006, LNAI, 978-3-540-30704-4. 〈10.1007/11542384_18〉
Accès au bibtex
BibTex
titre
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
auteur
Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Tiu
article
Holger Hermanns and Jens Palsberg. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, Springer, 3920, pp.167-181, 2006, Lecture Notes in Computer Science. 〈10.1007/11691372_11〉
Accès au bibtex
BibTex
titre
How to Verify and Exploit a Refinement of Component-based Systems
auteur
Olga Kouchnarenko, Arnaud Lanoix
article
Sixth International Andrei Ershov Memorial Conference Perspectives Of System Informatics (PSI'06), 2006, Novosibirsk, Akademgorodok, Russia, France. Springer Verlag, 4378, pp.457-469, 2006, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Transformation of B Specifications into UML Class Diagrams and State Machines
auteur
Houda Fekih, Leila Jemni Ben Ayed, Stephan Merz
article
21st Annual ACM Symposium on Applied Computing - SAC 2006, Apr 2006, Dijon, France, ACM, 2, pp.1840-1844, 2006, Applied Computing 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001269/file/final.pdf BibTex
titre
Event Systems and Access Control
auteur
Dominique Méry, Stephan Merz
article
Dieter Gollmann and Jan Jürjens. Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, Mar 2006, Vienna/Austria, Vienna University of Technology, pp.40-54, 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001262/file/final.pdf BibTex
titre
Decision Procedures for the Formal Analysis of Software
auteur
David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
article
Kamel Barkaoui, Ana Cavalcanti, Antonio Cerone. 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, Nov 2006, Tunis, Tunisia, Springer, 4281, pp.366--370, 2006, Lecture Notes in Computer Science. 〈10.1007/11921240_26〉
Accès au bibtex
BibTex
titre
Specification and Refinement of Mobile Systems in MTLA and Mobile UML
auteur
Alexander Knapp, Stephan Merz, Martin Wirsing, Julia Zappe
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
titre
Formal Development Method of Automated Systems using the Temporal Logic of Actions TLA
auteur
Olfa Mosbahi, Leila Jemni Ben Ayed, Jacques Jaray
article
MOSIM'06 6ième Conférence Francophone de Modélisation et Simulation des Systèmes, Apr 2006, Rabat, Morocco. 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00102229/file/Mosbahi_MOSIM06.pdf BibTex
titre
A Formal Development Method of Control Systems using Event B Approach
auteur
Olfa Mosbahi, Jacques Jaray, Leila Jemni Ben Ayed
article
4th ACS/IEEE International Conference on Computer Systems and Applications, Mar 2006, DUBAI, 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00102208/file/Mosbahi_AICCSA06.pdf BibTex
titre
A formal development approach of control systems using the event based B approch, Case study : A parcel sorting device
auteur
Olfa Mosbahi, Jacques Jaray, Leila Jemni Ben Ayed
article
The 4th ACS/IEEE International Conference on Computer Systems and Applications - AICCSA'2006, Mar 2006, Dubai/Sharjah, UAE, 2006
Accès au bibtex
BibTex
titre
Formal and Incremental Construction of Distributed Algorithms: On the Distributed Reference Counting Algorithm
auteur
Dominique Cansell, Dominique Méry
article
Theoretical Computer Science, Elsevier, 2006
Accès au bibtex
BibTex

2005

titre
The invoice case study modelling in Event B
auteur
Dominique Cansell, Dominique Méry
article
[Research Report] 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000857/file/eventb.pdf BibTex
titre
Refinement and Reachability in Event_B
auteur
Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
article
Helen Treharne, Steve King, Martin Henson, Steve Schneider. ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users, Apr 2005, Guilford/UK, Springer, 3455, pp.222-241, 2005, Lecture Notes in Computer Science. 〈10.1007/11415787_14〉
Accès au bibtex
BibTex
titre
MP2GL: prototyping 3D objects with METAPOST and OpenGL
auteur
Denis Roegel
article
15ème Rencontre annuelle des utilisateurs européens de TeX - EuroTeX 2005, Mar 2005, Pont-à-Mousson/France, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00001243/file/eurotex2005roegel.pdf BibTex
titre
The challenge of QoS for digital television services
auteur
Dominique Méry, Dominique Cansell, Cyril Proch, Denis Abraham, Patrick Ditsch
article
EBU Technical Review, European Broadcasting Union, 2005, 302 (Avril), 11 p
Accès au bibtex
BibTex
titre
A Formalization of a Generalized Clock Synchronization Protocol in Isabelle/HOL
auteur
Alwen Tiu
article
2005
Accès au bibtex
BibTex
titre
Un système d'analyse de la qualité: de la norme au produit en passant par le raffinement
auteur
Dominique Cansell, Dominique Méry, Cyril Proch
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
titre
Predicate Diagrams for the Verification of Real-Time Systems
auteur
Eunyoung Kang, Stephan Merz
article
Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou. The Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS'05, Sep 2005, Coventry/UK, Elsevier, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000631/file/final.pdf BibTex
titre
Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools
auteur
Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu
article
Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS '05, Sep 2005, Coventry/UK, Elsevier, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000638/file/barsotti_prensa_tiu.pdf BibTex
titre
Real-Time system verification techniques based on abstraction/deduction and model checking
auteur
Eunyoung Kang
article
Judi Romijn. Doctoral Symposium of the Fifth International Conference on Integrated Formal Methods - IFM'2005, Nov 2005, Eindhoven/The Netherlands, 2005, Technical Report of MCS, TU-Eindhoven
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000641/file/kangifm2.pdf BibTex
titre
Simple algorithms for preemptive traffic control, and an appraisal of their quality
auteur
Denis Roegel
article
[Research Report] 2005, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000658/file/streetcar.pdf BibTex
titre
Kissing Circles: A French Romance in METAPOST
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2005, 26 (1), pp.10-17
Accès au bibtex
BibTex
titre
Modelling SystemC scheduler by refinement
auteur
Dominique Cansell, Dominique Méry, Cyril Proch
article
IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05, Sep 2005, Columbia/USA, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000564/file/cansellmeryprochisola2005.pdf BibTex
titre
Synthesis of the QoS for digital TV services
auteur
Denis Abraham, Dominique Cansell, Patrick Ditsch, Dominique Méry, Cyril Proch
article
First International Workshop on Incentive Based Computing - IBC'05, Sep 2005, Amsterdam/Hollande, 2005
Accès au bibtex
BibTex
titre
Combining Lists with Non-Stably Infinite Theories
auteur
Pascal Fontaine, Silvio Ranise, Calogero Zarba
article
Franz Baader; Andrei Voronkov. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), Mar 2005, Montevideo/Uruguay, Springer-Verlag, 3452, pp.51--66, 2005, Lecture Notes in Computer Science. 〈10.1007/b106931〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000481/file/FontaineRaniseZarba.pdf BibTex
titre
Truly On-The-Fly LTL Model Checking
auteur
Moritz Hammer, Alexander Knapp, Stephan Merz
article
Nicolas Halbwachs, Lenore D. Zuck. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Apr 2005, Edinburgh / U.K., Springer, 3440, pp.191-205, 2005, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000753/file/final.pdf BibTex
titre
Component Reuse in B Using ACL2
auteur
Yann Zimmermann, Diana Toma
article
Helen Treharne, Steve King, Martin Henson, Steve Schneider. ZB Formal Specification and Development in Z and B - 4th International Conference of B and Z Users - ZB 2005, Apr 2005, University of Surrey, Guildford, UK, Springer-Verlag GmbH, 3455, pp.280-299, 2005, Lecture Notes in Computer Science. 〈10.1007/b135596〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000755/file/34550281.pdf BibTex
titre
DIXIT: a Graphical Toolkit for Predicate Abstractions
auteur
Loïc Fejoz, Dominique Méry, Stephan Merz
article
Ramesh Bharadwaj and Supratik Mukhopadhyay. Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000767/file/workshop-paper.pdf BibTex
titre
A Formal development approach of control systems using the event-based B approach
auteur
Olfa Mosbahi, Leila Jemni Ben Ayed, Samir Ben Ahmed
article
Third International Conference on Informatics and Systems - INFOS'2005, Mar 2005, Caire, Egypte, 2005
Accès au bibtex
BibTex
titre
Utilisation conjointe de B et TLA+ pour la modélisation et la vérification des systèmes réactifs
auteur
Olfa Mosbahi, Leila Jemni Ben Ayed
article
Premières Rencontres des Jeunes Chercheurs en Informatique Temps Réel 2005 - RJCITR'05, Sep 2005, Nancy, France. pp.31-34, 2005
Accès au bibtex
BibTex
titre
Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity)
auteur
Jean-Raymond Abrial, Dominique Cansell
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

2004

titre
Refining Mobile UML State Machines
auteur
Alexander Knapp, Stephan Merz, Martin Wirsing
article
Charles Rattray and Savitri Maharaj and Carron Shankland. 10th International Conference on Algebraic Methodology and Software Technology - AMAST'2004, 2004, Stirling, Scotland, UK, Springer-Verlag, 3116, pp.274--288, 2004, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Transformation des spécifications B en des diagrammes UML
auteur
Houda Fekih, Leila Jemni, Stephan Merz
article
Jacques Julliand. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'2004, 2004, Besançon, France, Impression Burs, pp.131-145, 2004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107777/file/A04-R-085.pdf BibTex
titre
Derivation of SystemC code from abstract system models
auteur
Dominique Cansell, Jean-François Culat, Dominique Méry, Cyril Proch
article
Forum on specification and Design Languages - FDL'04, 2004, Lille, France, 12 p, 2004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107780/file/A04-R-091.pdf BibTex
titre
TLA+ Case Study: A Resource Allocator
auteur
Stephan Merz
article
[Intern report] A04-R-101 || merz04a, 2004, 20 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107809/file/A04-R-101.pdf BibTex
titre
Projet RNRT EQUAST ; SP2 Spécification incrémentale du système
auteur
Cyril Proch, Dominique Cansell, Dominique Mery
article
[Interne] A04-R-237 || proch04a, 2004
Accès au bibtex
BibTex
titre
Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems
auteur
Gilles Barthe, Leonor Prensa Nieto
article
2nd ACM Workshop on Formal Methods in Security Engineering - FMSE'2004, Oct 2004, Washington D.C./USA, ACM Press, pp.13-22, 2004, Proceedings of the 2004 ACM workshop on Formal methods in security engineering. 〈10.1145/1029133.1029136〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000632/file/p21-barthe.pdf BibTex
titre
Développement formel de systèmes de contrôle-commande.
auteur
Olfa Mosbahi, Jacques Jaray
article
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2004, Jun 2004, Besançon/France, 2004
Accès au bibtex
BibTex
titre
Représentation du temps en B événementiel pour la modélisation des systèmes de temps réel.
auteur
Olfa Mosbahi, Jacques Jaray
article
[Interne] 2004
Accès au bibtex
BibTex
titre
Une démarche formelle de développement de systèmes de contrôle-commande.
auteur
Olfa Mosbahi, Jacques Jaray
article
[Interne] 2004
Accès au bibtex
BibTex
titre
The missing new moon of A.D. 16399 and other anomalies of the Gregorian calendar
auteur
Denis Roegel
article
[Intern report] A04-R-436 || roegel04a, 2004, 15 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00099868/file/A04-R-436.pdf BibTex
titre
The First Key-driven Calculating Machine (1844)
auteur
Denis Roegel
article
[Intern report] A04-R-437 || roegel04b, 2004, 8 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00099869/file/A04-R-437.pdf BibTex
titre
Formal modelling of electronic circuits using event-B, Case Study: SAE J1708 Serial Communication Link
auteur
Yann Zimmermann, Stefan Hallerstede, Dominique Cansell
article
Jean Mermet. UML-B - Specification for Proven Embedded Systems Design, Kluwer Academic Publishers, 2004
Accès au bibtex
BibTex
titre
Circuit Design by Refinement in EventB
auteur
Stefan Hallerstede, Yann Zimmermann
article
Forum on Specification and Design Languages - FDL'04, 2004, Lille, France, 13 p, 2004
Accès au bibtex
BibTex
titre
Construction sûre de systèmes électroniques
auteur
Dominique Cansell, Stefan Hallerstede, Yann Zimmermann
article
Génie logiciel, C & S, 2004, pp.38-44
Accès au bibtex
BibTex
titre
UML-B specification and hardware implementation of a Hamming coder/decoder
auteur
Dominique Cansell, Stefan Hallerstede, Ian Oliver
article
Jean Mermet. UML-B - Specification for Proven Embedded Systems Design, Kluwer Academic Publishers, 2004
Accès au bibtex
BibTex
titre
Synthèse formelle par raffinement de modèles et de logiciels pour l'automaisation
auteur
Dominique Méry
article
Journées d'Etude "Automatique et Informatique", 2004, Cachan, France, 2004
Accès au bibtex
BibTex
titre
Tutorial on the event-based B method : Concepts and Case Studies
auteur
Dominique Cansell, Dominique Méry
article
Dines Bjoerner and Martin Henson. Logics of Formal Software Specification Languages - LFSL'2004, 2004, The High Tatras, Slovakia, 2004
Accès au bibtex
BibTex
titre
Proof-Oriented Fault-Tolerant Systems Engineering : Rationales, Experiments and Open Issues
auteur
Gérard Morel, Dominique Méry, Jean-Baptiste Léger, Thierry Lecomte
article
7th IFAC Symposium on Cost Oriented Automation - COA'2004, 2004, Gatineau, Québec, Canada. 2004
Accès au bibtex
BibTex

2003

titre
Emptiness of Linear Weak Alternating Automata
auteur
Stephan Merz, Ali Sezgin
article
[Intern report] A03-R-503 || merz03c, 2003, 14 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107750/file/A03-R-503.pdf BibTex
titre
Solving Layout Problems Concurrently With TeX and Java
auteur
Denis Roegel
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
titre
Translating B machines into UML diagrams
auteur
Houda Fekih, Stephan Merz
article
[Intern report] A03-R-502 || fekih03a, 2003, 13 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107751/file/A03-R-502.pdf BibTex
titre
The QSL platform at LORIA
auteur
Mohamed El Habib, Claude Kirchner, Hélène Kirchner, Jean-Yves Marion, Stephan Merz
article
First QPQ Workshop on Deductive Software Components, 2003, Miami, Floride, 3 p, 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00099497/file/A03-R-539.pdf BibTex
titre
Modélisation des systèmes réactifs
auteur
Dominique Méry, Nidhal Rezg, Xiaolan Xie
article
Méry, Dominique et Rezg, Nidhal et Xie, Xiaolan. 4ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2003, 2003, Metz, France, Hermès, 568 p, 2003
Accès au bibtex
BibTex
titre
Modélisation formelle de circuits électroniques en B événementiel
auteur
Yann Zimmermann
article
Manifestation des Jeunes Chercheurs du domaine des STIC 2003 -MAJECSTIC'03, 2003, Marseille, France, 2003
Accès au bibtex
BibTex
titre
Formal derivation of spanning trees algorithms
auteur
Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
article
Didier Bert, Jonathan Peter Bowen, Steve King, Marina Walden. Third International Conference of B and Z Users - ZB'2003, 2003, Turku, Finland, Springer Verlag, 2651, pp.457-476, 2003, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Foundations of the B method
auteur
Dominique Cansell, Dominique Méry
article
Computers and Informatics, 2003, 22, 31 p
Accès au bibtex
BibTex
titre
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems
auteur
Stephan Merz, Martin Wirsing, Julia Zappe
article
Mauro Pezze. Fundamental Approaches to Software Engineering '03 - FASE 2003, 2003, Warsaw, Poland, Springer-Verlag, 2621, pp.87-101, 2003
Accès au bibtex
BibTex
titre
On the Logic of TLA+
auteur
Stephan Merz
article
Computers and Informatics, 2003, 22 (4), 27 p
Accès au bibtex
BibTex
titre
Proof-based design of a microelectronic architecture for MPEG-2 bit-rate measurement
auteur
Dominique Cansell, Camel Tanougast, Yves Berviller, Dominique Méry, Cyril Proch, Hassan Rabah, Serge Weber
article
Forum on specification and Design Languages - FDL'03, 2003, Frankfurt, Germany, France. 12 p, 2003
Accès au bibtex
BibTex
titre
Designing event-driven systems by combining coordination and refinement
auteur
Dominique Cansell, Dominique Méry
article
2nd International Workshop on Refinement of Critical Systems: Methods, Tools and Developments - RCS'03, 2003, Turku, Finland, 2003
Accès au bibtex
BibTex
titre
Click'n'Prove: Interactive Proofs Within Set Theory
auteur
Jean-Raymond Abrial, Dominique Cansell
article
David Basin et Burkhart Wolff. 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, 2003, Rome, Italy, Springer, 2758, pp.1-24, 2003, Lecture notes in Computer Science
Accès au bibtex
BibTex
titre
A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol
auteur
Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
article
Formal Aspects of Computing, Springer Verlag, 2003, 14 (3), pp.215-227
Accès au bibtex
BibTex

2002

titre
Formalisation of enterprise modelling standards using UML and the B method.
auteur
Hervé Panetto, Jean-François Pétin, Dominique Méry
article
8th International Conference on Concurrent Enterprising, ICE2002, Jun 2002, Rome, Italy. ESOCE, pp.93-101, 2002, ISBN : 0 85358 113 4
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00120944/file/panetto_et_al_ice2002.pdf BibTex
titre
A Scalable Approach to Network Enabled Servers
auteur
Eddy Caron, Philippe Combes, Sylvain Contassot-Vivier, Frédéric Desprez, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
[Research Report] RR-2002-21, LIP - ENS Lyon. 2002
Accès au bibtex
BibTex
titre
A Scalable Approach to Network Enabled Servers
auteur
Eddy Caron, Frédéric Desprez, Frédéric Lombard, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
B. Monien and R. Feldmann. 8th International EuroPar Conference, 2002, Paderborn, Germany. Springer-Verlag, 2400, pp.4, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Une approche hiérarchique des serveurs de calculs
auteur
Eddy Caron, Frédéric Desprez, Eric Fleury, Frédéric Lombard, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
Françoise Baude. Calcul réparti à grande échelle, Hermès Science Paris, pp.23, 2002, 2-7462-0472-X
Accès au bibtex
BibTex
titre
Higher-Order" Mathematics in B
auteur
Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte
article
D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB'2002, Jan 2002, Grenoble, France, Springer, 2272, pp.370-393, 2002, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Développement de fonctions définies récursivement en B : Application du B événementiel
auteur
Dominique Cansell, Dominique Méry
article
[Interne] A02-R-347 || cansell02b, 2002, 25 p
Accès au bibtex
BibTex
titre
Integration of the proof process in the system development through refinement steps
auteur
Dominique Cansell, Dominique Méry
article
Eugenio Villar. 5th Forum on Specification and Design Language - Workshop SFP in FDL'02, 2002, Marseille, France, 12 p, 2002
Accès au bibtex
BibTex
titre
Incremental Proof of the Producer/Consumer Property for the PCI Protocol
auteur
Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Méry, Airy Weinzoepflen
article
D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB 2002, 2002, Grenoble, France, Springer, 2272, pp.22-41, 2002, Lectures Notes in Computer Science
Accès au bibtex
BibTex
titre
METAOBJ: Very High-Level Objects in METAPOST
auteur
Denis Roegel
article
23rd Annual Meeting and Conference of the TEX Users Group - TUG 2002, 2002, Trivandrum, India, 2002
Accès au bibtex
BibTex
titre
A Specification and Validation Technique Based on STATEMATE and FNLOG
auteur
Olfa Mosbahi, Leila Jemni Ben Ayed, Samir Ben Ahmed, Jacques Jaray
article
Chris George and Huaikou Miao. 4th International Conference on Formal Engineering Methods - ICFEM 2002, Oct 2002, Shanghai, China. Springer - Verlag GmbH, 2495, pp.216-220, 2002, Lecture Notes in Computer Science. 〈10.1007/3-540-36103-0_23〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00102167/file/Mosbahi_ICFEM02.pdf BibTex
titre
ÉCRITURES EN LIGNE: PRATIQUES ET COMMUNAUTÉS. Sous la dir de Brigitte Chapelain. (485 p.)
auteur
Brigitte Chapelain, Jean Clément, Xavier Malbreil, Jean-Max Noyer, Henri Hudrisier, Laura-Borras Castanyer, Franck Cormerais, Marc Silberstein, Alexandre Peraud, Evelyne Broudoux, Annie Gentes, Jean-Claude Moissinac, Paul Fourmentraux, F. Rakotonoelina, Sylvie Catellin, Annabelle Klein, Philippe Quinton, Florence Bailly, Thierry Dezelay, Catherine Peyrard, Fabienne Martin-Juchat, Valérie Lépine, Véronique Mattio, Patrick Rebollar, Gisèle Tessier, Christian Derrien, Jean Marc Turban, Isabelle Rieusset-LemariÉ, Joa Elies Adell, Olivier Galibert, Alexandre Serres, François Lermigeaux, Béatrice Drot-Delange, Hassan Attifi, Michel Marcoccia, Émilie Moreau, Michel Moatti, Lionel Dax
article
Université de Rennes 2, 486p., 2002
Accès au texte intégral et bibtex
https://archivesic.ccsd.cnrs.fr/sic_00126719/file/Actes_2_collo_ecritures_def2.pdf BibTex

2001

titre
SCILAB to SCILAB// - The Ouragan Project
auteur
Eddy Caron, Serge Chaumette, Sylvain Contassot-Vivier, Frédéric Desprez, Eric Fleury, Claude Gomez, Maurice Goursat, Emmanuel Jeannot, Dominique Lazure, Frédéric Lombard, Jean-Marc Nicod, Laurent Philippe, Martin Quinson, Pierre Ramet, Jean Roman, Franck Rubi, Serge Steer, Frederic Suter, Gil Utard
article
[Research Report] RR-2001-24, LIP - ENS Lyon. 2001
Accès au bibtex
BibTex
titre
The METAOBJ tutorial and reference manual
auteur
Denis Roegel
article
A01-R-406 || roegel01c. This manual describes METAOBJ, a system for high-level object-oriented drawing based on METAPOST. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107539/file/A01-R-406.pdf BibTex
titre
Code Generation From Hierarchical Concurrency Specifications
auteur
Denis Roegel, Scott Smolka
article
[Intern report] A01-R-404 || roegel01a, 2001, 23 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107548/file/A01-R-404.pdf BibTex
titre
Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams
auteur
Dominique Cansell, Dominique Méry, Stephan Merz
article
Martin Wirsing. Integrating Diagrammatic and Formal Specification Techniques, 2001, Wien, Austria, pp.39-45, 2001
Accès au bibtex
BibTex
titre
Utilisation de B pour l'aide à la spécification d'un système de diagnostic
auteur
Dominique Cansell, Jacques Jaray, Dominique Mery
article
Approche Formelles dans l'Assistance au Développement de Logiciels - AFADl'2001, Jun 2001, Nancy, France, 15 p, 2001
Accès au bibtex
BibTex
titre
Modélisation et analyse de la documentation technique d'un système
auteur
Dominique Cansell, Dominique Méry, Airy Weinzoepflen
article
Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2001, 2001, Toulouse, France, Hermes, 16 p, 2001
Accès au bibtex
BibTex
titre
Anatomy of a macro
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2001, 22 (1-2), pp.78-82
Accès au bibtex
BibTex
titre
La géométrie dans l'espace avec METAPOST
auteur
Denis Roegel
article
Cahiers Gutenberg, Association GUTenberg, 2001, 39-40, pp.107-138
Accès au bibtex
BibTex
titre
Specification and Design of the Leader Election Protocol of IEEE 1394
auteur
Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
article
S. Maharaj and J. Romijn and C. Shankland. IEEE 1394 (FireWire) Workshop: International Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001, Berlin, Germany, University of Stirling, 3 p, 2001
Accès au bibtex
BibTex
titre
Développement Incrémental Prouvé de Systèmes
auteur
Airy Weinzoepflen
article
[Intership report] A01-R-315 || weinzoepflen01a, 2001, 51 p
Accès au bibtex
BibTex
titre
METAPOST, l'intelligence graphique
auteur
Denis Roegel
article
Cahiers Gutenberg, Association GUTenberg, 2001, pp.5-16
Accès au bibtex
BibTex
titre
Space geometry with MetaPost
auteur
Denis Roegel
article
Tugboat, TeX Users Group, 2001, 22 (4), pp.298-314
Accès au bibtex
BibTex

2000

titre
Predicate diagrams for the verification of reactive systems
auteur
Dominique Cansell, Dominique Méry, Stephan Merz
article
W. Grieskamp, T. Santen, B. Stoddart. Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, Springer-Verlag, 1945, pp.380-397, 2000, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Playing with abstraction and refinement for managing features interactions. A methodological approach to feature interaction problem
auteur
Dominique Cansell, Dominique Méry
article
Jonathan P. Bowen & Steve Dunne & Andy Galloway & Steve King. International Conference on B & Z Users - ZB'2000, 2000, York, GB, Springer-Verlag, 1878, pp.148-167, 2000, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Verifying Reactive Systems Using Predicate Diagrams
auteur
Dominique Cansell, Dominique Méry, Stephan Merz
article
Wolfgang Reif & Gerhard Schellhorn. FM-TOOLS'2000, 2000, Ulm, 5 p, 2000
Accès au bibtex
BibTex
titre
Abstraction and Refinement of Concurrent Programs and Formal Specification
auteur
Dominique Cansell, Dominique Méry, Christophe Tabacznyj
article
Jose Rolim et al. Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, 2000, Cancun, Mexico, Springer-Verlag, 1800, pp.1037-1038, 2000, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Predicate diagrams
auteur
Dominique Cansell, Dominique Méry, Stephan Merz
article
M.V. Cengarle. Workshop on Requirement, Design, Correct Construction & Verification, 2000, Munich, Germany, 2000
Accès au bibtex
BibTex
titre
Abstraction and refinement of features
auteur
Dominique Cansell, Dominique Méry
article
Stephen, Gilmore et Mark, Ryan. Language Constructs for Designing Features, Springer, 2000
Accès au bibtex
BibTex
titre
Diagrams Refinement for the Design of Reactive Systems
auteur
Dominique Cansell, Dominique Méry, Stephan Merz
article
Journal of Universal Computer Science, Springer, 2000, 7 (2), pp.159-174
Accès au bibtex
BibTex
titre
A taxonomy for triggered interactions using fair object semantics
auteur
Paul Gibson, Geoff Hamilton, Dominique Méry
article
M. Calder & E. Magill. Feature Interactions in Telecommunications & Software Systems VI, 2000, Glasgow, UK, IOS Press, 20 p, 2000
Accès au bibtex
BibTex
titre
A Data-Parallel Implementation of the Gauss-Seidel Iteration Method Applied to the Sliding Box Problem
auteur
Jacques Jaray, Olivier Galibert
article
[Intern report] A00-R-085 || jaray00a, 2000, 14 p
Accès au bibtex
BibTex
titre
Fixing Race Condition Errors with Formal Techniques. A Case Study in Concurrent Java Programming
auteur
Jacques Jaray
article
[Intern report] A00-R-086 || jaray00b, 2000, 13 p
Accès au bibtex
BibTex
titre
Fair Objects
auteur
John Paul Gibson, Dominique Méry
article
H. Zedan & A. Cau. Object-oriented technology and computing systems re-engineering, Horwood Publishing Ltd, 2000, Computer Science & Electronic Engineering
Accès au bibtex
BibTex
titre
Rapport final de contrat Cifre entre le LORIA et Peugeot SA et de contrat d'expertise sur l'utilisation de la méthode B.
auteur
Dominique Cansell, Jacques Jaray, Dominique Méry
article
[Contrat] A00-R-047 || cansell00a, 2000, 34 p
Accès au bibtex
BibTex
titre
Parallel Molecular Dynamics Using OpenMP on a Shared Memory Machine
auteur
Raphael Couturier, Christophe Chipot
article
Computer Physics Communications, Elsevier, 2000, 124 (1), pp.49-59
Accès au bibtex
BibTex

1999

titre
Trois expérimentations parallèles différentes en simulation numérique
auteur
Raphaël Couturier
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 1999, 19 (5), pp.625-648
Accès au bibtex
BibTex
titre
Special Issue FMPPTA'98
auteur
Dominique Méry
article
World Scientific, 1999, Parallel Processing Letters
Accès au bibtex
BibTex
titre
Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems : Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems
auteur
Dominique Méry
article
A. Galloway & K. Taguchi. Integrated Formal Methods - IFM'99, 1999, York, UK, Springer Verlag, 20 p, 1999
Accès au bibtex
BibTex
titre
Edition Spéciale RenPar'10
auteur
Dominique Méry, Guy-René Perrin
article
Hermès, 1999, TSI
Accès au bibtex
BibTex
titre
Animating formal specifications : a telephone simulation case study
auteur
Jean-Paul Gibson, Dominique Méry, Yassine Mokhtari
article
13th European Simulation Multiconference - ESM'99, Jun 1999, Warsaw, Poland, II, pp.139--145, 1999
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00108114/file/99-R-161.pdf BibTex
titre
Validation of formal specifications
auteur
Dominique Méry, Yassine Mokhtari
article
AAAI'99, Fall Symposium, Nov 1999, none, 5 p, 1999
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00108115/file/99-R-280.pdf BibTex
titre
A compiler for parallel Unity programs using OpenMp
auteur
Raphaël Couturier, Bertrand Couturier, Dominique Méry
article
Parallel and Distributed Processing Techniques & Applications - PDPTA'99, Jul 1999, Las Vegas, USA, 21 p, 1999
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00098760/file/99-R-121.pdf BibTex
titre
Towards a formal engineering framework for process automation
auteur
Patrick Lamboley, Jean-François Pétin, Dominique Méry
article
Seventh IEEE International Conference on Emerging Technologies & Factory Automation - ETFA'99, 1999, Barcelona, Spain, IEEE, 8 p, 1999
Accès au bibtex
BibTex
titre
Specifying historical Consequence and Postponed Effect Properties in Real-Time Systems
auteur
Leila Jemni, Jacques Jaray, Ahmed Mahjoub
article
IASTED International Conference in Modelling, Identification & Control, 1999, Innsbruck, Austria, 4 p, 1999
Accès au bibtex
BibTex
titre
Integration Problems in Telephone Feature requirements
auteur
John Paul Gibson, Geoff Hamilton, Dominique Méry
article
K. Araki & A. Galloway & K. Taguchi. Workshop on Integrated Formal Methods - IFM'99, 1999, York, England, Springer Verlag, 19 p, 1999
Accès au bibtex
BibTex
titre
Abstract Animator for Temporal Specifications
auteur
Dominique Cansell, Dominique Méry
article
Françoise Bellegarde & Olga Kouchnarenko. Workshop on Modelling & Verification, 1999, Besançon, France, 1999
Accès au bibtex
BibTex
titre
Abstract animator for temporal specifications Application to TLA
auteur
Dominique Cansell, Dominique Méry
article
Agostino Cortesi and Gilberto Fil. International Symposium on Static Analysis - SAS'99, 1999, Venise, Italie, Springer Verlag, 1694, pp.284-299, 1999, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Formal modelling of services for getting a better understanding of the feature interaction problem - multi-view approach
auteur
Jean-Paul Gibson, Dominique Méry
article
D. Bjorner, M. Broy, A. Zamulin. Andrei Ershov Third International Conference, Perspectives of system Informatics - PSI'99, 1999, Novosibirsk, Russia, Springer-Verlag, 1755, pp.155-179, 1999, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Animating TLA Specifications
auteur
Yassine Mokhtari, Stephan Merz
article
H. Ganzinger, D. McAllester, A. Voronkov. International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, Springer, 1705, pp.92--110, 1999, Lecture Notes in Artificial Intelligence
Accès au bibtex
BibTex
titre
Lazy Caching in TLA
auteur
Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
article
Distributed Computing, Springer Verlag, 1999, 12 (2-3), pp.151-174
Accès au bibtex
BibTex

1998

titre
Spécification de services : une approche avec B
auteur
Bruno Mermet, Dominique Méry, Dmitri Samborski
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 1998, 17 (9), pp.1157-1180
Accès au bibtex
BibTex
titre
Process control engineering: contribution to a formal structuring framework with the B method
auteur
Jean-François Pétin, Gérard Morel, Dominique Méry, Patrick Lamboley
article
Didier Bert. The 2nd International B Conference, 1998, Montpellier, France. Springer Verlag, 1393, pp.198-209, 1998, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Service specifications to B, or not to B
auteur
Bruno Mermet, Dominique Méry
article
Second Workshop on Formal Methods in Software Practice, 1998, Clearwater Beach, Florida, USA, ACM, 8 p, 1998
Accès au bibtex
BibTex
titre
Formal engineering of the bitonic sort using pvs
auteur
Raphaël Couturier
article
Butterfield, Andrew and Flynn, Sharon. 2nd Irish Workshop in Formal Methods - IWFM'98, 1998, Cork, irlande, 16 p, 1998
Accès au bibtex
BibTex
titre
An experiment in parallelizing an application using formal methods
auteur
Raphaël Couturier, Dominique Méry
article
Hu, Alan and Vardi, Moshe. International Conference on Computer Aided Verification - CAV'98, 1998, Vancouver, Canada, 10 p, 1998, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Interprétation de spécifications temporelles à l'aide d'un outil de preuve
auteur
Dominique Cansell, Dominique Méry
article
AFADl'98, 1998, none, 13 p, 1998
Accès au bibtex
BibTex
titre
Parallelization of a Monte Carlo simulation of a spins system
auteur
Raphaël Couturier, Dominique Méry
article
Arabnia, Hamid R. Parallel and Distributed Processing Techniques and Applications - PDPTA'98, 1998, Las Vegas, USA, 5 p, 1998
Accès au bibtex
BibTex
titre
Anatomie d'une macro
auteur
Denis Roegel
article
Cahiers Gutenberg, Association GUTenberg, 1998, pp.19-27
Accès au bibtex
BibTex
titre
Teaching Formal Methods: Lessons to learn
auteur
Jean-Paul Gibson, Dominique Méry
article
Irish Workshop For Formal Methods 1998, 1998, Cork, Irlande, 16 p, 1998
Accès au bibtex
BibTex
titre
Always and Eventually in Object Requirements
auteur
Jean-Paul Gibson, Dominique Méry
article
Rigorous Object Oriented Methods, 1998, none, 20 p, 1998
Accès au bibtex
BibTex
titre
Third International Workshop on Formal Methods for Parallel Programming : Theory and Applications
auteur
Dominique Méry, Beverly Sanders
article
Springer Verlag, 100 p, 1998, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Formal engineering methods for modelling and verification of control systems
auteur
Dominique Méry, Jean-François Pétin
article
9th symposium on information control problems in manufacturing Advances in Industrial Engineering - INCOM'98, 1998, Nancy/France, ELSEVIER, 6 p, 1998, IFAC
Accès au bibtex
BibTex
titre
Fair Objects
auteur
Dominique Méry, Jean-Paul Gibson
article
Object Technology 98 (Colloquim on Object Technology System Re-engineering), 1998, none, 16 p, 1998
Accès au bibtex
BibTex
titre
RenPar'10
auteur
Guy-René Perrin, Dominique Méry
article
ULP, 264 p, 1998
Accès au bibtex
BibTex
titre
Parallélisation d'une simulation Monte Carlo d'un système de spins et preuve
auteur
Raphaël Couturier
article
Méry, Dominique and Perrin, Guy-René. Renpar'10, 1998, Strasbourg, France, 4 p, 1998
Accès au bibtex
BibTex
titre
The invoice system problem in TLA+
auteur
Yassine Mokhtari
article
International Workshop on Specification Techniques & Formal Methods, 1998, Nantes, France, 16 p, 1998
Accès au bibtex
BibTex
titre
An Object Oriented Requirements Capture and Analysis Environment
auteur
Jean-Paul Gibson
article
[Intern report] 98-R-010 || gibson98g, 1998, 33 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00098728/file/98-R-010.pdf BibTex
titre
POTS: An OO LOTOS Specification
auteur
Jean-Paul Gibson, Yassine Mokhtari
article
[Intern report] 98-R-013 || gibson98b, 1998, 27 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00098729/file/98-R-013.pdf BibTex