2024
- titre
- Leaf-First Zipper Semantics
- auteur
- Sergueï Lenglet, Alan Schmitt
- article
- 2024
- Accès au texte intégral et bibtex
-
- titre
- When are two Parametric Semi-linear Sets Equal?
- auteur
- Engel Lefaucheux
- article
- 2024
- Accès au texte intégral et bibtex
-
- titre
- Gröbner Bases for Boolean Function Minimization
- auteur
- Nicolas Faroß, Simon Schwarz
- article
- Proceedings of the 8th SC-Square Workshop, Jul 2024, Tromsø, Norway
- Accès au texte intégral et bibtex
-
- titre
- Destination-passing style programming: a Haskell implementation
- auteur
- Thomas Bagrel
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
2023
- titre
- From System Events to Software Operations for Refinement-based Modeling of Hybrid Systems *
- auteur
- Zheng Cheng, Dominique Méry
- article
- 2023
- Accès au texte intégral et bibtex
-
- titre
- Encoding TLA$^{+}$ Proof Obligations Safely for SMT
- auteur
- Rosalie Defourné
- article
- 9th International Conference on Rigorous State-Based Methods (ABZ 2023), May 2023, Nancy, France. pp.88-106, ⟨10.1007/978-3-031-33163-3_7⟩
- Accès au texte intégral et bibtex
-
- titre
- Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings
- auteur
- Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque
- article
- Lecture Notes in Computer Science, 14010, Springer Nature Switzerland, 2023, 978-3-031-33162-6. ⟨10.1007/978-3-031-33163-3⟩
- Accès au bibtex
-
- titre
- Extending PlusCal for Modeling Distributed Algorithms
- auteur
- Horatiu Cirstea, Stephan Merz
- article
- 18th International Conference on Integrated Formal Methods (iFM 2023), Nov 2023, Leiden, Netherlands. pp.321-340, ⟨10.1007/978-3-031-47705-8_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Extending a High-Performance Prover to Higher-Order Logic
- auteur
- Petar Vukmirović, Jasmin Blanchette, Stephan Schulz
- article
- TACAS 2023, 2023, Paris, France. pp.111-129, ⟨10.1007/978-3-031-30820-8_10⟩
- Accès au texte intégral et bibtex
-
- titre
- F3FLUID: A formal framework for developing safety‐critical interactive systems in FLUID
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Ismail Mendil, Dominique Méry, David Navarre, Philippe Palanque, Marc Pantel
- article
- Journal of Software: Evolution and Process, In press, ⟨10.1002/smr.2439⟩
- Accès au bibtex
-
- titre
- A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions
- auteur
- Zheng Cheng, Dominique Méry
- article
- 2023
- Accès au texte intégral et bibtex
-
- titre
- Mechanical certification of FOLID cyclic proofs
- auteur
- Sorin Stratulat
- article
- Annals of Mathematics and Artificial Intelligence, 2023, 95 (5), pp.651-673. ⟨10.1007/s10472-023-09832-7⟩
- Accès au texte intégral et bibtex
-
- titre
- SAP: A Secure Low-Latency Protocol for Mitigating High Computation Overhead in WI-FI Networks
- auteur
- Vineeta Jain, Ulf Wetzker, Vijay Laxmi, Manoj Singh Gaur, Mohamed Mosbah, Dominique Méry
- article
- IEEE Access, 2023, 11, pp.84620-84635. ⟨10.1109/ACCESS.2023.3302529⟩
- Accès au bibtex
-
- titre
- SCL(EQ): SCL for First-Order Logic with Equality
- auteur
- Hendrik Leidinger, Christoph Weidenbach
- article
- Journal of Automated Reasoning, 2023, 67 (3), pp.22. ⟨10.1007/s10817-023-09673-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Unifying Splitting
- auteur
- Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
- article
- Journal of Automated Reasoning, 2023, 67 (2), pp.16. ⟨10.1007/s10817-023-09660-8⟩
- Accès au texte intégral et bibtex
-
- titre
- Verified Given Clause Procedures
- auteur
- Jasmin Blanchette, Qi Qiu, Sophie Tourret
- article
- CADE-29, 2023, Rome, Italy. pp.61-77, ⟨10.1007/978-3-031-38499-8_4⟩
- Accès au texte intégral et bibtex
-
- titre
- Foreword. Special issue on CASC 2022
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- article
- 2023, pp.22. ⟨10.1007/s11786-023-00565-8⟩
- Accès au bibtex
-
- titre
- Encodages de la théorie des ensembles de TLA+ pour la preuve automatique
- auteur
- Antoine Defourné
- article
- Informatique [cs]. Université de Lorraine, 2023. Français. ⟨NNT : 2023LORR0263⟩
- Accès au texte intégral et bibtex
-
- titre
- SAT-Inspired Eliminations for Superposition
- auteur
- Petar Vukmirović, Jasmin Blanchette, Marijn J H Heule
- article
- ACM Transactions on Computational Logic, 2023, 24 (1), pp.1-25. ⟨10.1145/3565366⟩
- Accès au texte intégral et bibtex
-
- titre
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- auteur
- Martin Bromberger, Chaahat Jain, Christoph Weidenbach
- article
- Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Jul 2023, Rome (IT), Italy. pp.134 - 152, ⟨10.1007/978-3-031-38499-8_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
- auteur
- Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
- article
- CADE-29 - 29th International Conference on Automated Deduction (2023), Jul 2023, Rome, Italy. pp.542-559, ⟨10.1007/978-3-031-38499-8_31⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards an Automatic Proof of the Bakery Algorithm
- auteur
- Aman Goel, Stephan Merz, Karem A. Sakallah
- article
- Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2023., Jun 2023, Lisbon, Portugal. pp.21-28, ⟨10.1007/978-3-031-35355-0_2⟩
- Accès au texte intégral et bibtex
-
- titre
- Recurrence-Driven Summations in Automated Deduction
- auteur
- Visa Nummelin, Jasmin Blanchette, Sander Dahmen
- article
- FroCoS 2023, 2023, Prague, Czech Republic. pp.23-40, ⟨10.1007/978-3-031-43369-6_2⟩
- Accès au texte intégral et bibtex
-
- titre
- SCL(FOL) Revisited
- auteur
- Martin Bromberger, Simon Schwarz, Christoph Weidenbach
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
- titre
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- auteur
- Martin Bromberger, Chaahat Jain, Christoph Weidenbach
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
- titre
- Combining representation formalisms for reasoning upon mathematical knowledge
- auteur
- Mathieu D’aquin, Renata Bunoiu, Horatiu Cirstea, Michel Lenczner, Jean Lieber, Frédéric Zamkotsian
- article
- K-CAP '23: Knowledge Capture Conference 2023, Dec 2023, Pensacola FL USA, United States. pp.180-187, ⟨10.1145/3587259.3627549⟩
- Accès au texte intégral et bibtex
-
- titre
- Enumerative Level-2 Solution Counting for Quantified Boolean Formulas
- auteur
- Andreas Plank, Sibylle Möhle, Martina Seidl
- article
- 29th International Conference on Principles and Practice of Constraint Programming - CP 2023, Aug 2023, Toronto, Canada. ⟨10.4230/LIPIcs.CP.2023.49⟩
- Accès au texte intégral et bibtex
-
- titre
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
- titre
- Satisfiability Checking and Symbolic Computation 2023
- auteur
- Erika Ábrahám, Thomas Sturm
- article
- CEUR Workshop Proceedings, 3455, 2023
- Accès au bibtex
-
- titre
- Model Checking Linear Dynamical Systems under Floating-point Rounding
- auteur
- Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi
- article
- Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Apr 2023, Paris, France. pp.47-65, ⟨10.1007/978-3-031-30823-9_3⟩
- Accès au texte intégral et bibtex
-
- titre
- Universal First-Order Quantification over Automata
- auteur
- Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
- article
- EMU 2023 - 27th International Conference on Implementation and Application of Automata, Eastern Mediterranean University, Sep 2023, Famagusta, Cyprus. pp.91-102, ⟨10.1007/978-3-031-40247-0_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
- auteur
- Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack Mckeown
- article
- LPAR 2023 - 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Jun 2023, Manizales, Colombia. ⟨10.29007/1rhx⟩
- Accès au texte intégral et bibtex
-
- titre
- Formal domain-driven system development in Event-B: Application to interactive critical systems
- auteur
- Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Guillaume Dupont, Dominique Méry, Philippe Palanque
- article
- Journal of Systems Architecture, 2023, 135, pp.102798. ⟨10.1016/j.sysarc.2022.102798⟩
- Accès au bibtex
-
- titre
- Computer Algebra in Scientific Computing 2022
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- article
- Mathematics in Computer Science, 17 (3-4), 2023
- Accès au bibtex
-
- titre
- Exploring Partial Models with SCL
- auteur
- Martin Bromberger, Simon Schwarz, Christoph Weidenbach
- article
- Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Jun 2023, Manizales, Colombia. pp.48-22, ⟨10.29007/8BR1⟩
- Accès au texte intégral et bibtex
-
- titre
- SAT-Inspired Higher-Order Eliminations
- auteur
- Jasmin Blanchette, Petar Vukmirović
- article
- Logical Methods in Computer Science, 2023, 19 (2), ⟨10.48550/arXiv.2208.07775⟩
- Accès au texte intégral et bibtex
-
- titre
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- article
- Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Sep 2023, Prague (CZ), Czech Republic. pp.137 - 155, ⟨10.1007/978-3-031-43369-6_8⟩
- Accès au texte intégral et bibtex
-
- titre
- An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
- auteur
- Sibylle Möhle
- article
- Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Sep 2023, Prague, Czech Republic. pp.195 - 213, ⟨10.1007/978-3-031-43369-6_11⟩
- Accès au texte intégral et bibtex
-
- titre
- KBO Constraint Solving Revisited
- auteur
- Yasmine Briefs, Hendrik Leidinger, Christoph Weidenbach
- article
- Frontiers of Combining Systems - 14th International Symposium, Sep 2023, Prague (CZ), Czech Republic. pp.81 - 98, ⟨10.1007/978-3-031-43369-6_5⟩
- Accès au texte intégral et bibtex
-
- titre
- Closure Properties of General Grammars – Formally Verified
- auteur
- Martin Dvorak, Jasmin Blanchette
- article
- ITP 2023, 2023, Białystok, Poland. ⟨10.4230/LIPIcs.ITP.2023.15⟩
- Accès au texte intégral et bibtex
-
- titre
- Mechanical Mathematicians
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- article
- Communications of the ACM, 2023, 66 (4), pp.80-90. ⟨10.1145/3557998⟩
- Accès au texte intégral et bibtex
-
- titre
- Superposition for Higher-Order Logic
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović
- article
- Journal of Automated Reasoning, 2023, 67 (1), pp.10. ⟨10.1007/s10817-022-09649-9⟩
- Accès au texte intégral et bibtex
-
- titre
- Synchronization modulo P in dynamic networks
- auteur
- Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
- article
- Theoretical Computer Science, 2023, 942, pp.200-212. ⟨10.1016/J.TCS.2022.11.033⟩
- Accès au texte intégral et bibtex
-
- titre
- Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
- auteur
- Étienne André, Engel Lefaucheux, Didier Lime, Dylan Marinho, Jun Sun
- article
- Electronic Proceedings in Theoretical Computer Science, 2023, 392, pp.1 - 26. ⟨10.4204/eptcs.392.1⟩
- Accès au texte intégral et bibtex
-
2022
- titre
- Extending a brainiac prover to lambda-free higher-order logic
- auteur
- Petar Vukmirović, Jasmin Blanchette, Simon Cruanes, Stephan Schulz
- article
- International Journal on Software Tools for Technology Transfer, 2022, 24 (1), pp.67-87. ⟨10.1007/s10009-021-00639-7⟩
- Accès au texte intégral et bibtex
-
- titre
- Selected papers from the Rigorous State-Based Methods 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020
- auteur
- Dominique Méry, Alexander Raschke
- article
- Science of Computer Programming, 2022, 216, pp.102780. ⟨10.1016/j.scico.2022.102780⟩
- Accès au bibtex
-
- titre
- SCL(EQ): SCL for First-Order Logic with Equality
- auteur
- Hendrik Leidinger, Christoph Weidenbach
- article
- IJCAR, International Joint Conference in Automated Reasoning, Aug 2022, Haifa, Israel. pp.228-247, ⟨10.1007/978-3-031-10769-6_14⟩
- Accès au texte intégral et bibtex
-
- titre
- A Computational Approach to Complete Exact and Approximate Conservation Laws of Chemical Reaction Networks
- auteur
- Aurélien Desoeuvres, Alexandru Iosif, Christoph Lüders, Ovidiu Radulescu, Hamid Rahkooy, Matthias Seiß, Thomas Sturm
- article
- 2022
- Accès au bibtex
-
- titre
- Guaranteeing Timed Opacity using Parametric Timed Model Checking
- auteur
- Étienne André, Didier Lime, Dylan Marinho, Jun Sun
- article
- ACM Transactions on Software Engineering and Methodology, 2022, 31 (4), pp.1-36. ⟨10.1145/3502851⟩
- Accès au bibtex
-
- titre
- Empowering the Event-B Method Using External Theories
- auteur
- Yamine Aït-Ameur, Ismail Mendil, Guillaume Dupont, Dominique Méry, Marc Pantel, Peter Riviere, Neeraj Kumar Singh
- article
- Integrated Formal Methods, 13274, Springer International Publishing, pp.18-35, 2022, Lecture Notes in Computer Science, 978-3-031-07726-5. ⟨10.1007/978-3-031-07727-2_2⟩
- Accès au bibtex
-
- titre
- What’s decidable about linear loops?
- auteur
- Toghrul Karimov, Engel Lefaucheux, Joel Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell
- article
- 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022), Jan 2022, Philadelphia, United States. pp.1 - 25, ⟨10.1145/3498727⟩
- Accès au texte intégral et bibtex
-
- titre
- Making Higher-Order Superposition Work
- auteur
- Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
- article
- Journal of Automated Reasoning, 2022, 66 (4), pp.541-564. ⟨10.1007/s10817-021-09613-z⟩
- Accès au texte intégral et bibtex
-
- titre
- ODEbase: A Repository of ODE Systems for Systems Biology
- auteur
- Christoph Lüders, Thomas Sturm, Ovidiu Radulescu
- article
- Bioinformatics Advances, 2022, 2 (1), ⟨10.1093/bioadv/vbac027⟩
- Accès au bibtex
-
- titre
- Napier, John
- auteur
- Denis Roegel
- article
- Encyclopedia of Renaissance Philosophy, 2022, pp.2295-2297
- Accès au bibtex
-
- titre
- An Efficient State Space Construction for a Class of Timed Automata
- auteur
- Johan Arcile, Raymond Devillers, Hanna Klaudel
- article
- 43rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2022), Jun 2022, Bergen, Norway. pp.246--263, ⟨10.1007/978-3-662-68191-6_10⟩
- Accès au bibtex
-
- titre
- Non-Intrusive Annotation-Based Domain-Specific Analysis to Certify Event-B Models Behaviours
- auteur
- Ismail Mendil, Peter Riviere, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- article
- 29th Asia-Pacific Software Engineering Conference (APSEC 2022), Dec 2022, x, Japan. pp.129-138, ⟨10.1109/APSEC57359.2022.00025⟩
- Accès au texte intégral et bibtex
-
- titre
- Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
- auteur
- Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joel Ouaknine, David Purser, Markus A. Whiteland, James Worrell
- article
- 33rd International Conference on Concurrency Theory (CONCUR 2022), Sep 2022, Varsovie, Poland. ⟨10.4230/LIPIcs.CONCUR.2022.10⟩
- Accès au texte intégral et bibtex
-
- titre
- Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set
- auteur
- Julian d'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell
- article
- 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), Aug 2022, Vienna, Austria. pp.14, ⟨10.4230/LIPIcs⟩
- Accès au texte intégral et bibtex
-
- titre
- A Comprehensive Framework for Saturation Theorem Proving
- auteur
- Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
- article
- Journal of Automated Reasoning, 2022, 66 (4), pp.499-539. ⟨10.1007/s10817-022-09621-7⟩
- Accès au texte intégral et bibtex
-
- titre
- Certified Derivation of Small-Step From Big-Step Skeletal Semantics
- auteur
- Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille Noûs
- article
- PPDP 2022 - 24th International Symposium on Principles and Practice of Declarative Programming, Sep 2022, Tbilisi, Georgia. pp.1-48, ⟨10.1145/3551357.3551384⟩
- Accès au texte intégral et bibtex
-
- titre
- Connection-Minimal Abduction in EL via Translation to FOL
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- article
- Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Aug 2022, Haifa, Israel. pp.188-207, ⟨10.1007/978-3-031-10769-6_12⟩
- Accès au bibtex
-
- titre
- Analyse statique de transformations pour l'élimination de motifs
- auteur
- Pierre Lermusiaux
- article
- Langage de programmation [cs.PL]. Université de Lorraine, 2022. Français. ⟨NNT : 2022LORR0372⟩
- Accès au texte intégral et bibtex
-
- titre
- The boundedness and zero isolation problems for weighted automata over nonnegative rationals
- auteur
- Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, David Purser, Markus A Whiteland
- article
- LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. ⟨10.1145/3531130⟩
- Accès au texte intégral et bibtex
-
- titre
- A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column
- auteur
- Sophie Tourret, Christoph Weidenbach
- article
- Journal of Automated Reasoning, 2022, 66 (4), pp.575-584. ⟨10.1007/s10817-022-09617-3⟩
- Accès au bibtex
-
- titre
- Polite Combination of Algebraic Datatypes
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- article
- Journal of Automated Reasoning, 2022, 66 (3), pp.331-355. ⟨10.1007/s10817-022-09625-3⟩
- Accès au bibtex
-
- titre
- Non-Deterministic Abstract Machines
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt
- article
- CONCUR 2022 - 33rd International Conference on Concurrency Theory, Sep 2022, Varsovie, Poland. pp.1-24, ⟨10.4230/LIPIcs.CONCUR.2022.7⟩
- Accès au texte intégral et bibtex
-
- titre
- Offline and Online Monitoring of Scattered Uncertain Logs Using Uncertain Linear Dynamical Systems
- auteur
- Bineet Ghosh, Étienne André
- article
- 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Mohammad Mousavi and Anna Philippou, Jun 2022, Lucca, Italy. pp.67-87, ⟨10.1007/978-3-031-08679-3_5⟩
- Accès au bibtex
-
- titre
- Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract)
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- article
- 35th International Workshop on Description Logics (DL 2022), Aug 2022, Haifa, Israel
- Accès au texte intégral et bibtex
-
- titre
- Activity for learning computational thinking in plugged and unplugged mode
- auteur
- Margarida Romero, Thierry Viéville, Marie Duflot-Kremer
- article
- [Research Report] 006, UCA - INSPE Académie de Nice. 2022
- Accès au texte intégral et bibtex
-
- titre
- Stronger SMT Solvers for Proof Assistants : Proofs, Quantifier Simplification, Strategy Schedules
- auteur
- Hans-Jörg Schurr
- article
- Logic in Computer Science [cs.LO]. Université de Lorraine, 2022. English. ⟨NNT : 2022LORR0135⟩
- Accès au texte intégral et bibtex
-
- titre
- Semantic Relevance
- auteur
- Fajar Haifani, Christoph Weidenbach
- article
- IJCAR, International Joint Conference in Automated Reasoning, Aug 2022, Haifa, Israel. pp.208-227, ⟨10.1007/978-3-031-10769-6_13⟩
- Accès au texte intégral et bibtex
-
- titre
- Timed automata as a formalism for expressing security: A survey on theory and practice
- auteur
- Johan Arcile,, Étienne André
- article
- ACM Computing Surveys, 2022, ⟨10.1145/3534967⟩
- Accès au bibtex
-
- titre
- One-Clock Priced Timed Games with Arbitrary Weights
- auteur
- Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, Benjamin Monmege
- article
- Logical Methods in Computer Science, 2022, 18 (3), pp.51
- Accès au texte intégral et bibtex
-
- titre
- Zone Extrapolations in Parametric Timed Automata
- auteur
- Johan Arcile,, Étienne André
- article
- 14th NASA Formal Methods Symposium (NFM 2022), Klaus Havelund; Jyo Deshmukh; Ivan Perez, May 2022, Caltech, Pasadena, United States. pp.451-469, ⟨10.1007/978-3-031-06773-0_24⟩
- Accès au bibtex
-
- titre
- Experiments with Automated Reasoning in the Class
- auteur
- Isabela Drămnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
- article
- CICM 2022 - 15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi / Hybrid, Georgia. pp.287-304, ⟨10.1007/978-3-031-16681-5_20⟩
- Accès au texte intégral et bibtex
-
- titre
- Reachability and liveness in parametric timed automata
- auteur
- Étienne André, Didier Lime, Olivier Henri Roux
- article
- Logical Methods in Computer Science, 2022, 18 (1), ⟨10.46298/lmcs-18(1:31)2022⟩
- Accès au bibtex
-
- titre
- ARC: An Educational Project on Automated Reasoning in the Class
- auteur
- Isabela Drămnesc, Tudor Jebelean, Erika Ábrahám, Gábor Kusper, Sorin Stratulat
- article
- EdMedia + Innovate Learning 2022 - AACE Conferences, Jun 2022, New York, United States
- Accès au texte intégral et bibtex
-
- titre
- An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- article
- IJCAR 2022 - International Joint Conference in Automated Reasoning, Aug 2022, Haifa, Israel. pp.147-168, ⟨10.1007/978-3-031-10769-6_10⟩
- Accès au texte intégral et bibtex
-
- titre
- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
- auteur
- Igor Konnov, Markus Kuppe, Stephan Merz
- article
- Leveraging Applications of Formal Methods, Verification and Validation. 11th International Symposium, ISoLA 2022, 2022, Rhodes, Greece. pp.88-105, ⟨10.1007/978-3-031-19849-6_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Non-Deterministic Abstract Machines
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt
- article
- [Research Report] RR-9475, Inria. 2022, pp.1-33
- Accès au texte intégral et bibtex
-
- titre
- pylfit
- auteur
- Tony Ribeiro, Maxime Folschette, Morgan Magnin, Katsumi Inoue, Chiaki Sakama, Olivier Roux, Sophie Tourret, Madeleine Eyraud
- article
- 2022, ⟨swh:1:dir:253fc595a7b0695e8b58396de8a0dbecfcc2d4f8;origin=https://hal.archives-ouvertes.fr/hal-04435180;visit=swh:1:snp:32e97fa297205b15881d7e629637ebaf1167a1f7;anchor=swh:1:rel:bd05bc079cbaec08139ca176051e66b656cd64ee;path=/⟩
- Accès au texte intégral et bibtex
-
- titre
- Prophecy Made Simple
- auteur
- Leslie Lamport, Stephan Merz
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, 44 (2), pp.1-27. ⟨10.1145/3492545⟩
- Accès au texte intégral et bibtex
-
- titre
- Récurrence noethérienne pour le raisonnement de premier ordre
- auteur
- Sorin Stratulat
- article
- 1024 : Bulletin de la Société Informatique de France, 2022, 19, pp.157-169. ⟨10.48556/SIF.1024.19.157⟩
- Accès au texte intégral et bibtex
-
- titre
- Certified Abstract Machines for Skeletal Semantics
- auteur
- Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
- article
- CPP 2022 - 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.1-13, ⟨10.1145/3497775.3503676⟩
- Accès au texte intégral et bibtex
-
- titre
- Selected papers from The 13th International Symposium on Theoretical Aspects of Software Engineering 29 July – 1 August 2019, Guilin, China
- auteur
- Dominique Méry, Shengchao Qin
- article
- Science of Computer Programming, 2022, 218, pp.102804. ⟨10.1016/j.scico.2022.102804⟩
- Accès au bibtex
-
- titre
- Efficient Convex Zone Merging in Parametric Timed Automata
- auteur
- Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol
- article
- 20th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2022, Warsaw, Poland. pp.200-218, ⟨10.1007/978-3-031-15839-1_12⟩
- Accès au bibtex
-
- titre
- LibNDT: towards a formal library on spreadable properties over linked nested datatypes
- auteur
- Mathieu Montin, Amélie Ledein, Catherine Dubois
- article
- Ninth Workshop on Mathematically Structured Functional Programming (MSFP), Jeremy Gibbons; Max S. New, Apr 2022, Munich, Germany. pp.27-44, ⟨10.4204/eptcs.360.2⟩
- Accès au texte intégral et bibtex
-
- titre
- Briggs, Henry
- auteur
- Denis Roegel
- article
- Encyclopedia of Renaissance Philosophy, 2022, pp.496-497
- Accès au bibtex
-
- titre
- Seventeen Provers under the Hammer
- auteur
- Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, Makarius Wenzel
- article
- 13th International Conference on Interactive Theorem Proving - ITP 2022, Jul 2022, Tel Aviv, Israel. ⟨10.5281/zenodo.5940084⟩
- Accès au texte intégral et bibtex
-
- titre
- Foreword
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- article
- Mathematics in Computer Science, 2022, 16 (2-3), pp.16. ⟨10.1007/s11786-022-00533-8⟩
- Accès au bibtex
-
- titre
- F5: A REDUCE Package for Signature-based Gröbner Basis Computation
- auteur
- Alexander Demin, Hamid Rahkooy, Thomas Sturm
- article
- CASC 2022 - Computer Algebra in Scientific Computing, Aug 2022, Gezbe, Turkey
- Accès au texte intégral et bibtex
-
- titre
- Automated Reasoning in the Class
- auteur
- Isabela Drămnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
- article
- Computer-Algebra-Rundbrief, 2022, 71, pp.21-26
- Accès au texte intégral et bibtex
-
- titre
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- auteur
- Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish Murali, Christoph Weidenbach
- article
- Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Apr 2022, Munich (Germany), Germany. pp.480-501, ⟨10.1007/978-3-030-99524-9_27⟩
- Accès au bibtex
-
- titre
- The central role of data repositories and data models in Data Science and Advanced Analytics
- auteur
- Ladjel Bellatreche, Carlos Ordonez, Dominique Méry, Matteo Golfarelli, El Hassan Abdelwahed
- article
- Future Generation Computer Systems, 2022, 129, pp.13-17. ⟨10.1016/j.future.2021.11.027⟩
- Accès au bibtex
-
- titre
- strategFTO: Untimed control for timed opacity
- auteur
- Étienne André, Shapagat Bolat, Engel Lefaucheux, Dylan Marinho
- article
- 8th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022), Cyrille Artho; Peter Ölveczky, Dec 2022, Auckland, New Zealand. pp.27-33, ⟨10.1145/3563822.3568013⟩
- Accès au bibtex
-
- titre
- Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior
- auteur
- Étienne André, Masaki Waga, Natuski Urabe, Ichiro Hasuo
- article
- 14th NASA Formal Methods Symposium (NFM 2022), May 2022, Pasadena, United States. pp.470-488, ⟨10.1007/978-3-031-06773-0_25⟩
- Accès au bibtex
-
- titre
- Reduction of Chemical Reaction Networks with Approximate Conservation Laws
- auteur
- Aurélien Desoeuvres, Alexandru Iosif, Christoph Lüders, Ovidiu Radulescu, Hamid Rahkooy, Matthias Seiß, Thomas Sturm
- article
- 2022
- Accès au bibtex
-
- titre
- Deep Specification and Proof Preservation for the CoqTL Transformation Language
- auteur
- Zheng Cheng, Massimo Tisi
- article
- Software & Systems Modeling, 2022, ⟨10.1007/s10270-022-01004-1⟩
- Accès au texte intégral et bibtex
-
- titre
- Non-Intrusive Annotation-Based Domain-Specific Analysis to Certify Event-B Models Behaviours
- auteur
- Ismail Mendil, Peter Riviere, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- article
- 2022 29th Asia-Pacific Software Engineering Conference (APSEC), Dec 2022, Japan, Japan. pp.129-138, ⟨10.1109/APSEC57359.2022.00025⟩
- Accès au bibtex
-
2021
- titre
- Abduction inELvia Translation to FOL
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret
- article
- SOQE 2021 - 2nd Workshop on Second-Order Quantifier Elimination and Related Topics, Nov 2021, Hanoï (online), Vietnam. pp.46-58
- Accès au texte intégral et bibtex
-
- titre
- Robust optimal periodic control using guaranteed Euler's method
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- article
- ACC 2021 - American Control Conference, May 2021, New Orleans/Virtual, United States. pp.986-991, ⟨10.23919/ACC50511.2021.9482621⟩
- Accès au bibtex
-
- titre
- Superposition for Full Higher-order Logic
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.396-412, ⟨10.1007/978-3-030-79876-5_23⟩
- Accès au texte intégral et bibtex
-
- titre
- IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability
- auteur
- Étienne André
- article
- CAV 2021 - 33rd International Conference on Computer-Aided Verification, Rustan Leino and Alexandra Silva, Jul 2021, Los Angeles/Online, United States. pp.552-565, ⟨10.1007/978-3-030-81685-8_26⟩
- Accès au bibtex
-
- titre
- Contextual Dependency in State-based Modelling
- auteur
- Dominique Méry, Souad Kherroubi
- article
- Implicit and explicit semantics integration in proof based developments of discrete systems, Springer, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6_9⟩
- Accès au bibtex
-
- titre
- Formal Ontological Analysis for Medical Protocols
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry
- article
- Implicit and explicit semantics integration in proof based developments of discrete systems, Springer, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6_5⟩
- Accès au bibtex
-
- titre
- A reconstruction of Maurolico's tables of sines, tangents and secants (1558)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Regiomontanus's table of tangents (1490)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Peuerbach's table for his ``Quadratum geometricum'' (1516)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints
- auteur
- Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, David Lesens
- article
- Fundamenta Informaticae, 2021, 182 (1), pp.31-67. ⟨10.3233/FI-2021-2065⟩
- Accès au bibtex
-
- titre
- Superposition for Lambda-Free Higher-Order Logic
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
- article
- Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:1)2021⟩
- Accès au texte intégral et bibtex
-
- titre
- Superposition with First-class Booleans and Inprocessing Clausification
- auteur
- Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirović
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.378-395, ⟨10.1007/978-3-030-79876-5_22⟩
- Accès au bibtex
-
- titre
- Superposition with Lambdas
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- article
- Journal of Automated Reasoning, 2021, 65 (7), pp.893-940. ⟨10.1007/s10817-021-09595-y⟩
- Accès au texte intégral et bibtex
-
- titre
- Parametric Analyses of Attack-fault Trees
- auteur
- Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga
- article
- Fundamenta Informaticae, 2021, 182 (1), pp.69 - 94. ⟨10.3233/fi-2021-2066⟩
- Accès au texte intégral et bibtex
-
- titre
- A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations
- auteur
- Werner M Seiler, Matthias Seiss, Thomas Sturm
- article
- Mathematics in Computer Science, 2021, 15 (2), pp.333-352. ⟨10.1007/s11786-020-00485-x⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Reinhold's trigonometric tables (1554)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
- auteur
- Fajar Haifani, Sophie Tourret, Christoph Weidenbach
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.327-343, ⟨10.1007/978-3-030-79876-5_19⟩
- Accès au bibtex
-
- titre
- Improving Automation for Higher-Order Proof Steps
- auteur
- Antoine Defourné
- article
- FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.139-153, ⟨10.1007/978-3-030-86205-3_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Noetherian Induction for Computer-Assisted First-Order Reasoning
- auteur
- Sorin Stratulat
- article
- Symbolic Computation [cs.SC]. Université de Lorraine, 2021
- Accès au texte intégral et bibtex
-
- titre
- Static analysis of pattern-free properties
- auteur
- Horatiu Cirstea, Pierre Lermusiaux, Pierre-Etienne Moreau
- article
- PPDP 2021 - 23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallinn, Estonia. pp.1-13, ⟨10.1145/3479394.3479404⟩
- Accès au bibtex
-
- titre
- A Benchmarks Library for Extended Parametric Timed Automata
- auteur
- Étienne André, Dylan Marinho, Jaco van de Pol
- article
- TAP 2021 - 15th International Conference on Tests and Proofs, Jun 2021, Virtual, Norway. pp.39-50, ⟨10.1007/978-3-030-79379-1_3⟩
- Accès au bibtex
-
- titre
- Model-bounded monitoring of hybrid systems
- auteur
- Masaki Waga, Étienne André, Ichiro Hasuo
- article
- ICCPS 2021 - 12th ACM/IEEE International Conference on Cyber-Physical Systems, Martina Maggio; James Weimer, May 2021, Nashville, United States
- Accès au bibtex
-
- titre
- A reconstruction of Fine's table of sines (1530)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Lansberge's trigonometric tables (1591)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Fine's table of sines (1550)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA. 2021
- Accès au texte intégral et bibtex
-
- titre
- Foreword, with a Dedication to Andreas Weber
- auteur
- Matthew England, Wolfram Koepf, Timur Sadykov, Werner M Seiler, Thomas Sturm
- article
- Mathematics in Computer Science, 2021, 15 (2), pp.173 - 175. ⟨10.1007/s11786-020-00476-y⟩
- Accès au texte intégral et bibtex
-
- titre
- Parametric updates in parametric timed automata
- auteur
- Étienne André, Didier Lime, Mathias Ramparison
- article
- Logical Methods in Computer Science, 2021, 17 (2), pp.13:1-13:67. ⟨10.23638/LMCS-17(2:13)2021⟩
- Accès au bibtex
-
- titre
- French vital records data gathering and analysis through image processing and machine learning algorithms
- auteur
- Cyprien Plateau-Holleville, Enzo Bonnot, Franck Gechter, Laurent Heyberger
- article
- Journal of Data Mining and Digital Humanities, In press, 2021, ⟨10.46298/jdmdh.7327⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of the tables of Pitiscus' Thesaurus Mathematicus (1613)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A survey of the main fundamental European trigonometric tables printed in the 15th and 16th centuries
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of the tables of Rheticus' Canon doctrinæ triangulorum (1551)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Synchronization Modulo k in Dynamic Networks
- auteur
- Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
- article
- SSS 2021 - International Symposium on Stabilizing, Safety, and Security of Distributed Systems, Nov 2021, Virtual Event, France. pp.425-439, ⟨10.1007/978-3-030-91081-5_28⟩
- Accès au texte intégral et bibtex
-
- titre
- A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- auteur
- Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
- article
- FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.3-24, ⟨10.1007/978-3-030-86205-3_1⟩
- Accès au bibtex
-
- titre
- Automated Orchestration of Security Chains Driven by Process Learning
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- Communication Networks and Service Management in the Era of Artificial Intelligence and Machine Learning, Wiley, 2021, 978-1-119-67550-1. ⟨10.1002/9781119675525.ch12⟩
- Accès au bibtex
-
- titre
- Méthodes pour le raisonnement d'ordre supérieur dans SMT
- auteur
- Daniel El Ouraoui
- article
- Logique en informatique [cs.LO]. Université de Lorraine, 2021. Français. ⟨NNT : 2021LORR0023⟩
- Accès au texte intégral et bibtex
-
- titre
- E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning
- auteur
- Sorin Stratulat
- article
- SCSS 2021 - 9th International Symposium on Symbolic Computation in Software Science, Sep 2021, Linz, Austria. pp.129--135
- Accès au texte intégral et bibtex
-
- titre
- GdR Génie de la Programmation et du Logiciel, Défis 2030
- auteur
- Mireille Blay-Fornarino, Catherine Dubois, Pierre-Etienne Moreau
- article
- 2021
- Accès au texte intégral et bibtex
-
- titre
- An Approximation of Minimax Control using Random Sampling and Symbolic Computation
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- article
- IFAC-PapersOnLine, 2021, Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2021), 54 (5), pp.265-270. ⟨10.1016/j.ifacol.2021.08.509⟩
- Accès au bibtex
-
- titre
- Leveraging Event-B Theories for Handling Domain Knowledge in Design Models
- auteur
- Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- article
- 7th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2021), Nov 2021, Beijing, China. pp.40-58, ⟨10.1007/978-3-030-91265-9_3⟩
- Accès au texte intégral et bibtex
-
- titre
- Rigorous State-Based Methods-8th International Conference, ABZ 2021, Ulm, Germany, June 9–11, 2021, Proceedings
- auteur
- Alexander Raschke, Dominique Méry
- article
- ABZ 2021 - 8th International Conference on Rigorous State Based Methods, Jun 2021, Ulm, Germany. 12709, Springer International Publishing, 2021, Lecture Notes in Computer Science, 978-3-030-77543-8. ⟨10.1007/978-3-030-77543-8⟩
- Accès au bibtex
-
- titre
- MEMOCODE '21: Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design
- auteur
- Arunkumar S, Dominique Méry, Indranil Saha, Lijun Zhang
- article
- MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Nov 2021, Virtual, China. ACM, 2021, 978-1-4503-9127-6. ⟨10.1145/3487212⟩
- Accès au bibtex
-
- titre
- Computer Algebra in Scientific Computing 2019
- auteur
- Matthew England, Wolfram Koepf, Timur Sadykov, Werner Seiler, Thomas Sturm
- article
- Mathematics in Computer Science, 15 (2), 2021
- Accès au bibtex
-
- titre
- Towards Multi-layered Temporal Models: A Proposal to Integrate Instant Refinement in CCSL
- auteur
- Mathieu Montin, Marc Pantel
- article
- 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2021), Jun 2021, Valletta, Malta. pp.120-137, ⟨10.1007/978-3-030-78089-0_7⟩
- Accès au texte intégral et bibtex
-
- titre
- A Unifying Splitting Framework
- auteur
- Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.344-360, ⟨10.1007/978-3-030-79876-5_20⟩
- Accès au texte intégral et bibtex
-
- titre
- Alethe: Towards a Generic SMT Proof Format (extended abstract)
- auteur
- Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
- article
- PxTP 2021 - 7th Workshop on Proof eXchange for Theorem Proving, Sep 2021, Pittsburgh, PA / virtual, United States. pp.49-54, ⟨10.4204/EPTCS.336.6⟩
- Accès au texte intégral et bibtex
-
- titre
- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
- auteur
- Martin Bromberger, Alberto Fiori, Christoph Weidenbach
- article
- VMCAI 2021 - 22nd International Conference Verification, Model Checking, and Abstract Interpretation, Jan 2021, Copenhagen/virtuel, Denmark. pp.511-533, ⟨10.1007/978-3-030-67067-2_23⟩
- Accès au texte intégral et bibtex
-
- titre
- Parametric non-interference in timed automata
- auteur
- Étienne André, Aleksander Kryukov
- article
- ICECCS 2020 - 25th International Conference on Engineering of Complex Computer Systems, Yi Li and Alan Liew, Mar 2021, Singapore, Singapore
- Accès au bibtex
-
- titre
- Parametric Toricity of Steady State Varieties of Reaction Networks
- auteur
- Hamid Rahkooy, Thomas Sturm
- article
- CASC 2021 - Computer Algebra in Scientific Computing, Sep 2021, Sochi, Russia. pp.314-333, ⟨10.1007/978-3-030-85165-1_18⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Regiomontanus's great tables of sines (1541)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Computer Algebra in Scientific Computing 2020
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- article
- Mathematics in Computer Science, 15 (3), 2021
- Accès au bibtex
-
- titre
- SAT-Inspired Eliminations for Superposition
- auteur
- Petar Vukmirović, Jasmin Blanchette, Marijn J H Heule
- article
- FMCAD 2021 - 21st International Conference on Formal Methods in Computer-Aided Design, Oct 2021, New Haven, CT / virtual, United States. pp.231-240, ⟨10.5281/zenodo.4552499⟩
- Accès au texte intégral et bibtex
-
- titre
- Making Higher-Order Superposition Work
- auteur
- Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.415-432, ⟨10.1007/978-3-030-79876-5_24⟩
- Accès au texte intégral et bibtex
-
- titre
- A modular Isabelle framework for verifying saturation provers
- auteur
- Sophie Tourret, Jasmin Blanchette
- article
- CPP 2021 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2021, Virtual, Denmark. pp.224-237, ⟨10.1145/3437992.3439912⟩
- Accès au texte intégral et bibtex
-
- titre
- Politeness for the Theory of Algebraic Datatypes (Extended Abstract)
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- article
- IJCAI 2021 - International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers), Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
- Accès au bibtex
-
- titre
- Towards Leveraging Domain Knowledge in State-Based Formal Methods
- auteur
- Yamine Aït-Ameur, Régine Laleau, Dominique Méry, Neeraj Kumar Singh
- article
- Raschke, Alexander; Riccobene, Elvinia; Schewe, Klaus-Dieter. Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday, 12750, Springer, pp.1-13, 2021, Lecture Notes in Computer Science, 978-3-030-76020-5. ⟨10.1007/978-3-030-76020-5_1⟩
- Accès au bibtex
-
- titre
- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
- auteur
- Étienne André, Jaime Arias, Laure Petrucci, Jaco van De Pol
- article
- TACAS 2021 - 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote; Kim G. Larsen, Mar 2021, virtual, Luxembourg. pp.311-329, ⟨10.1007/978-3-030-72016-2_17⟩
- Accès au bibtex
-
- titre
- Efficiently and Effectively Recognizing Toricity of Steady State Varieties
- auteur
- Dima Grigoriev, Alexandru Iosif, Hamid Rahkooy, Thomas Sturm, Andreas Weber
- article
- Mathematics in Computer Science, 2021, 15 (2), pp.199 - 232. ⟨10.1007/s11786-020-00479-9⟩
- Accès au texte intégral et bibtex
-
- titre
- DUF : Dynamic Uncore Frequency scaling to reduce power consumption
- auteur
- Étienne André, Rémi Dulong, Amina Guermouche, François Trahay
- article
- Concurrency and Computation: Practice and Experience, 2021, 34 (3), pp.e6580
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Apian's table of sines (1533)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA. 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Rheticus's table of sines (1542)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Towards Dynamic Dependable Systems through Evidence-Based Continuous Certification
- auteur
- Rasha Faqeh, Christof Fetzer, Holger Herrmanns, Jörg Hoffmann, Michaela Klauck, Maximilian Koehl, Marcel Steinmetz, Christoph Weidenbach
- article
- ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2021, Rhodes, Greece
- Accès au texte intégral et bibtex
-
- titre
- On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Romain Geniet, Dominique Méry, Philippe Palanque
- article
- Interacting with Computers, 2021, ⟨10.1093/iwcomp/iwab016⟩
- Accès au bibtex
-
- titre
- Decidable $\exists$*$\forall$* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates
- auteur
- Marco Voigt
- article
- Journal of Automated Reasoning, 2021, 65 (3), pp.357-423. ⟨10.1007/s10817-020-09567-8⟩
- Accès au bibtex
-
- titre
- A Refinement Strategy for Hybrid System Design with Safety Constraints
- auteur
- Zheng Cheng, Dominique Méry
- article
- MEDI 2021 - 10th International Conference Model and Data Engineering, Jun 2021, Tallinn, Estonia. pp.3-17, ⟨10.1007/978-3-030-78428-7_1⟩
- Accès au bibtex
-
- titre
- Refinement-based Construction of Correct Distributed Algorithms
- auteur
- Dominique Méry
- article
- ICI2ST 2021 - 2nd International Conference on Information Systems and Software Technologies, Mar 2021, Quito / Virtual, Ecuador
- Accès au bibtex
-
- titre
- A reconstruction of Johannes Engel's table of sines in Regiomontanus's Tabulæ directionum profectionumque (1504)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA. 2021
- Accès au texte intégral et bibtex
-
- titre
- Special Issue
- auteur
- Matthew England, Wolfram Koepf, Timur M. Sadykov, Werner Seiler, Thomas Sturm
- article
- Aug 2019, Moscow, Russia. Mathematics in Computer Science, 2021
- Accès au bibtex
-
- titre
- Algorithmic Reduction of Biological Networks with Multiple Time Scales
- auteur
- Niclas Kruff, Christoph Lüders, Ovidiu Radulescu, Thomas Sturm, Sebastian Walcher
- article
- Mathematics in Computer Science, 2021, 15 (3), pp.499 - 534. ⟨10.1007/s11786-021-00515-2⟩
- Accès au texte intégral et bibtex
-
- titre
- Foreword, with a Dedication to Vladimir Gerdt
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- article
- Mathematics in Computer Science, 2021, 15 (3), pp.369 - 371. ⟨10.1007/s11786-021-00509-0⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Fincke's trigonometric tables (1583)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Viète's Canon Mathematicus (1579)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems
- auteur
- Hamid Rahkooy, Thomas Sturm
- article
- CASC 2021 - Computer Algebra in Scientific Computing, Sep 2021, Sochi, Russia. pp.334-352, ⟨10.1007/978-3-030-85165-1_19⟩
- Accès au texte intégral et bibtex
-
- titre
- Analysis of the Conradi-Kahle Algorithm for Detecting Binomiality on Biological Models
- auteur
- Alexandru Iosif, Hamid Rahkooy
- article
- 2021
- Accès au bibtex
-
- titre
- A reconstruction of the tables of Rheticus' Opus Palatinum (1596)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2021
- Accès au texte intégral et bibtex
-
- titre
- Quantifier Simplification by Unification in SMT
- auteur
- Pascal Fontaine, Hans-Jörg Schurr
- article
- FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.232-249, ⟨10.1007/978-3-030-86205-3_13⟩
- Accès au texte intégral et bibtex
-
- titre
- Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
- auteur
- Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
- article
- CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. ⟨10.1007/978-3-030-79876-5⟩
- Accès au texte intégral et bibtex
-
- titre
- Standard Conformance-by-Construction with Event-B
- auteur
- Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- article
- FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. pp.126-146, ⟨10.1007/978-3-030-85248-1_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems
- auteur
- Yamine Aït-Ameur, Shin Nakajima, Dominique Méry
- article
- Springer Singapore, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6⟩
- Accès au bibtex
-
2020
- titre
- Signature-Based Abduction for Expressive Description Logics
- auteur
- Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, Renate Schmidt
- article
- 17th International Conference on Principles of Knowledge Representation and Reasoning {KR-2020}, Sep 2020, Rhodes, France. pp.592-602, ⟨10.24963/kr.2020/59⟩
- Accès au bibtex
-
- titre
- Certifying a Rule-Based Model Transformation Engine for Proof Preservation
- auteur
- Zheng Cheng, Massimo Tisi, Joachim Hotonnier
- article
- ACM/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems, Oct 2020, Montreal, Canada. ⟨10.1145/3365438.3410949⟩
- Accès au texte intégral et bibtex
-
- titre
- PIAF : développer la Pensée Informatique et Algorithmique dans l'enseignement Fondamental
- auteur
- Gilbert Busana, Brigitte Denis, Marie Duflot-Kremer, Sarah Higuet, Lara Kataja, Yves Kreis, Christophe Laduron, Christian Meyers, Yannick Parmentier, Robert Reuter, Armin Weinberger
- article
- Didapro 8 – DidaSTIC – L'informatique, objets d’enseignements – enjeux épistémologiques, didactiques et de formation, Feb 2020, Lille, France
- Accès au texte intégral et bibtex
-
- titre
- SPIKE, an automatic theorem prover -- revisited
- auteur
- Sorin Stratulat
- article
- SYNASC2020 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2020, Timisoara, Romania. pp.93-96
- Accès au texte intégral et bibtex
-
- titre
- Cybersecurity risks and situation awareness: Audit committees' appraisal
- auteur
- Didier Fass, Stéphanie Thiéry
- article
- AHFE 2020 - Advances in Human Factors in Cybersecurity, Jul 2020, Virtual Conference, United States. pp.83-87, ⟨10.1007/978-3-030-52581-1_11⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of logarithms of the first 10000 primes (K4)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks
- auteur
- Hamid Rahkooy, Ovidiu Radulescu, Thomas Sturm
- article
- Computer Algebra in Scientific Computing: 22nd International Workshop - CASC 2020, pp.492-509, 2020, ⟨10.1007/978-3-030-60026-6_29⟩
- Accès au bibtex
-
- titre
- HOπ in Coq
- auteur
- Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
- article
- Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-020-09553-0⟩
- Accès au texte intégral et bibtex
-
- titre
- A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.7⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
- auteur
- Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
- article
- Journal of Automated Reasoning, 2020, 64 (7), pp.1169-1195. ⟨10.1007/s10817-020-09561-0⟩
- Accès au texte intégral et bibtex
-
- titre
- A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations
- auteur
- Werner M. Seiler, Matthias Seiss, Thomas Sturm
- article
- 2020
- Accès au bibtex
-
- titre
- A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks
- auteur
- Hamid Rahkooy, Cristian Vargas Montero
- article
- 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - SYNASC 2020, Sep 2020, Timisoara/Virtual, Romania
- Accès au bibtex
-
- titre
- A reconstruction of Edward Sang's table of mean anomalies, volume B (K47,1880)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A guide to Edward Sang's tables and to their reconstructions
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's canon of sines (K40/2,1877)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Politeness and Combination Methods for Theories with Bridging Functions
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- article
- Journal of Automated Reasoning, 2020, 64, pp.97-134. ⟨10.1007/s10817-019-09512-4⟩
- Accès au texte intégral et bibtex
-
- titre
- A Comprehensive Framework for Saturation Theorem Proving
- auteur
- Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
- article
- IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.316-334, ⟨10.1007/978-3-030-51074-9_18⟩
- Accès au texte intégral et bibtex
-
- titre
- Automated synthesis of local time requirement for service composition
- auteur
- Étienne André, Tian Huat Tan, Manman Chen, Shuang Liu, Jun Sun, Yang Liu, Jin Song Dong
- article
- Software and Systems Modeling, 2020, 19, pp.983-1013. ⟨10.1007/s10270-020-00787-5⟩
- Accès au bibtex
-
- titre
- Edward Sang’s computation of the logarithms of integers
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Edward Sang's steps for the construction of the logarithms of the primes (K1-K3)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of logarithms of the first myriad of integers (K5)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Symbolic computation and satisfiability checking (Editorial)
- auteur
- James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
- article
- Journal of Symbolic Computation, 2020, 100, pp.1-10. ⟨10.1016/j.jsc.2019.07.017⟩
- Accès au texte intégral et bibtex
-
- titre
- Lambert’s proof of the irrationality of Pi: Context and translation
- auteur
- Denis Roegel
- article
- [Research Report] LORIA. 2020
- Accès au texte intégral et bibtex
-
- titre
- Introduction to Edward Sang’s table of logarithms to 15 places
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- First-Order Tests for Toricity
- auteur
- Hamid Rahkooy, Thomas Sturm
- article
- 2020
- Accès au bibtex
-
- titre
- SCL with Theory Constraints
- auteur
- Martin Bromberger, Alberto Fiori, Christoph Weidenbach
- article
- 2020
- Accès au texte intégral et bibtex
-
- titre
- Statistical Model Checking of Distributed Programs within SimGrid
- auteur
- Marie Duflot, Yann Duplouy
- article
- SIMULTECH 2020 - 10th International Conference on Simulation and Modeling Methodologies, Technologies and Applications, Jul 2020, Lieusaint, France
- Accès au texte intégral et bibtex
-
- titre
- Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step
- auteur
- Guillaume Ambal, Alan Schmitt, Sergueï Lenglet
- article
- [Research Report] RR-9363, Inria Rennes - Bretagne Atlantique. 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's canon of sines (K40/1,1876)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Évaluation de la fiabilité des systèmes modélisés par arbres de défaillances grâce aux techniques de satisfiabilité
- auteur
- Margaux Duroeulx
- article
- Performance et fiabilité [cs.PF]. Université de Lorraine, 2020. Français. ⟨NNT : 2020LORR0026⟩
- Accès au texte intégral et bibtex
-
- titre
- Rigorous State-Based Methods - 7th International Conference, {ABZ} 2020, Ulm, Germany, May 27-29, 2020, Proceedings
- auteur
- Alexander Raschke, Dominique Méry, Frank Houdek
- article
- Alexander Raschke; Dominique Méry; Frank Houdek. ABZ 2020, May 2020, ULM, Germany. Lecture Notes in Computer Science (12071), Springer, 2020, Rigorous State-Based Methods - 7th International Conference, {ABZ} 2020, Ulm, Germany, May 27-29, 2020, Proceedings, 978-3-030-48076-9
- Accès au bibtex
-
- titre
- Special Issue : Symbolic Computation and Satisfiability Checking
- auteur
- James Harold Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
- article
- Journal of Symbolic Computation, 100, 2020
- Accès au bibtex
-
- titre
- Politeness for the Theory of Algebraic Datatypes
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- article
- 10th International Joint Conference on Automated Reasoning, IJCAR, Jul 2020, Paris, France. pp.238--255, ⟨10.1007/978-3-030-51074-9_14⟩
- Accès au bibtex
-
- titre
- Better Automation for TLA+ Proofs
- auteur
- Antoine Defourné
- article
- JFLA 2020 - 31emes Journées Francophones des Langages Applicatifs, Zaynah Dargaye; Yann Regis-Gianas, Jan 2020, Gruissan, France
- Accès au texte intégral et bibtex
-
- titre
- Generating Distributed Programs from Event-B Models
- auteur
- Horatiu Cirstea, Alexis Grall, Dominique Méry
- article
- International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
- Accès au bibtex
-
- titre
- A reconstruction of Edward Sang's table of mean anomalies, volume A (K46,1880)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's canon of sines (K41-K42,1881)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of logarithms of the second myriad of integers (K6)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding
- auteur
- Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
- article
- SMT 2020 - 18th International Workshop on Satisfiability Modulo Theories, Jul 2020, Online COVID-19, France
- Accès au texte intégral et bibtex
-
- titre
- Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method (verification challenge)
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- article
- ARCH20 - 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, Goran Frehse and Matthias Althoff, Jul 2020, Berlin, Germany. pp.197-184, ⟨10.29007/l3k2⟩
- Accès au bibtex
-
- titre
- A Mission Definition, Verification and Validation Architecture
- auteur
- Louis Viard, Laurent Ciarletta, Pierre-Etienne Moreau
- article
- Formal Methods. FM 2019 International Workshops, 12232, pp.281-287, 2020, 978-3-030-54993-0. ⟨10.1007/978-3-030-54994-7_20⟩
- Accès au bibtex
-
- titre
- A complete and terminating approach to linear integer solving
- auteur
- Martin Bromberger, Thomas Sturm, Christoph Weidenbach
- article
- Journal of Symbolic Computation, 2020, 100, pp.102-136. ⟨10.1016/j.jsc.2019.07.021⟩
- Accès au texte intégral et bibtex
-
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- auteur
- Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, Pascal Fontaine
- article
- Journal of Automated Reasoning, 2020, 64 (3), pp.485-510. ⟨10.1007/s10817-018-09502-y⟩
- Accès au texte intégral et bibtex
-
- titre
- Human Systems Design: Towards an Integrative Conceptual Framework
- auteur
- Didier Fass, J. M. Christian Bastien, Franck Gechter
- article
- AHFE 2020 Virtual Conference on Human Factors and Systems Interaction, Jul 2020, Florida, United States
- Accès au bibtex
-
- titre
- Language Preservation Problems in Parametric Timed Automata
- auteur
- Étienne André, Didier Lime, Nicolas Markey
- article
- Logical Methods in Computer Science, 2020, 16 (1), ⟨10.23638/LMCS-16⟩
- Accès au bibtex
-
- titre
- A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks
- auteur
- Hamid Rahkooy, Ovidiu Radulescu, Thomas Sturm
- article
- 2020
- Accès au bibtex
-
- titre
- Algorithmic Reduction of Biological Networks With Multiple Time Scales
- auteur
- Niclas Kruff, Christoph Lüders, Ovidiu Radulescu, Thomas Sturm, Sebastian Walcher
- article
- 2020
- Accès au bibtex
-
- titre
- Identifying the parametric occurrence of multiple steady states for some biological networks
- auteur
- Russell Bradford, James Harold Davenport, Matthew England, Hassan Errami, Vladimir Gerdt, Dima Grigoriev, Charles Hoyt, Marek Košta, Ovidiu Radulescu, Thomas Sturm, Andreas Weber
- article
- Journal of Symbolic Computation, 2020, 98, pp.84-119. ⟨10.1016/j.jsc.2019.07.008⟩
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of sines in degrees (K44,1879)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA. 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's auxiliary table for logarithms of almost unitary values (K39,1884)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Generating Distributed Programs from Event-B Models
- auteur
- Horatiu Cirstea, Alexis Grall, Dominique Méry
- article
- [Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36
- Accès au texte intégral et bibtex
-
- titre
- Logical reduction of metarules
- auteur
- Andrew Cropper, Sophie Tourret
- article
- Machine Learning, 2020, 109 (7), pp.1323 - 1369. ⟨10.1007/s10994-019-05834-x⟩
- Accès au texte intégral et bibtex
-
- titre
- On a Notion of Relevance
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- article
- Proceedings of the 33rd International Workshop on Description Logics (DL 2020), Sep 2020, Online, Greece
- Accès au texte intégral et bibtex
-
- titre
- PIAF: Developing Computational and Algorithmic Thinking in Fundamental Education
- auteur
- Yannick Parmentier, Robert Reuter, Sarah Higuet, Lara Kataja, Yves Kreis, Marie Duflot-Kremer, Christophe Laduron, Christian Meyers, Gilbert Busana, Armin Weinberger, Brigitte Denis
- article
- AACE 2020 - EdMedia + Innovate Learning, Jun 2020, Amsterdam / Virtual, Netherlands. pp.315-322
- Accès au texte intégral et bibtex
-
- titre
- Preface to the Special Issue on Automated Reasoning Systems
- auteur
- Armin Biere, Cesare Tinelli, Christoph Weidenbach
- article
- Journal of Automated Reasoning, 2020, 64 (3), pp.361-362. ⟨10.1007/s10817-019-09531-1⟩
- Accès au bibtex
-
- titre
- SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment
- auteur
- Andreas Teucke, Christoph Weidenbach
- article
- Journal of Automated Reasoning, 2020, 64 (3), pp.611-640. ⟨10.1007/s10817-020-09546-z⟩
- Accès au texte intégral et bibtex
-
- titre
- Edward Sang's computation of sines
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of logarithmic sines and tangents (K43,1888)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Edward Sang's table of circular segments (K45,1879)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2020
- Accès au texte intégral et bibtex
-
- titre
- Higher-order Automation in TLAPS
- auteur
- Antoine Defourné, Petar Vukmirovic
- article
- TLA+ Community Event 2020, Oct 2020, Virtual, France
- Accès au texte intégral et bibtex
-
- titre
- Pattern eliminating transformations
- auteur
- Horatiu Cirstea, Pierre Lermusiaux, Pierre-Etienne Moreau
- article
- LOPSTR 2020 - 30th International Symposium on Logic-Based Program Synthesis and Transformation, Sep 2020, Bologna, Italy
- Accès au texte intégral et bibtex
-
- titre
- First-Order Tests for Toricity
- auteur
- Hamid Rahkooy, Thomas Sturm
- article
- Computer Algebra in Scientific Computing: 22nd International Workshop - CASC 2020, 12291, pp.510-527, 2020, LNCS, ⟨10.1007/978-3-030-60026-6_30⟩
- Accès au bibtex
-
- titre
- A Refinement Strategy for Hybrid System Design with Safety Constraints
- auteur
- Zheng Cheng, Dominique Méry
- article
- [Research Report] Université de Lorraine; INRIA; CNRS. 2020
- Accès au texte intégral et bibtex
-
- titre
- Quand la technologie médicale mime les formes vivantes
- auteur
- Didier Fass
- article
- Georges Chapouthier; Marie-Christine Maurel. L'explosion des formes de vie : êtres vivants et morphologie, pp.195-215, 2020, 9781789480054
- Accès au bibtex
-
- titre
- Formalization of Logical Calculi in Isabelle/HOL
- auteur
- Mathias Fleury
- article
- Logic in Computer Science [cs.LO]. Universität des Saarlandes Saarbrücken, 2020. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- An Extension of PlusCal for Modeling Distributed Algorithms
- auteur
- Heba Alkayed, Horatiu Cirstea, Stephan Merz
- article
- TLA+ Community Event 2020, Oct 2020, Freiburg (online), Germany
- Accès au texte intégral et bibtex
-
- titre
- An Integrated Framework for the Formal Analysis of Critical Interactive Systems
- auteur
- Ismail Mendil, Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry, Philippe Palanque
- article
- The 27th Asia-Pacific Software Engineering Conference, Jun Sun, Dec 2020, Singapour, Singapore. pp.10
- Accès au bibtex
-
2019
- titre
- Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
- auteur
- Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
- article
- TACAS 2019 - International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17465-1_20⟩
- Accès au texte intégral et bibtex
-
- titre
- Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries
- auteur
- Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
- article
- CONCUR 2019 - 30th International Conference on Concurrency Theory, Aug 2019, Amsterdam, Netherlands. pp.1-16, ⟨10.4230/LIPIcs.CONCUR.2019.33⟩
- Accès au texte intégral et bibtex
-
- titre
- On the Expressivity and Applicability of Model Representation Formalisms
- auteur
- Andreas Teucke, Marco Voigt, Christoph Weidenbach
- article
- FroCoS 2019 - 12th International Symposium on Frontiers of Combining Systems, 2019, London, United Kingdom. pp.22-39, ⟨10.1007/978-3-030-29007-8_2⟩
- Accès au texte intégral et bibtex
-
- titre
- Decision Procedures for Linear Arithmetic
- auteur
- Martin Bromberger
- article
- Logic in Computer Science [cs.LO]. Saarland University, 2019. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- SCL: Clause Learning from Simple Models
- auteur
- Alberto Fiori, Christoph Weidenbach
- article
- 27th International Conference on Automated Deduction, 2019, Natal, Brazil. pp.233-249, ⟨10.1007/978-3-030-29436-6_14⟩
- Accès au texte intégral et bibtex
-
- titre
- Efficiently and Effectively Recognizing Toricity of Steady State Varieties
- auteur
- Dima Grigoriev, Alexandru Iosif, Hamid Rahkooy, Thomas Sturm, Andreas Weber
- article
- 2019
- Accès au bibtex
-
- titre
- Le jeu du robot : analyse d’une activité d’informatique débranchée sous la perspective de la cognition incarnée.
- auteur
- Margarida Romero, Marie Duflot, Thierry Viéville
- article
- Review of science, mathematics and ICT education, 2019, 13 (1), ⟨10.26220/rev.3089⟩
- Accès au texte intégral et bibtex
-
- titre
- Proving Soundness of Extensional Normal-Form Bisimilarities
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- Logical Methods in Computer Science, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩
- Accès au bibtex
-
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- Electronic Communications of the EASST, 2019, 076, ⟨10.14279/tuj.eceasst.76.1075.1042⟩
- Accès au texte intégral et bibtex
-
- titre
- The Challenge of Unifying Semantic and Syntactic Inference Restrictions
- auteur
- Christoph Weidenbach
- article
- 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), 2019, Natal, Brazil
- Accès au texte intégral et bibtex
-
- titre
- Formal specification and verification
- auteur
- Stephan Merz
- article
- Dahlia Malkhi. Concurrency: the Works of Leslie Lamport, 29, Association for Computing Machinery, pp.103-129, 2019, ACM Books, ⟨10.1145/3335772.3335780⟩
- Accès au texte intégral et bibtex
-
- titre
- Ergonomie théorique de l’humain-machine : quels fondements épistémologiques pour une conception sûre ?
- auteur
- Rémi Nazin
- article
- Interface homme-machine [cs.HC]. Université de Lorraine, 2019. Français. ⟨NNT : 2019LORR0012⟩
- Accès au texte intégral et bibtex
-
- titre
- Selected Extended Papers of ITP 2016: Preface
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- article
- Journal of Automated Reasoning, 2019, 62 (2), pp.169-170. ⟨10.1007/s10817-018-9470-8⟩
- Accès au texte intégral et bibtex
-
- titre
- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
- auteur
- Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz
- article
- TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. pp.192-210
- Accès au texte intégral et bibtex
-
- titre
- Monitor-Centric Mission Definition with Sophrosyne
- auteur
- Louis Viard, Laurent Ciarletta, Pierre-Etienne Moreau
- article
- ICUAS -2019 International Conference on Unmanned Aircraft Systems, Jun 2019, Atlanta, United States
- Accès au bibtex
-
- titre
- Extending SMT Solvers to Higher-Order Logic
- auteur
- Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark Barrett
- article
- CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.35-54, ⟨10.1007/978-3-030-29436-6_3⟩
- Accès au texte intégral et bibtex
-
- titre
- Bisimulations for Delimited-Control Operators
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- Logical Methods in Computer Science, 2019, 15 (2), pp.18:1-18:57. ⟨10.23638/LMCS-15(2:18)2019⟩
- Accès au bibtex
-
- titre
- Human factors: the real issues of autonomous vehicles?
- auteur
- Franck Gechter, Pierre Romet, Didier Fass
- article
- AutomotiveUI 2019 USER INTERFACES, ACM SIGCHI, Sep 2019, UTRECHT, Netherlands
- Accès au texte intégral et bibtex
-
- titre
- Machine Learning for Instance Selection in SMT Solving
- auteur
- Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine, Cezary Kaliszyk
- article
- AITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
- Accès au texte intégral et bibtex
-
- titre
- Reconstructing veriT Proofs in Isabelle/HOL
- auteur
- Mathias Fleury, Hans-Jörg Schurr
- article
- PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving, Aug 2019, Natal, Brazil. pp.36-50, ⟨10.4204/EPTCS.301.6⟩
- Accès au texte intégral et bibtex
-
- titre
- Superposition with Lambdas
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- article
- CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.55-73, ⟨10.1007/978-3-030-29436-6_4⟩
- Accès au texte intégral et bibtex
-
- titre
- SLD-Resolution Reduction of Second-Order Horn Fragments
- auteur
- Sophie Tourret, Andrew Cropper
- article
- JELIA 2019 - European Conference on Logics in Artificial Intelligence, May 2019, Rende, Italy. pp.259-276, ⟨10.1007/978-3-030-19570-0_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
- auteur
- Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
- article
- 2019
- Accès au texte intégral et bibtex
-
- titre
- Verification by Construction of Distributed Algorithms
- auteur
- Dominique Méry
- article
- Theoretical Aspects of Computing - {ICTAC} 2019 - 16th International Colloquium, Oct 2019, Mammamet, Tunisia. pp.22-38, ⟨10.1007/978-3-030-32505-3_2⟩
- Accès au bibtex
-
- titre
- Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
- auteur
- Marco Voigt
- article
- Logic in Computer Science [cs.LO]. Universität des Saarlandes, 2019. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Orchestration et vérification de fonctions de sécurité pour des environnements intelligents
- auteur
- Nicolas Schnepf
- article
- Réseaux et télécommunications [cs.NI]. Université de Lorraine, 2019. Français. ⟨NNT : 2019LORR0088⟩
- Accès au texte intégral et bibtex
-
- titre
- Pattern eliminating transformations
- auteur
- Pierre Lermusiaux, Horatiu Cirstea, Pierre-Etienne Moreau
- article
- CIEL 2019 - 8ème Conférence en IngénieriE du Logiciel, Jun 2019, Toulouse, France
- Accès au texte intégral et bibtex
-
- titre
- Automated Deduction – CADE-27
- auteur
- Pascal Fontaine
- article
- Pascal Fontaine. CADE 27 - 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. 11716, Springer, 2019, Lecture Notes in Artificial Intelligence
- Accès au bibtex
-
- 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, 2019, 90, pp.3-41. ⟨10.1016/j.jsc.2018.04.002⟩
- Accès au texte intégral et bibtex
-
- titre
- A Verified Prover Based on Ordered Resolution
- auteur
- Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
- article
- CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. ⟨10.1145/3293880.3294100⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
- auteur
- Jasmin Christian Blanchette
- article
- CPP 2019 - The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. ⟨10.1145/3293880.3294087⟩
- Accès au texte intégral et bibtex
-
- titre
- Diacritical Companions
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- MFPS 2019-Mathematical Foundations of Programming Semantics XXXV, Jun 2019, London, United Kingdom. ⟨10.1016/j.entcs.2019.09.003⟩
- Accès au texte intégral et bibtex
-
- titre
- Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry, David Navarre, Philippe Palanque, Marc Pantel
- article
- 7th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2019), Nov 2019, Shenzhen, China. pp.21-39, ⟨10.1007/978-3-030-46902-3_2⟩
- Accès au texte intégral et bibtex
-
- titre
- Automated Factorization of Security Chains in Software-Defined Networks
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- IFIP/IEEE IM 2019 - IFIP/IEEE International Symposium on Integrated Network Management, Apr 2019, Washington, United States
- Accès au texte intégral et bibtex
-
- titre
- Generic Encodings of Constructor Rewriting Systems
- auteur
- Horatiu Cirstea, Pierre-Etienne Moreau
- article
- PPDP '19: Principles and Practice of Programming Languages 2019, Oct 2019, Porto, Portugal. pp.19, ⟨10.1145/3354166.3354173⟩
- Accès au texte intégral et bibtex
-
- titre
- Integrating satisfiability solving in the assessment of system reliability modeled by dynamic fault trees
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- article
- 29th European Safety and Reliability Conference, ESREL 2019, Sep 2019, Hannover, Germany. ⟨10.3850/981-973-0000-00-0⟩
- Accès au texte intégral et bibtex
-
- titre
- SPASS-SATT: A CDCL(LA) Solver
- auteur
- Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
- article
- CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.111-122, ⟨10.1007/978-3-030-29436-6_7⟩
- Accès au texte intégral et bibtex
-
- titre
- Better SMT Proofs for Easier Reconstruction
- auteur
- Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, Hans-Jörg Schurr
- article
- AITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
- Accès au texte intégral et bibtex
-
- titre
- Bindings as Bounded Natural Functors
- auteur
- Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
- article
- Proceedings of the ACM on Programming Languages, 2019, 3 (POPL), pp.1-34. ⟨10.1145/3290335⟩
- Accès au texte intégral et bibtex
-
- titre
- Theory Combination: Beyond Equality Sharing
- auteur
- Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
- article
- Carsten Lutz; Uli Sattler; Cesare Tinelli; Anni-Yasmin Turhan; Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.57-89, 2019, Theoretical Computer Science and General Issues, 978-3-030-22101-0
- Accès au texte intégral et bibtex
-
- titre
- A Tool Suite for the Automated Synthesis of Security Function Chains
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- IFIP/IEEE IM 2019 - IFIP/IEEE International Symposium on Integrated Network Management, Apr 2019, Washington, United States
- Accès au texte intégral et bibtex
-
- titre
- Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry
- article
- ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
- Accès au texte intégral et bibtex
-
- titre
- TLA+ Model Checking Made Symbolic
- auteur
- Igor Konnov, Jure Kukovec, Thanh-Hai Tran
- article
- Proceedings of the ACM on Programming Languages, 2019, 3 (OOPSLA), pp.123:1--123:30. ⟨10.1145/3360549⟩
- Accès au texte intégral et bibtex
-
- titre
- 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE)
- auteur
- Dominique Méry, Shengchao Qin
- article
- Dominique Méry and Shengchao Qin. Theoretical Aspects of Software Engineering (TASE), Guillin, China. IEEE, 2019, 978-1-7281-3342-3
- Accès au bibtex
-
- titre
- Handbook of Model Checking by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds), published by Springer International Publishing AG, Cham, Switzerland, 2018.
- auteur
- Igor Konnov
- article
- Formal Aspects of Computing, 2019, pp.455-456. ⟨10.1007/s00165-019-00486-z⟩
- Accès au texte intégral et bibtex
-
- titre
- A Complete Normal-Form Bisimilarity for State
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- [Research Report] RR-9251, Inria Nancy - Grand Est. 2019
- Accès au texte intégral et bibtex
-
- titre
- A Complete Normal-Form Bisimilarity for State
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- FoSSaCS, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17127-8_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Hierarchic Superposition Revisited
- auteur
- Peter Baumgartner, Uwe Waldmann
- article
- Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni-Yasmin Turhan and Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.15-56, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-22102-7_2⟩
- Accès au texte intégral et bibtex
-
- titre
- PIAF : développer la Pensée Informatique et Algorithmique dans l'enseignement Fondamental
- auteur
- Gilbert Busana, Brigitte Denis, Marie Duflot-Kremer, Sarah Higuet, Lara Kataja, Yves Kreis, Christophe Laduron, Christian Meyers, Yannick Parmentier, Robert Reuter, Armin Weinberger
- article
- 2019
- Accès au texte intégral et bibtex
-
- titre
- A Formal Proof of the Expressiveness of Deep Learning
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Dietrich Klakow
- article
- Journal of Automated Reasoning, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
- Accès au texte intégral et bibtex
-
2018
- titre
- Extracting Symbolic Transitions from $TLA+$ Specifications
- auteur
- Jure Kukovec, Thanh-Hai Tran, Igor Konnov
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018, Jun 2018, Southampton, United Kingdom. pp.89-104, ⟨10.1007/978-3-319-91271-4_7⟩
- Accès au texte intégral et bibtex
-
- 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, ⟨10.1145/3167083⟩
- Accès au texte intégral et 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. pp.20
- Accès au texte intégral et bibtex
-
- titre
- Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary
- auteur
- Igor Konnov, Stephan Merz
- article
- BCRB 2018 - DSN Workshop on Byzantine Consensus and Resilient Blockchains, Jun 2018, Luxembourg, Luxembourg
- Accès au texte intégral et bibtex
-
- titre
- Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B
- auteur
- Souad Kherroubi
- article
- Théorie et langage formel [cs.FL]. Université de Lorraine, 2018. Français. ⟨NNT : 2018LORR0230⟩
- Accès au texte intégral et bibtex
-
- titre
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- auteur
- Marion Guthmuller, Gabriel Corona, Martin Quinson
- article
- Journal of Logical and Algebraic Methods in Programming, 2018, 96, pp.1 - 11. ⟨10.1016/j.jlamp.2017.12.004⟩
- Accès au texte intégral et 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, Belgique
- Accès au texte intégral et bibtex
-
- titre
- Encoding TLA+ into unsorted and many-sorted first-order logic
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- Science of Computer Programming, 2018, 158, pp.3-20. ⟨10.1016/j.scico.2017.09.004⟩
- Accès au texte intégral et bibtex
-
- titre
- Synaptic: A formal checker for SDN-based security policies
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- NOMS 2018 - IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, Taiwan. ⟨10.1109/NOMS.2018.8406122⟩
- Accès au texte intégral et bibtex
-
- titre
- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
- auteur
- Martin Bromberger
- article
- IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.329-345
- Accès au texte intégral et bibtex
-
- titre
- Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)
- auteur
- Régine Laleau, Dominique Méry, Shin Nakajima, Elena Troubitsyna
- article
- Electronic Proceedings in Theoretical Computer Science, 271, 2018, ⟨10.4204/EPTCS.271⟩
- Accès au bibtex
-
- titre
- Modelling by Patterns for Correct-by-Construction Process.
- auteur
- Dominique Méry
- article
- ISOLA 2018 - 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Nov 2018, Limassol, Cyprus. pp.399-423
- Accès au bibtex
-
- titre
- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
- auteur
- Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
- article
- IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
- auteur
- Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To, Xuan Tung Vu
- article
- SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- ByMC: Byzantine Model Checker
- auteur
- Igor Konnov, Josef Widder
- article
- ISoLA 2018 - 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2018, Limassol, Cyprus. pp.327-342, ⟨10.1007/978-3-030-03424-5_22⟩
- Accès au texte intégral et 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. pp.238 - 253, ⟨10.1007/978-3-319-99639-4_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- AVOCS 2018 - 18th International Workshop on Automated Verification of Critical Systems, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Superposition for Lambda-Free Higher-Order Logic
- auteur
- Alexander Bentkamp, Simon Cruanes, Jasmin Christian Blanchette, Uwe Waldmann
- article
- IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery
- article
- 2018
- Accès au texte intégral et bibtex
-
- titre
- Formal Ontology Driven Model Refactoring
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Mery
- article
- 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), Dec 2018, Melbourne, Australia. pp.136-145, ⟨10.1109/ICECCS2018.2018.00022⟩
- Accès au texte intégral et bibtex
-
- titre
- BmcMT: Bounded Model Checking of TLA + Specifications with SMT
- auteur
- Igor Konnov, Jure Kukovec, Thanh Hai Tran
- article
- TLA+ Community Meeting 2018, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et 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
-
- titre
- Higher-Order SMT Solving (Work in Progress)
- auteur
- Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, Cesare Tinelli
- article
- SMT 2018 - 16th International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Revisiting Enumerative Instantiation
- auteur
- Andrew J Reynolds, Haniel Barbosa, Pascal Fontaine
- article
- [Research Report] University of Iowa; Inria. 2018
- Accès au texte intégral et 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. pp.39--53
- Accès au texte intégral et bibtex
-
- titre
- Vers un principe de conception sûre des systèmes cyber-économiques
- auteur
- Stéphanie Thiéry, Didier Fass
- article
- Journée du droit pénal économique, ILCE - Institut de lutte contre la criminalité économique HEG-ARC, Université de Fribourg, Expert Suisse, Jun 2018, Neuchâtel, Suisse
- Accès au texte intégral et bibtex
-
- titre
- Satisfiability Modulo Theories: state-of-the-art, contributions, project
- auteur
- Pascal Fontaine
- article
- Logic in Computer Science [cs.LO]. Université de lorraine, 2018
- Accès au texte intégral et bibtex
-
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
- article
- Journal of Automated Reasoning, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩
- Accès au texte intégral et bibtex
-
- titre
- Virtual environment design as automated "physiological" counter-measures in extreme environment: from intensive care to human space flight.
- auteur
- Didier Fass, Bruno Levy, Pierre Perez, Dominique Méry
- article
- AHFE 2018 - Human Factors and Simulation, Jul 2018, Orlando, United States
- Accès au texte intégral et bibtex
-
- titre
- Superposition with Datatypes and Codatatypes
- auteur
- Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
- article
- IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Why co-adaptation is mandatory in extreme environment human-system integration and co-evolution modelling?
- auteur
- Franck Gechter, Didier Fass
- article
- AHFE 2018 - Human Factors and Simulation, Jul 2018, Orlando, United States
- Accès au texte intégral et bibtex
-
- titre
- Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)
- auteur
- Régine Laleau, Dominique Méry, Shin Nakajima, Elena Troubitsyna
- article
- IMPEX/FM&MDD 2017, Xi'an, China, Electronic Proceedings in Theoretical Computer Science, EPTCS 271, arXiv, 2018, ⟨10.48550/arXiv.1805.04636⟩
- Accès au bibtex
-
- titre
- Thirty Years of Virtual Substitution
- auteur
- Thomas Sturm
- article
- ISSAC 2018 - 43rd International Symposium on Symbolic and Algebraic Computation, Jul 2018, New York, United States. ⟨10.1145/3208976.3209030⟩
- Accès au texte intégral et bibtex
-
- titre
- Model and Data Engineering. 8th International Conference, MEDI 2018, Proceedings
- auteur
- El Hassan Abdelwahed, Ladjel Bellatreche, Matteo Golfarelli, Dominique Méry, Carlos Ordonez
- article
- Springer, 2018, Lecture Notes in Computer Science, 978-3-030-00855-0. ⟨10.1007/978-3-030-00856-7⟩
- Accès au bibtex
-
- titre
- SMT Solving Modulo Tableau and Rewriting Theories
- auteur
- Guillaume Bury, Simon Cruanes, David Delahaye
- article
- SMT 2018 - 16th International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- An Automation-Friendly Set Theory for the B Method
- auteur
- Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
- article
- ABZ 2018 - 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Jun 2018, Southampton, United Kingdom. pp.409-414, ⟨10.1007/978-3-319-91271-4_32⟩
- Accès au texte intégral et bibtex
-
- titre
- The SYMBIONT Project: Symbolic Methods for Biological Networks
- auteur
- François Boulier, Francois Fages, Ovidiu Radulescu, Satya Swarup Samal, Andreas Schuppert, Werner Seiler, Thomas Sturm, Sebastian Walcher, Andreas Weber
- article
- ISSAC 2018, Jul 2018, New York City, NY, United States
- Accès au bibtex
-
- titre
- The SYMBIONT Project: Symbolic Methods for Biological Networks
- auteur
- François Boulier, François Fages, Ovidiu Radulescu, Satya S Samal, Andreas Schuppert, Werner M. Seiler, Thomas Sturm, Sebastian Walcher, Andreas Weber
- article
- 2018
- Accès au texte intégral et bibtex
-
- titre
- A verified SAT solver with watched literals using imperative HOL
- auteur
- Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
- article
- CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ⟨10.1145/3167080⟩
- Accès au texte intégral et bibtex
-
- titre
- Derivation Reduction of Metarules in Meta-interpretive Learning
- auteur
- Andrew Cropper, Sophie Tourret
- article
- Inductive Logic Programming, Sep 2018, Ferrara, Italy. pp.1-21, ⟨10.1007/978-3-319-99960-9_1⟩
- Accès au texte intégral et bibtex
-
- titre
- New Trends in Model and Data Engineering
- auteur
- El Hassan Abdelwahed, Ladjel Bellatreche, Djamal Benslimane, Matteo Golfarelli, Stéphane Jean, Dominique Méry, Kazumi Nakamatsu, Carlos Ordonez
- article
- MEDI 2018 - International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Oct 2018, Marrakesh, Morocco. Communications in Computer and Information Science, Communications in Computer and Information Science (929), 2018, 978-3-030-02851-0. ⟨10.1007/978-3-030-02852-7⟩
- Accès au 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 - IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, Taiwan. ⟨10.1109/NOMS.2018.8406153⟩
- Accès au texte intégral et bibtex
-
- titre
- A Machine-Checked Correctness Proof for Pastry
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- article
- Science of Computer Programming, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩
- Accès au texte intégral et bibtex
-
- titre
- On the importance of explicit domain modelling in refinement-based modelling design: experiments with Event-B
- auteur
- Yamine Aït-Ameur, Idir Ait-Sadoune, Pierre Castéran, John Paul Gibson, Kahina Hacid, Souad Kherroubi, Dominique Méry, Linda Mohand Oussaid, Neeraj Kumar Singh, Laurent Voisin
- article
- 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2018), Jun 2018, Southampton, United Kingdom. pp.425--430, ⟨10.1007/978-3-319-91271-4_35⟩
- Accès au texte intégral et bibtex
-
2017
- titre
- Before Torchi and Schwilgué, there was White
- auteur
- Denis Roegel
- article
- ComputingEdge, 2017, May, pp.42-43
- Accès au bibtex
-
- titre
- A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
- auteur
- Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
- article
- CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.432-453, ⟨10.1007/978-3-319-63046-5_27⟩
- Accès au texte intégral et bibtex
-
- titre
- NP-completeness of small conflict set generation for congruence closure
- auteur
- Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
- article
- Formal Methods in System Design, 2017, 51 (3), pp.533 - 544. ⟨10.1007/s10703-017-0283-x⟩
- Accès au texte intégral et 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. pp.137--152, ⟨10.1007/978-3-319-66854-3_11⟩
- Accès au 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
-
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- auteur
- Haniel Barbosa, Jasmin Christian 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
-
- 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
-
- 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
-
- titre
- A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
- auteur
- Thomas Sturm
- article
- Mathematics in Computer Science, 2017, 11 (3-4), pp.483 - 502. ⟨10.1007/s11786-017-0319-z⟩
- Accès au texte intégral et bibtex
-
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
- article
- IJCAI 2017 - 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
-
- 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
- Accès au texte intégral et 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
- CASC 2017 - 19th International Workshop on Computer Algebra in Scientific Computing, Sep 2017, Beijing, China. ⟨10.1007/978-3-319-66320-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Applying a Dependency Mechanism for Voting Protocol Models Using Event-B
- auteur
- Paul J. Gibson, Souad Kherroubi, Dominique Méry
- article
- 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2017), Jun 2017, Neuchâtel, Switzerland. pp.124-138, ⟨10.1007/978-3-319-60225-7_9⟩
- Accès au texte intégral et bibtex
-
- titre
- Explicit modelling of physical measures: from Event-B to Java
- auteur
- John Paul Gibson, Dominique Méry
- article
- IMPEX 2017: 1st International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development, Nov 2017, Xi’An, China. pp.64 - 79, ⟨10.4204/EPTCS.271.5⟩
- Accès au texte intégral et bibtex
-
- titre
- Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
- auteur
- Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- Logical Methods in Computer Science, 2017, 13 (3), ⟨10.23638/LMCS-13(3:27)2017⟩
- Accès au 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. pp.123-137, ⟨10.1007/978-3-319-60170-0_9⟩
- Accès au bibtex
-
- titre
- Superposition: Types and Induction
- auteur
- Daniel Wand
- article
- Computer Science [cs]. Saarland University, 2017. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Bisimulations for Delimited-Control Operators
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- [Research Report] RR-9096, Inria Nancy - Grand Est. 2017
- Accès au texte intégral et 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, ⟨10.1109/LICS.2017.8005071⟩
- Accès au texte intégral et 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, 2017, 16 (4), pp.1083--1115. ⟨10.1007/s10270-015-0504-y⟩
- Accès au bibtex
-
- titre
- A reconstruction of the Mathematical Tables Project’s table of natural logarithms (4 volumes, 1941)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2017
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of the Mathematical Tables Project’s tables of the exponential function exp(x) (1939)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2017
- Accès au texte intégral et bibtex
-
- titre
- Schwilgué's calculating machines -- A collection of articles
- auteur
- Denis Roegel
- article
- [Research Report] LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2017
- Accès au texte intégral et 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. pp.311 - 327, ⟨10.1007/978-3-319-66902-1_19⟩
- Accès au texte intégral et 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. pp.1 - 11, ⟨10.4230/LIPIcs.FSCD.2017.11⟩
- Accès au texte intégral et bibtex
-
- titre
- Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
- article
- [Research Report] RR-9052, Inria. 2017
- Accès au texte intégral et 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, 2017, 39 (3), pp.55-64. ⟨10.1109/MAHC.2017.3481339⟩
- Accès au bibtex
-
- titre
- Satisfiability techniques for computing minimal tie sets in reliability assessment
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- article
- 2017
- Accès au texte intégral et bibtex
-
- titre
- A Case Study on the Parametric Occurrence of Multiple Steady States
- auteur
- Russell Bradford, James H. 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. pp.45-52, ⟨10.1145/3087604.3087622⟩
- Accès au bibtex
-
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- auteur
- Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
- article
- Proc. Conference on Automated Deduction (CADE), 2017, Gotenburg, Sweden. pp.398 - 412, ⟨10.1007/978-3-642-02959-2_10⟩
- Accès au texte intégral et 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
-
- titre
- A fine-grained hierarchy of hard problems in the separated fragment
- auteur
- Marco Voigt
- article
- LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1 - 12, ⟨10.1109/LICS.2017.8005094⟩
- Accès au texte intégral et 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. 9pp., ⟨10.1109/NETSOFT.2017.8004195⟩
- Accès au texte intégral et 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
-
- titre
- Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
- article
- LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩
- Accès au texte intégral et bibtex
-
- titre
- Efficient Parameter Synthesis Using Optimized State Exploration Strategies
- auteur
- Étienne André, Hoang Gia Nguyen, Laure Petrucci
- article
- 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS), Nov 2017, Fukuoka, France. pp.1-10, ⟨10.1109/ICECCS.2017.28⟩
- Accès au 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. Electronic Proceedings in Theoretical Computer Science, 240, 2017, ⟨10.4204/EPTCS.240⟩
- Accès au 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-VPPC 2017 - Vehicle Power and Propulsion Conference, Dec 2017, Belfort, France. ⟨10.1109/VPPC.2017.8330913⟩
- Accès au texte intégral et 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
- CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.77-94, ⟨10.1007/978-3-319-63046-5_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Satisfiability Modulo Bounded Checking
- auteur
- Simon Cruanes
- article
- International Conference on Automated Deduction (CADE), Leonardo de Moura, Aug 2017, Gothenburg, Sweden. pp.114-129, ⟨10.1007/978-3-319-63046-5_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Proving Soundness of Extensional Normal-Form Bisimilarities
- auteur
- Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. ⟨10.1016/j.entcs.2018.03.015⟩
- Accès au texte intégral et 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
- Accès au texte intégral et bibtex
-
- titre
- Congruence Closure with Free Variables
- auteur
- Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
- article
- TACAS 2017 - 23rd International Conference on Tools and Algorithms for Construction and Analysis of Systems, Apr 2017, Uppsala, Sweden. pp.220 - 230, ⟨10.1007/10721959_17⟩
- Accès au texte intégral et bibtex
-
- 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
-
- titre
- Briggs, Henry
- auteur
- Denis Roegel
- article
- Marco Sgarbi. Encyclopedia of Renaissance Philosophy, Springer Verlag, 2017, 978-3-319-02848-4 (Print) 978-3-319-02848-4 (Online)
- Accès au bibtex
-
- titre
- Napier, John
- auteur
- Denis Roegel
- article
- Marco Sgarbi. Encyclopedia of Renaissance Philosophy, Springer Verlag, 2017, 978-3-319-02848-4 (Print) 978-3-319-02848-4 (Online)
- Accès au bibtex
-
- titre
- Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
- auteur
- Andreas Teucke, Christoph Weidenbach
- article
- CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.202-219, ⟨10.1007/978-3-319-63046-5_13⟩
- Accès au texte intégral et 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, 2017, 13 (4), pp.1-54. ⟨10.23638/LMCS-13(4:16)2017⟩
- Accès au texte intégral et bibtex
-
- titre
- Subtropical Satisfiability
- auteur
- Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Vu
- article
- FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. ⟨10.1007/978-3-319-66167-4⟩
- Accès au texte intégral et bibtex
-
- titre
- The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable
- auteur
- Marco Voigt
- article
- FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. pp.244-261, ⟨10.1007/978-3-319-66167-4_14⟩
- Accès au texte intégral et 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
-
- titre
- Playing with State-Based Models for Designing Better Algorithms
- auteur
- Dominique Méry
- article
- Future Generation Computer Systems, 2017, 68, pp.445-455. ⟨10.1016/j.future.2016.04.019⟩
- Accès au bibtex
-
- titre
- New Techniques for Linear Arithmetic: Cubes and Equalities
- auteur
- Martin Bromberger, Christoph Weidenbach
- article
- Formal Methods in System Design, 2017, 51 (3), pp.433-461. ⟨10.1007/s10703-017-0278-7⟩
- Accès au texte intégral et bibtex
-
- titre
- Soundness and Completeness Proofs by Coinductive Methods
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- article
- Journal of Automated Reasoning, 2017, 58 (1), pp.149 - 179. ⟨10.1007/s10817-016-9391-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
- auteur
- Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Christian Sternagel, René Thiemann, Dmitriy Traytel
- article
- Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩
- Accès au texte intégral et bibtex
-
- titre
- What did Napier invent?
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2017
- Accès au texte intégral et bibtex
-
- titre
- Towards Strong Higher-Order Automation for Fast Interactive Verification
- auteur
- Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
- article
- ARCADE 2017 - 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, 2017, Göteborg, Sweden. pp.16-7, ⟨10.29007/3ngx⟩
- Accès au 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
- Accès au texte intégral et bibtex
-
- titre
- A Lambda-Free Higher-Order Recursive Path Order
- auteur
- Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
- article
- Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. pp.461-479, ⟨10.1007/978-3-662-54458-7_27⟩
- Accès au texte intégral et bibtex
-
- titre
- Superposition with Structural Induction
- auteur
- Simon Cruanes
- article
- Clare Dixon; Marcelo Finger. Frontiers of Combining Systems, Springer, pp.172-188, 2017, 11th International Symposium on Frontiers of Combining Systems - FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings, 978-3-319-66166-7. ⟨10.1007/978-3-319-66167-4_10⟩
- Accès au texte intégral et bibtex
-
2016
- titre
- Satisfiability Checking and Symbolic Computation
- auteur
- Thomas Sturm, Erika Abraham, John A. Abbott, Bern W. Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler
- article
- ACM Communications in Computer Algebra, 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
- Accès au bibtex
-
- titre
- Friends with Benefits
- auteur
- Jasmin Christian 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
-
- titre
- A Decision Procedure for (Co)datatypes in SMT Solvers
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette
- article
- IJCAI 2016 - 25th International Joint Conference on Artificial Intelligence, Jul 2016, New York, United States
- Accès au texte intégral et bibtex
-
- titre
- Editorial
- auteur
- Stephan Merz, Jun Pang
- article
- Formal Aspects of Computing, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. ⟨10.1007/s00165-016-0378-y⟩
- Accès au bibtex
-
- titre
- Human Machine : From Interaction to Integration
- auteur
- Rémi Nazin, Didier Fass, J. M. Christian Bastien
- article
- Joint Life Science Meeting ‘Life in Space for Life on Earth’ - 14th European Life Sciences Symposium - 37th Annual International Gravitational Physiology Meeting, CNES, ISGP and ESA, Jun 2016, Toulouse, France
- Accès au texte intégral et 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. pp.1-10
- Accès au texte intégral et 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, ⟨10.1145/2933575.2934532⟩
- Accès au bibtex
-
- titre
- Making explicit domain knowledge in formal system development
- auteur
- Yamine Aït-Ameur, Dominique Méry
- article
- Science of Computer Programming, 2016, 121 (100--127), ⟨10.1016/j.scico.2015.12.004⟩
- Accès au 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
-
- 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
-
- 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
-
- titre
- Better answers to real questions
- auteur
- Marek Košta, Thomas Sturm, Andreas Dolzmann
- article
- Journal of Symbolic Computation, 2016, 74, pp.255 - 275. ⟨10.1016/j.jsc.2015.07.002⟩
- Accès au bibtex
-
- titre
- Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
- auteur
- Martin Bromberger, Christoph Weidenbach
- article
- 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. pp.15-30
- Accès au texte intégral et bibtex
-
- titre
- Interactive Theorem Proving
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- article
- Springer, 9807, 2016, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-43144-4⟩
- Accès au bibtex
-
- titre
- Model Finding for Recursive Functions in SMT
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
- article
- IJCAR 2016 - 8th International Joint Conference on Automated Reasoning, Jun 2016, Coimbra, Portugal. ⟨10.1007/978-3-319-40229-1_10⟩
- Accès au texte intégral et bibtex
-
- titre
- A Learning-Based Fact Selector for Isabelle/HOL
- auteur
- Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
- article
- Journal of Automated Reasoning, 2016, 57, pp.219 - 244. ⟨10.1007/s10817-016-9362-8⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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. ⟨10.1007/978-3-319-40229-1_4⟩
- Accès au texte intégral et 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
-
- 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, ⟨10.1007/978-3-319-46750-4_18⟩
- Accès au texte intégral et bibtex
-
- titre
- Proving Determinacy of the PharOS Real-Time Operating System
- auteur
- Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
- Accès au texte intégral et 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
- ISOLA 2016 , Bernhard Steffen and Tiziana Margaria, Oct 2016, CORFU, Greece. pp.18, ⟨10.1007/978-3-319-47166-2_57⟩
- Accès au bibtex
-
- titre
- Editorial
- auteur
- Stephan Merz, Jun Pang
- article
- Formal Aspects of Computing, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. ⟨10.1007/s00165-016-0390-2⟩
- Accès au bibtex
-
- titre
- Intégration des savoirs et préservation des spécificités
- auteur
- Rémi Nazin
- article
- Journée Internationale des Jeunes Chercheurs 2016, École Doctorale Stanislas (Langage, Temps, Société), Jun 2016, Nancy, France
- Accès au texte intégral et bibtex
-
- titre
- A Rigorous Correctness Proof for Pastry
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.86-101, ⟨10.1007/978-3-319-33600-8_5⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- titre
- Before Torchi and Schwilgué, there was White
- auteur
- Denis Roegel
- article
- IEEE Annals of the History of Computing, 2016, 38 (4), pp.92-93. ⟨10.1109/MAHC.2016.46⟩
- Accès au bibtex
-
- titre
- Encoding TLA+ into Many-Sorted First-Order Logic
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.54-69, ⟨10.1007/978-3-319-33600-8_3⟩
- Accès au texte intégral et bibtex
-
- titre
- Extending Nunchaku to Dependent Type Theory
- auteur
- Simon Cruanes, Jasmin Christian Blanchette
- article
- Hammers for Type Theories (HaTT 2016), Jul 2016, Coimbra, Portugal. pp.3 - 12, ⟨10.4204/EPTCS.210.3⟩
- Accès au texte intégral et bibtex
-
- titre
- Compliance, Functional Safety and Fault Detection by Formal Methods
- auteur
- Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski
- article
- Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016), 2016, Corfu, Greece. pp.626 - 632, ⟨10.1007/978-3-319-47169-3_48⟩
- Accès au texte intégral et bibtex
-
- titre
- Hammering towards QED
- auteur
- Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
- article
- Journal of Formalized Reasoning, 2016, 9 (1), pp.101-148. ⟨10.6092/issn.1972-5787/4593⟩
- Accès au texte intégral et 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
-
- titre
- The interesting linkages for the suspension of the great bell in the cathedral of Metz
- auteur
- Denis Roegel
- article
- [Research Report] Loria & Inria Grand Est. 2016
- Accès au texte intégral et 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
-
- titre
- A new early adding machine by Schwilgué (c. 1840?)
- auteur
- Denis Roegel
- article
- Bulletin of the Scientific Instrument Society, 2016, 130, pp.24-27
- Accès au 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
-
- titre
- Some remarks on Bürgi’s interpolations
- auteur
- Denis Roegel
- article
- 2016
- Accès au texte intégral et bibtex
-
- titre
- Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
- auteur
- Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
- article
- [Research Report] RR-8905, Inria. 2016
- Accès au texte intégral et 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, 2016, ⟨10.1007/s10817-015-9335-3⟩
- Accès au texte intégral et bibtex
-
- titre
- From Event-B specifications to programs for distributed algorithms
- auteur
- Mohamed Mosbah, Mohamed Tounsi, Dominique Mery
- article
- International journal of autonomous and adaptive communications systems, 2016, 9 (3-4), pp.223 - 242. ⟨10.1504/IJAACS.2016.079623⟩
- Accès au bibtex
-
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
- article
- Isabelle Workshop 2016, Aug 2016, Nancy, France
- Accès au texte intégral et bibtex
-
- titre
- Ordered Resolution with Straight Dismatching Constraints
- auteur
- Andreas Teucke, Christoph Weidenbach
- article
- 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, Coimbra, Portugal. pp.95-109
- Accès au texte intégral et bibtex
-
- titre
- L'homme augmenté : Épistémologie et bio-ingénierie de l'humain machine
- auteur
- Didier Fass
- article
- Life Sciences [q-bio]. Université de Lorraine, 2016
- Accès au texte intégral et bibtex
-
- titre
- Fast Cube Tests for LIA Constraint Solving
- auteur
- Martin Bromberger, Christoph Weidenbach
- article
- Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. pp.116-132, ⟨10.1007/978-3-319-40229-1_9⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- titre
- A mechanical calculator for arithmetic sequences (1844-1852): part 2, working details
- auteur
- Denis Roegel
- article
- IEEE Annals of the History of Computing, 2016, 38 (1), pp.80-88. ⟨10.1109/MAHC.2016.3⟩
- Accès au 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
-
- titre
- SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
- auteur
- Eriká H Abrahám, John Abbott, Bernd Becker, Anna M Bigatti, Martin M Brain, Bruno Buchberger, Alessandro Cimatti, James H Davenport, Matthew M England, Pascal Fontaine, Stephen M Forrest, Alberto Griggio, Daniel Kroening, Werner M Seiler, Thomas Sturm
- article
- Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland
- Accès au texte intégral et 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
-
- 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
-
- titre
- Modelling bio-compatible and bio-integrative medical devices
- auteur
- Didier Fass, Dominique Méry
- article
- European & Asian System, Software & Service Process Improvement & Innovation - EUROSPII 2016, Sep 2016, Graz, Austria
- Accès au texte intégral et bibtex
-
- titre
- A Machine-Checked Proof of Correctness of Pastry
- auteur
- Noran Azmy
- article
- Networking and Internet Architecture [cs.NI]. Université de Lorraine, 2016. English. ⟨NNT : 2016LORR0277⟩
- Accès au texte intégral et bibtex
-
2015
- titre
- Human Machine Design
- auteur
- Didier Fass
- article
- Airbus group - Innovations, creative design concept center TXDDI, 2015, Munich, Germany
- Accès au 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. pp.623-637
- Accès au bibtex
-
- titre
- Affordances and safe design of assistance wearable virtual environment of gesture
- auteur
- Didier Fass
- article
- Tared Ahram, Waldemar Karwowski, Dylan Schmorrow. Elsevier, 2015
- Accès au 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
-
- titre
- A Decision Procedure for (Co)datatypes in SMT Solvers
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette
- article
- CADE-25 - The 25th jubilee edition of the International Conference on Automated Deduction, Aug 2015, Berlin, Germany. pp.197-213, ⟨10.1007/978-3-319-21401-6_13⟩
- Accès au texte intégral et bibtex
-
- titre
- Analyzing Requirements Using Environment Modelling
- auteur
- Dominique Mery, Neeraj Kumar Singh
- article
- DHM 2015 - 6th International Conference on Digital Human Modeling Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, Aug 2015, Los Angeles, United States. pp.345-357, ⟨10.1007/978-3-319-21070-4_35⟩
- Accès au texte intégral et 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
-
- 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
-
- titre
- Subtropical Real Root Finding
- auteur
- Thomas Sturm
- article
- Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ACM, Jul 2015, Bath, United Kingdom
- Accès au 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. ⟨10.1145/2729094.2742626⟩
- Accès au texte intégral et bibtex
-
- titre
- Second International Workshop on Formal Integrated Development Environment
- auteur
- Catherine Dubois, Paolo Masci, Dominique Méry
- article
- EPTCS, 187, 2015, EPTCS ⟨10.4204/EPTCS.187⟩
- Accès au bibtex
-
- titre
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- article
- 25th International Conference on Automated Deduction, CADE-25, Christoph Benzmueller, Aug 2015, Berlin, Germany. pp.419-433, ⟨10.1007/978-3-319-21401-6_29⟩
- Accès au texte intégral et 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, 2015, 291, pp.279-302. ⟨10.1016/j.jcp.2015.02.050⟩
- Accès au 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
-
- titre
- Linear Integer Arithmetic Revisited
- auteur
- Martin Bromberger, Thomas Sturm, Christoph Weidenbach
- article
- 2015
- Accès au bibtex
-
- titre
- Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
- auteur
- Marco Voigt, Christoph Weidenbach
- article
- 2015
- Accès au 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
- Accès au texte intégral et bibtex
-
- titre
- Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study
- auteur
- Dominique Méry, Sawant Rushikesh, Anton Tarasyuk
- article
- Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. pp.89-102
- Accès au bibtex
-
- titre
- {NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment
- auteur
- Gábor Alagi, Christoph Weidenbach
- article
- Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), 2015, Wroclaw, Poland. pp.69-84, ⟨10.1007/978-3-319-24246-0_5⟩
- Accès au 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. ⟨10.1007/978-3-319-21073-5_25⟩
- Accès au texte intégral et bibtex
-
- titre
- Integrated human systems design : bridging the gap between formal and experimental approaches
- auteur
- Didier Fass, Dominique Méry
- article
- NASA AMES Research Center, Human Systems Integration Division,, 2015, MOFETT FIELD - Etats-Unis d'Amérique, Unknown Region
- Accès au bibtex
-
- titre
- Affordances and Safe Design of Assistance Wearable Virtual Environment of Gesture
- auteur
- Didier Fass
- article
- Human Factors and Egonomics (AHFE 2015), Jul 2015, Las Vegas, United States. pp.8, ⟨10.1016/j.promfg.2015.07.343⟩
- Accès au texte intégral et bibtex
-
- titre
- Witnessing (Co)datatypes
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- article
- ESOP 2015, Apr 2015, London, United Kingdom. ⟨10.1007/978-3-662-46669-8_15⟩
- Accès au texte intégral et 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
-
- titre
- A Rewriting Approach to the Combination of Data Structures with Bridging Theories
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- article
- Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. pp.275--290, ⟨10.1007/978-3-319-24246-0_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Model Finding for Recursive Functions in SMT
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli
- article
- SMT Workshop 2015 - 13th International Workshop on on Satisfiability Modulo Theories, Jul 2015, San Francisco, United States
- Accès au texte intégral et bibtex
-
- titre
- Modal Tableau Systems with Blocking and Congruence Closure
- auteur
- Renate Schmidt, Uwe Waldmann
- article
- 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wroclaw, Poland. pp.38-53, ⟨10.1007/978-3-319-24312-2_4⟩
- Accès au 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
-
- 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, 2015, 205 (1), pp.202-215. ⟨10.1111/nph.13073⟩
- Accès au texte intégral et bibtex
-
- 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
-
- titre
- Beagle – A Hierarchic Superposition Prover
- auteur
- Peter Baumgartner, Joshua Bax, Uwe Waldmann
- article
- 25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. pp.367-377, ⟨10.1007/978-3-319-21401-6_25⟩
- Accès au 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
-
- titre
- Foreword to the Special Focus on Constraints and Combinations
- auteur
- Pascal Fontaine, Thomas Sturm, Uwe Waldmann
- article
- Dongming Wang. Springer, 9 (3), 2015, Mathematics in Computer Science, ⟨10.1007/s11786-015-0239-8⟩
- Accès au bibtex
-
- titre
- Congruence Closure with Free Variables (Work in Progress)
- auteur
- Haniel Barbosa, Pascal Fontaine
- article
- QUANTIFY 2015 - 2nd International Workshop on Quantification, Aug 2015, Berlin, Germany
- Accès au texte intégral et bibtex
-
- titre
- Foundational Extensible Corecursion: A Proof Assistant Perspective
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- article
- ICFP 2015, Aug 2015, Vancouver, Canada. ⟨10.1145/2784731.2784732⟩
- Accès au texte intégral et bibtex
-
- titre
- Better Answers to Real Questions
- auteur
- Marek Kosta, Thomas Sturm, Andreas Dolzmann
- article
- 2015
- Accès au 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
- SCRATCH, Aug 2015, Amsterdam, Netherlands
- Accès au texte intégral et 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
-
- 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. ⟨10.1007/978-3-319-20615-8_1⟩
- Accès au texte intégral et 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, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩
- Accès au texte intégral et 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
-
- titre
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation
- auteur
- Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
- article
- Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. pp.151-166, ⟨10.1007/978-3-319-24246-0_10⟩
- Accès au texte intégral et bibtex
-
- titre
- Human Machine Epistemology Survey
- auteur
- Rémi Nazin, Didier Fass
- article
- HCI Interantional 2016, Aug 2015, Los Angeles, United States. pp.12, ⟨10.1007/978-3-319-21073-5_35⟩
- Accès au texte intégral et 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
-
- 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, 2015, 37 (4), pp.90-96. ⟨10.1109/MAHC.2015.79⟩
- Accès au 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
-
- titre
- An overview of Schwilgué's patented adding machines
- auteur
- Denis Roegel
- article
- Bulletin of the Scientific Instrument Society, 2015, 126, pp.16-22
- Accès au 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
-
- titre
- Software Component Design with the B Method — A Formalization in Isabelle/HOL
- auteur
- David Déharbe, Stephan Merz
- article
- Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. pp.31-47, ⟨10.1007/978-3-319-28934-2_2⟩
- Accès au texte intégral et 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
-
- titre
- L'homme augmenté
- auteur
- Didier Fass
- article
- Séminaire équipe PerSeUS, Université de Lorraine,, 2015, METZ, France
- Accès au bibtex
-
- titre
- A Generalized Framework for Virtual Substitution
- auteur
- Marek Kosta, Thomas Sturm
- article
- 2015, pp.17
- Accès au bibtex
-
2014
- 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
-
- titre
- Reclaiming human machine nature
- auteur
- Didier Fass
- article
- Vincent G. Dufy. NC, 8529 (8529), Springer International Publishing, pp.588-599, 2014
- Accès au 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
-
- titre
- Integrating SMT solvers in Rodin
- auteur
- David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
- article
- Science of Computer Programming, 2014, Abstract State Machines, Alloy, B, VDM, and Z — Selected and extended papers from ABZ 2012, 94, pp.14
- Accès au 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
-
- titre
- Both Structural and Non-Structural Forms of the Readthrough Protein of Cucurbit aphid-borne yellows virus Are Essential for Efficient Systemic Infection of Plants
- auteur
- Sylvaine Boissinot, Monique Erdinger, Baptiste Monsion, Véronique Ziegler-Graff, Véronique Brault
- article
- PLoS ONE, 2014, 9 (4), pp.1-10. ⟨10.1371/journal.pone.0093448⟩
- Accès au texte intégral et 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
-
- titre
- Towards Conflict-Driven Learning for Virtual Substitution
- auteur
- Konstantin Korovin, Marek Kosta, Thomas Sturm
- article
- Computer Algebra in Scientific Computing - 16th International Workshop, CASC 2014, 2014, Warsaw, Poland. pp.256-270
- Accès au bibtex
-
- titre
- Reclaiming Human Machine Nature
- auteur
- Didier Fass
- article
- 16th International Conference on Human-Computer Interaction, 2014, Crete, Greece
- Accès au 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
- Accès au 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
- Accès au texte intégral et 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. pp.122-136, ⟨10.1007/978-3-319-08587-6_9⟩
- Accès au bibtex
-
- titre
- Easter bracelets for 5700000 years
- auteur
- Denis Roegel
- article
- [Research Report] 2014
- Accès au texte intégral et 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
-
- titre
- Reclaiming human machine nature
- auteur
- Didier Fass
- article
- HCI International 2014, Jul 2014, Heraklion, Greece. pp.588-589
- Accès au texte intégral et 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
-
- titre
- Science of Computer Programming Special Issue: Automated Verification of Critical Systems
- auteur
- Gerald Lüttgen, Stephan Merz
- article
- Elsevier, 96 (3), 2014, Science of Computer Programming, Jan Bergstra
- Accès au bibtex
-
- titre
- Polymorphic+Typeclass Superposition
- auteur
- Daniel Wand
- article
- 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
- Accès au texte intégral et bibtex
-
- titre
- Better Answers to Real Questions
- auteur
- Marek Kosta, Thomas Sturm, Andreas Dolzmann
- article
- 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Philipp Rümmer and Christoph M. Wintersteiger, Jul 2014, Vienna, Austria. pp.69
- Accès au bibtex
-
- titre
- Modeling an Aircraft Landing System in Event-B
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. pp.154-159
- Accès au 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
-
- titre
- On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
- auteur
- Yamine Aït-Ameur, John Paul Gibson, Dominique Méry
- article
- 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Specialized Techniques and Applications (ISoLA 2014), Oct 2014, Corfu, Greece. pp.604-618, ⟨10.1007/978-3-662-45231-8_50⟩
- Accès au texte intégral et bibtex
-
- titre
- Finite Quantification in Hierarchic Theorem Proving
- auteur
- Peter Baumgartner, Joshua Bax, Uwe Waldmann
- article
- 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. pp.152-167
- Accès au bibtex
-
- titre
- BDI: a new decidable clause class
- auteur
- Manuel Lamotte-Schubert, Christoph Weidenbach
- article
- Journal of Logic and Computation, 2014, 24 (6), pp.28
- Accès au 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, Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, Jul 2014, Vienna, Austria
- Accès au bibtex
-
- titre
- Editorial: Special Issue of Automated Verification of Critical Systems
- auteur
- Gerald Lüttgen, Stephan Merz
- article
- Science of Computer Programming, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
- Accès au bibtex
-
- titre
- Formal Evaluation of Landing Gear System
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam
- Accès au 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⟩
- Accès au 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
-
- titre
- The Semantics of Refinement Chart
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- HCI International, Jun 2014, Heraklion, Greece. pp.415-426, ⟨10.1007/978-3-319-07725-3_42⟩
- Accès au 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. EPTCS, 149, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩
- Accès au bibtex
-
- titre
- Playing with State-Based Models for Designing Better Algorithms
- auteur
- Dominique Méry
- article
- Model and Data Engineering - 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. pp.1-3
- Accès au 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/978-3-319-10882-7⟩
- Accès au bibtex
-
- titre
- Constructing a single cell in cylindrical algebraic decomposition
- auteur
- Christopher W. Brown, Marek Kosta
- article
- Journal of Symbolic Computation, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩
- Accès au 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 - The first International Workshop on Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. pp.1-16
- Accès au texte intégral et 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, 2014, Computer Science and Information System, 11 (1), pp.251-270. ⟨10.2298/CSIS130122007A⟩
- Accès au 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
-
- titre
- Easter-based walks on a sphere
- auteur
- Denis Roegel
- article
- [Research Report] 2014
- Accès au texte intégral et bibtex
-
- titre
- The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
- auteur
- Dominique Méry, Bernhard Schätz, Alan Wassyng
- article
- Dagstuhl Reports, 2014, 4 (2), pp.17--37
- Accès au bibtex
-
- titre
- Analysis of Self-* and P2P Systems using Refinement
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- article
- ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Yamine AIT AMEUR and Klaus-Dieter SCHEWE, Jun 2014, Toulouse, France. pp.117-123, ⟨10.1007/978-3-662-43652-3_9⟩
- Accès au 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
-
- titre
- The strange beauty of the twilight flower
- auteur
- Denis Roegel
- article
- [Research Report] 2014
- Accès au texte intégral et bibtex
-
- titre
- Flip-Pushdown Automata with $k$ Pushdown Reversals and E0L Systems are Incomparable
- auteur
- Marek Kosta, Pavol Duris
- article
- Information Processing Letters, 2014, 114 (8), pp.417-420. ⟨10.1016/j.ipl.2014.03.003⟩
- Accès au bibtex
-
- titre
- Refinement Types for TLA+
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩
- Accès au 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
-
- 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
-
- titre
- Bounding messages for free in security protocols – extension to various security properties
- auteur
- Myrto Arapinis, Marie Duflot
- article
- Information and Computation, 2014, pp.34. ⟨10.1016/j.ic.2014.09.003⟩
- Accès au texte intégral et bibtex
-
2013
- titre
- Computing prime implicants
- auteur
- David Deharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
- article
- 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD'13), Oct 2013, Portland, Oregon, United States. pp.46-52, ⟨10.1109/FMCAD.2013.6679390⟩
- Accès au 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
-
- titre
- Hierarchic Superposition: Completeness without Compactness
- auteur
- Peter Baumgartner, Uwe Waldmann
- article
- MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12
- Accès au bibtex
-
- 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
-
- 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
-
- 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, Astrium and Technische Universität München, Jul 2013, Munich, Germany
- Accès au texte intégral et bibtex
-
- titre
- Towards Certifying Network Calculus
- auteur
- Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
- article
- ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.484-489, ⟨10.1007/978-3-642-39634-2_37⟩
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- titre
- Approche théorique et expérimentale de l’intégration humain machine
- auteur
- Didier Fass
- article
- ONERA - Centre de recherche de l’Ecole de l’air, 2013, Salon de Provence, France
- Accès au 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
- Accès au 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. Dagstuhl, 3, pp.16, 2013, Dagstuhl Reports, ⟨10.4230/DagRep.3.4.1⟩
- Accès au 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
-
- 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
-
- 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
-
- titre
- Ideal Mode Selection of a Cardiac Pacing System
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- 4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. pp.258-267, ⟨10.1007/978-3-642-39173-6_31⟩
- Accès au 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
- CASC 2013 - 15th International Workshop on Computer Algebra in Scientific Computing, Sep 2013, Berlin, Germany. pp.88-99, ⟨10.1007/978-3-319-02297-0_7⟩
- Accès au 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
-
- titre
- Formal Modelling and Verification of Population Protocols
- auteur
- Dominique Méry, Mike Poppleton
- article
- iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland
- Accès au 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
- Accès au 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. pp.316-325, ⟨10.1007/978-3-642-39173-6_37⟩
- Accès au texte intégral et 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
-
- 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 : le magazine de l'ingénierie du logiciel et des systèmes, 2013, Mars 2013 (104), pp.29-39
- Accès au texte intégral et 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
- Accès au bibtex
-
- titre
- Transforming EVENT B Models into Verified C# Implementations
- auteur
- Dominique Méry, Monahan Rosemary
- article
- VPT 2013 - First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
- Accès au bibtex
-
- titre
- The emerging family of CULLIN3-RING ubiquitin ligases (CRL3s): cellular functions and disease implications
- auteur
- Pascal Genschik, Izabela Sumara, Esther Lechner
- article
- EMBO Journal, 2013, 32 (17), pp.2307-2320. ⟨10.1038/emboj.2013.173⟩
- Accès au bibtex
-
- titre
- Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
- auteur
- Ralf Karrenberg, Marek Kosta, Thomas Sturm
- article
- 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. pp.56-70, ⟨10.1007/978-3-642-40885-4_5⟩
- Accès au 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
-
- titre
- Hierarchic Superposition With Weak Abstraction
- auteur
- Peter Baumgartner, Uwe Waldmann
- article
- 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. pp.39-57, ⟨10.1007/978-3-642-38574-2_3⟩
- Accès au bibtex
-
- titre
- From Event-B Specifications to Programs for Distributed Algorithms
- auteur
- Mohammed Tounsi, Mohammed Mosbah, Dominique Méry
- article
- WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩
- Accès au 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), 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩
- Accès au 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
-
- 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
-
- titre
- A reconstruction of Magini's Tabula tetragonica (1592)
- auteur
- Denis Roegel
- article
- [Research Report] 2013
- Accès au texte intégral et 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
-
- titre
- Frontiers of Combining Systems
- auteur
- Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
- article
- Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. Springer, 8152, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
- Accès au bibtex
-
- titre
- A reconstruction of Herwart's table of multiplication (1610)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2013
- Accès au texte intégral et bibtex
-
- titre
- Theoretical and experimental approach of human machine integration
- auteur
- Didier Fass
- article
- NASA AMES Research Center, Human systems integration division, 2013, Mofett Field - Etats-Unis d'Amérique, Unknown Region. ⟨10.5772/33373⟩
- Accès au 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
-
2012
- 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
-
- 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
- Accès au texte intégral et bibtex
-
- titre
- Formal Verification Of Pastry Using TLA+
- auteur
- Tianxiang Lu, Stephan Merz, Christoph Weidenbach
- article
- International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France
- Accès au texte intégral et 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
- Accès au 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
-
- titre
- La numérisation durable
- auteur
- Denis Roegel
- article
- [Rapport de recherche] LORIA - Université de Lorraine. 2012
- Accès au texte intégral et bibtex
-
- titre
- Handling Heterogeneity in Formal Developments of Hardware and Software Systems
- auteur
- Yamine Aït-Ameur, Dominique Méry
- article
- ISoLA - 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - 2012, Tiziana Margaria and Bernhard Steffen, Oct 2012, Amirandes, Heraklion, Greece. pp.327-328, ⟨10.1007/978-3-642-34032-1_33⟩
- Accès au bibtex
-
- 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
-
- 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
-
- titre
- Stuttering Equivalence
- auteur
- Stephan Merz
- article
- [Research Report] 2012
- Accès au bibtex
-
- titre
- The LOCOMAT Project: Recomputing Mathematical and Astronomical Tables
- auteur
- Denis Roegel
- article
- IEEE Annals of the History of Computing, 2012, 34 (2), pp.74-79. ⟨10.1109/MAHC.2012.32⟩
- Accès au bibtex
-
- titre
- Harnessing SMT Solvers for TLA+ Proofs
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany
- Accès au texte intégral et 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), Mostefa BELARBI - University of Tiaret - Algeria, Dec 2012, Tiaret, Algeria
- Accès au texte intégral et 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
-
- 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. pp.3-12, ⟨10.1145/2350716.2350720⟩
- Accès au 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, 2012, 77 (10-11), pp.1122-1150
- Accès au 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
-
- titre
- A reconstruction of Crelle’s table of primes
- auteur
- Denis Roegel
- article
- [Research Report] Loria & Inria Grand Est. 2012
- Accès au texte intégral et bibtex
-
- titre
- More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification
- auteur
- Jasmin Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
- article
- Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. pp.345-360
- Accès au 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
-
- titre
- TLA+ Proofs
- auteur
- Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
- article
- 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩
- Accès au texte intégral et 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
-
- titre
- Sustainable digitization
- auteur
- Denis Roegel
- article
- [Research Report] LORIA - Université de Lorraine. 2012
- Accès au texte intégral et 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
-
2011
- 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
-
- 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
-
- titre
- A reconstruction of Chernac's Cribrum arithmeticum (1811)
- auteur
- Denis Roegel
- article
- [Research Report] 2011
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
- Accès au 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- titre
- A reconstruction of the tables of the Shuli Jingyun (1713-1723)
- auteur
- Denis Roegel
- article
- [Research Report] Loria & Inria Grand Est. 2011
- Accès au texte intégral et bibtex
-
- titre
- A reconstruction of Crelle's Rechentafeln (1820)
- auteur
- Denis Roegel
- article
- [Research Report] 2011
- Accès au texte intégral et 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. à paraître
- Accès au 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
-
- titre
- Human systems integration design: which generalized rationale?
- auteur
- Romain Lieber, Didier Fass
- article
- 14th International Conference on Human-Computer Interaction, HCI International 2011, Jul 2011, Orlando, Florida, United States. pp.101-109, ⟨10.1007/978-3-642-21753-1_12⟩
- Accès au texte intégral et bibtex
-
- titre
- Verification and synthesis using real quantifier elimination
- auteur
- Thomas Sturm, Ashish Tiwari
- article
- Proc. ISSAC 2011, Jun 2011, San Jose, United States. pp.329, ⟨10.1145/1993886.1993935⟩
- Accès au 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
-
- 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
-
- 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
-
- titre
- Analysis of DSR Protocol in Event-B
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. pp.401-415
- Accès au 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
-
- titre
- Medical Protocol Diagnosis using Formal Methods
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa
- Accès au 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- titre
- A reconstruction of Merritt's Brocot table (1947)
- auteur
- Denis Roegel
- article
- [Research Report] 2011
- Accès au texte intégral et bibtex
-
- titre
- A generic framework: from modeling to code
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- Innovations in Systems and Software Engineering (ISSE), 2011, pp.1-9
- Accès au bibtex
-
- titre
- EB2J : Code Generation from Event-B to Java
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- SBMF - Brazilian Symposium on Formal Methods, CBSoft - Brazilian Conference on Software: Theory and Practice, Sep 2011, São Paulo, Brazil
- Accès au 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
-
- 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
-
- titre
- A reconstruction of Crelle's Erleichterungstafel (1836)
- auteur
- Denis Roegel
- article
- [Research Report] 2011
- Accès au texte intégral et bibtex
-
- titre
- Formalisation of the Heart based on Conduction of Electrical Impulses and Cellular-Automata
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- International Symposium on Foundations of Health Information Engineering and Systems (FHIES, 2011), Aug 2011, Johannesburg, South Africa
- Accès au 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
-
- titre
- Tissot's table of logarithms (ca. 1880)
- auteur
- Denis Roegel
- article
- [Research Report] 2011
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- titre
- Automatic Code Generation from Event-B Models
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- SoICT 2011, Hanoi University, Oct 2011, Hanoi, Vietnam
- Accès au bibtex
-
2010
- titre
- O rozboru jednoho makra
- auteur
- Denis Roegel
- article
- Zpravodaj (Československého sdružení uživatelů TeXu, ISSN 1211-6661), 2010, 20 (1-2), pp.68-76
- Accès au texte intégral et 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
-
- titre
- Proving Distributed Algorithms by Combining Refinement and Local Computations
- auteur
- Dominique Méry, Mohammed Mosbah, Mohammed Tounsi
- article
- AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Sep 2010, Dusseldorf, Germany
- Accès au 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
-
- 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
- Accès au 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, 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
-
- 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
-
- 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
-
- 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
-
- titre
- Real-Time Animation for Formal Specification
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- Complex Systems Design & Management 2010, Oct 2010, Paris, France. pp.49-60, ⟨10.1007/978-3-642-15654-0_3⟩
- Accès au texte intégral et bibtex
-
- titre
- Specifying and Verifying PLC systems with TLA+: a case study
- auteur
- Hehua Zhang, Stephan Merz, Ming Gu
- article
- Computers & Mathematics with Applications, 2010, 60 (3), pp.695-705. ⟨10.1016/j.camwa.2010.05.017⟩
- Accès au 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, 2010, 240 (2 July 2009), pp.113-128. ⟨10.1016/j.entcs.2009.05.048⟩
- Accès au 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), 2010, 20 (1-2), pp.23-38
- Accès au texte intégral et bibtex
-
- titre
- Proof-Based Design of Security Protocols
- auteur
- Nazim Benaissa, Dominique Méry
- article
- 5th International Computer Science Symposium in Russia, CSR 2010, Farid Ablayev, Jun 2010, KAZAN, Russia. pp.25-36
- Accès au 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
-
- 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
-
- titre
- A reconstruction of Edward Sang's table of logarithms (1871)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2010
- Accès au texte intégral et bibtex
-
- titre
- EB2C : A Tool for Event-B to C Conversion Support
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- 2010
- Accès au texte intégral et bibtex
-
- titre
- The TLA+ Proof System: Building a Heterogeneous Verification Platform
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- article
- International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩
- Accès au 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
-
- 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
-
- titre
- A construction of Edward Sang's projected table of nine-place logarithms to one million (1872)
- auteur
- Denis Roegel
- article
- [Research Report] LORIA (Université de Lorraine, CNRS, INRIA). 2010
- Accès au texte intégral et 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), 2010, 20 (3), pp.138-151
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- titre
- Functional Behavior of a Cardiac Pacing System
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- International Journal of Discrete Event Control Systems (IJDECS), 2010
- Accès au bibtex
-
- titre
- Trustable Formal Specification for Software Certification
- auteur
- Dominique Méry, Neeraj Kumar Singh
- article
- 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, Oct 2010, Heraklion, Crete, Greece. pp.312-326, ⟨10.1007/978-3-642-16561-0_31⟩
- Accès au 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
-
- 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), 2010, 20 (3), pp.220-226
- Accès au texte intégral et 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
-
- 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
-
- 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
-
- titre
- Napier's ideal construction of the logarithms
- auteur
- Denis Roegel
- article
- [Research Report] 2010
- Accès au texte intégral et 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
-
- 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), 2010, 44 (9-10), pp.1119-1163. ⟨10.3166/jesa.44.1119-1163⟩
- Accès au bibtex
-
2009
- titre
- MetaPost macros for drawing Chinese and Japanese abaci
- auteur
- Denis Roegel
- article
- Tugboat, 2009, 30 (1), pp.74-79
- Accès au bibtex
-
- titre
- veriT: an open, trustable and efficient SMT-solver
- auteur
- Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
- article
- 22nd International Conference on Automated Deduction - CADE 22, Aug 2009, Montreal, Canada. pp.151-156, ⟨10.1007/978-3-642-02959-2_12⟩
- Accès au 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
-
- 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
- Accès au texte intégral et 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
- Accès au 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
- Accès au texte intégral et 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
-
- titre
- Design et ingénierie des systèmes homme-dans-la boucle
- auteur
- Didier Fass
- article
- La revue des Mines, 2009, R&D dans la santé: et demain ?, 440, pp.50-51
- Accès au texte intégral et bibtex
-
- titre
- A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
- auteur
- Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz
- article
- Reachability Problems 2009, Sep 2009, Palaiseau, France. pp.93-106, ⟨10.1007/978-3-642-04420-5_10⟩
- Accès au 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, 2009, 11 (3), pp.217-238. ⟨10.1007/s10009-009-0104-7⟩
- Accès au 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, Technische Universität München, Aug 2009, Munich, Germany
- Accès au texte intégral et 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, 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
-
- 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
-
- 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
- Accès au bibtex
-
- titre
- Refinement-Based Guidelines for Algorithmic Systems
- auteur
- Dominique Méry
- article
- International Journal of Software and Informatics (IJSI), 2009, 3 (2-3), pp.197-239
- Accès au 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
-
- titre
- An introduction to nomography: Garrigues' nomogram for the computation of Easter
- auteur
- Denis Roegel
- article
- Tugboat, 2009, 30 (1), pp.88-104
- Accès au bibtex
-
- titre
- Spheres, great circles and parallels
- auteur
- Denis Roegel
- article
- Tugboat, 2009, 30 (1), pp.80-87
- Accès au 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
-
- titre
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- auteur
- Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
- article
- 22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009, Aug 2009, Munich, Germany. pp.424-439, ⟨10.1007/978-3-642-03359-9_29⟩
- Accès au 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. pp.27-30
- Accès au texte intégral et 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
- Accès au texte intégral et bibtex
-
- titre
- A Simple Refinement-based Method for Constructing Algorithms
- auteur
- Dominique Méry
- article
- Sigcse Bulletin, 2009, inroads — SIGCSE Bulletin, 41 (2), pp.51-59. ⟨10.1145/1595453.1595462⟩
- Accès au bibtex
-
- titre
- A Rodin plugin for quantitative timed models
- auteur
- Joris Rehm
- article
- Rodin User and Developer Workshop, Jul 2009, Southampton, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Prototype Fragments from Babbage's First Difference Engine
- auteur
- Denis Roegel
- article
- IEEE Annals of the History of Computing, 2009, 31 (2), pp.70-75
- Accès au 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
- Accès au bibtex
-
- titre
- The eroding rotation: Why digital pictures should not be rotated
- auteur
- Denis Roegel
- article
- [Research Report] Loria & Inria Grand Est. 2009
- Accès au texte intégral et 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), 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303
- Accès au bibtex
-
- titre
- Combinations of theories for decidable fragments of first-order logic
- auteur
- Pascal Fontaine
- article
- 7th International Symposium, FroCoS 2009, Sep 2009, Trento, Italy. pp.263-278, ⟨10.1007/978-3-642-04222-5_16⟩
- Accès au bibtex
-
2008
- 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
- Accès au texte intégral et 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
- Accès au texte intégral et 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. Springer, 41, pp.209, 2008, Journal of Automated Reasoning
- Accès au 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
- The Plant cell, 2008, 20 (3), pp.752-767. ⟨10.1105/tpc.107.054858⟩
- Accès au texte intégral et 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
-
- 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
-
- titre
- Teaching programming methodology using Event B
- auteur
- Dominique Méry
- article
- The B Method: from Research to Teaching, Henri Habrias, Jul 2008, Nantes, France
- Accès au texte intégral et bibtex
-
- 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
-
- 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
-
- titre
- Combining decision procedures by (model-)equality propagation
- auteur
- Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
- article
- Brazilian Symposium on Formal Methods - SBMF 2008, Aug 2008, Salvador, Bahia, Brazil
- Accès au bibtex
-
- titre
- The Specification Language TLA+
- auteur
- Stephan Merz
- article
- Dines Bjoerner 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
-
- 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
-
- 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
-
- titre
- Kanji-Sudokus: Integrating Chinese and Graphics
- auteur
- Denis Roegel
- article
- Tugboat, 2008, 29 (2), pp.317-319
- Accès au 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
-
- titre
- Modelling Attacker's Knowledge for Cascade Cryptographic Protocols
- auteur
- Nazim Benaissa
- article
- First International Conference on Abstract State Machines, B and Z - ABZ 2008, Sep 2008, London, United Kingdom. pp.251-264, ⟨10.1007/978-3-540-87603-8_20⟩
- Accès au texte intégral et 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
-
- titre
- An Early (1844) Key-Driven Adding Machine
- auteur
- Denis Roegel
- article
- IEEE Annals of the History of Computing, 2008, 30 (1), pp.59-65. ⟨10.1109/MAHC.2008.1⟩
- Accès au bibtex
-
- titre
- Formal Verification of Distributed Algorithms in +CAL 2.0
- auteur
- Sabina Akhtar
- article
- 2008
- Accès au 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
-
- 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
-
- 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, 2008, 183, pp.39-55. ⟨10.1016/j.entcs.2007.01.060⟩
- Accès au bibtex
-
2007
- 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
-
- titre
- haRVey : satisfaisabilité et théories
- auteur
- Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. pp.287-288
- Accès au 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
-
- titre
- Patrons de conception prouvés
- auteur
- Thierry Lecomte, Dominique Méry, Dominique Cansell
- article
- Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2007, Ingénierie dirigée par les modèles, 81 (juin 2007), pp.14-18
- Accès au bibtex
-
- titre
- Formal verification of tamper-evident storage for e-voting
- auteur
- Dominique Cansell, Paul Gibson, Dominique Méry
- article
- 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. pp.329-338, ⟨10.1109/SEFM.2007.21⟩
- Accès au texte intégral et 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
- Accès au bibtex
-
- titre
- Time Constraint Patterns for Event B Development
- auteur
- Dominique Cansell, Dominique Méry, Joris Rehm
- article
- 7th International Conference of B Users, January 17-19, 2007, 2007, Besançon, France. pp.140-154, ⟨10.1007/11955757_13⟩
- Accès au texte intégral et bibtex
-
- titre
- Modelling and Proof Analysis of Interrupt Driven Scheduling
- auteur
- Bill Stoddart, Dominique Cansell, Frank Zeyda
- article
- The 7th International B Conference - B 2007, Jacques Jullian et Olga Kouchnarenko, Jan 2007, Besançon/France, pp.155-170, ⟨10.1007/11955757_14⟩
- Accès au bibtex
-
- titre
- A Formal Approach for the Development of Automated Systems
- auteur
- Olfa Mosbahi, Leila Jemni, Jacques Jaray
- article
- 2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.304-310
- Accès au texte intégral et bibtex
-
- titre
- A complex drawing in descriptive geometry
- auteur
- Denis Roegel
- article
- Tugboat, 2007, 28 (2), pp.218-228
- Accès au 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
-
- 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
- ISoLA 2007 Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Dec 2007, Poitiers-Futuroscope, France. pp.179-190
- Accès au texte intégral et 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
- The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13
- Accès au bibtex
-
- titre
- Incremental Parametric Development of Greedy Algorithms
- auteur
- Dominique Cansell, Dominique Méry
- article
- Electronic Notes in Theoretical Computer Science, 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
-
- titre
- Proved-Patterns-Based Development for Structured Programs.
- auteur
- Dominique Cansell, Dominique Méry
- article
- Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Ural State University (USU) ; Institute of Mathematics and Mechanics of Ural Branch of Russian Academy of Sciences, Sep 2007, Ekaterinburg, Russia. pp.104-114, ⟨10.1007/978-3-540-74510-5_13⟩
- Accès au bibtex
-
- titre
- Sphères, grands cercles et parallèles
- auteur
- Denis Roegel
- article
- Cahiers Gutenberg, 2007, Avril 2007 (48), pp.7-22
- Accès au bibtex
-
- titre
- Dérivation d'algorithmes sans verrou à partir d'une spécification atomique
- auteur
- Loïc Fejoz, Stephan Merz
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Marie-Laure Potet (IMAG, Grenoble) ; Pierre-Yves Schobbens (Facultés Universitaires Notre-Dame de la Paix - Namur, Belgique), Jun 2007, Namur, Belgique. pp.213-226
- Accès au texte intégral et 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, 2007, 19 (3), pp.321-341. ⟨10.1007/s00165-007-0027-6⟩
- Accès au texte intégral et bibtex
-
- titre
- Secure Information Flow for a Concurrent Language with Scheduling
- auteur
- Gilles Barthe, Leonor Prensa Nieto
- article
- Journal of Computer Security, 2007, Formal Methods in Security Engineering Workshop (FMSE 04), 16 (6), pp.647 - 689
- Accès au texte intégral et bibtex
-
- titre
- Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)
- auteur
- Stephan Merz, Tobias Nipkow
- article
- Michael Mislove. Elsevier, 185, pp.151, 2007, Electronic Notes in Theoretical Computer Science
- Accès au bibtex
-
- titre
- Predicate Diagrams for the Verification of Real-Time Systems
- auteur
- Eunyoung Kang, Stephan Merz
- article
- Formal Aspects of Computing, 2007, 19 (3), pp.401-413. ⟨10.1007/s00165-007-0030-y⟩
- Accès au texte intégral et bibtex
-
- titre
- Specification and Proof of Liveness Properties in B Event Systems
- auteur
- Olfa Mosbahi, Jacques Jaray
- article
- 2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.25-34
- Accès au texte intégral et bibtex
-
- titre
- Vérification formelle d'algorithmes distribués en +CAL
- auteur
- Sebti Mouelhi
- article
- 2007
- Accès au bibtex
-
- titre
- Review of ``Mathematical Illustrations: A Manual of Geometry and PostScript
- auteur
- Denis Roegel
- article
- Notices of the American Mathematical Society, 2007, 54 (1), pp.38-42
- Accès au 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. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class
- auteur
- Pascal Fontaine
- article
- 4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. pp.37-54
- Accès au 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
- Accès au texte intégral et 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
-
- titre
- Développement formel de circuits électroniques par la méthode B
- auteur
- Yann Zimmermann
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Pierre-Yves Schobbens, Jun 2007, Namur, Belgique. pp.181-198
- Accès au bibtex
-
- titre
- Specification and Refinement of Access Control
- auteur
- Dominique Méry, Stephan Merz
- article
- Journal of Universal Computer Science, 2007, 13 (8), pp.1073-1093
- Accès au bibtex
-
2006
- 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
-
- 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
-
- titre
- Proof reconstruction for first-order logic and set-theoretical constructions
- auteur
- Clément Hurlin
- article
- Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.157-162
- Accès au texte intégral et 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
- Accès au texte intégral et 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
- 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, pp.167-181, ⟨10.1007/11691372_11⟩
- Accès au 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, 2006, ⟨10.1016/j.tcs.2006.08.015⟩
- Accès au 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
-
- 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
-
- titre
- Decision Procedures for the Formal Analysis of Software
- auteur
- David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
- article
- 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, Nov 2006, Tunis, Tunisia, pp.366--370, ⟨10.1007/11921240_26⟩
- Accès au 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
- Accès au 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, pp.1840-1844
- Accès au texte intégral et bibtex
-
- titre
- Incremental Parametric Development of Greedy Algorithms
- auteur
- Dominique Cansell, Dominique Méry
- article
- 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62
- Accès au texte intégral et 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
- Accès au texte intégral et bibtex
-
- titre
- Airy's On the Disturbances of Pendulums and Balances, and on the Theory of Escapements (1830)
- auteur
- Denis Roegel
- article
- 2006
- Accès au texte intégral et 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. pp.457-469
- Accès au 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, 2006, 351 (2), pp.184--202. ⟨10.1016/j.tcs.2005.09.067⟩
- Accès au texte intégral et 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
- May 2006, pp.CDROM
- Accès au bibtex
-
- titre
- Event Systems and Access Control
- auteur
- Dominique Méry, Stephan Merz
- article
- Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, Mar 2006, Vienna/Austria, pp.40-54
- Accès au texte intégral et bibtex
-
- 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
-
- titre
- A method to refine time constraints in event B framework
- auteur
- Joris Rehm
- article
- Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.173-177
- Accès au texte intégral et bibtex
-
- titre
- haRVey: combining reasoners
- auteur
- David Déharbe, Pascal Fontaine
- article
- Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156
- Accès au texte intégral et bibtex
-
2005
- 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
- Accès au 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, 2005, 302 (Avril), 11 p
- Accès au bibtex
-
- titre
- Truly On-The-Fly LTL Model Checking
- auteur
- Moritz Hammer, Alexander Knapp, Stephan Merz
- article
- Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Apr 2005, Edinburgh / U.K., pp.191-205
- Accès au texte intégral et bibtex
-
- titre
- Combining Lists with Non-Stably Infinite Theories
- auteur
- Pascal Fontaine, Silvio Ranise, Calogero G. Zarba
- article
- 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), Mar 2005, Montevideo/Uruguay, pp.51--66, ⟨10.1007/b106931⟩
- Accès au texte intégral et 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
- Accès au texte intégral et 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
- Accès au bibtex
-
- 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
-
- 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, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK
- Accès au texte intégral et bibtex
-
- titre
- A Formalization of a Generalized Clock Synchronization Protocol in Isabelle/HOL
- auteur
- Alwen Tiu
- article
- 2005
- Accès au 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, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770
- Accès au bibtex
-
- titre
- Component Reuse in B Using ACL2
- auteur
- Yann Zimmermann, Diana Toma
- article
- 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, pp.280-299, ⟨10.1007/b135596⟩
- Accès au texte intégral et 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
- Accès au texte intégral et 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 : le magazine de l'ingénierie du logiciel et des systèmes, 2005, 73, pp.44-50
- Accès au texte intégral et bibtex
-
- titre
- Kissing Circles: A French Romance in METAPOST
- auteur
- Denis Roegel
- article
- Tugboat, 2005, 26 (1), pp.10-17
- Accès au bibtex
-
- titre
- Arabidopsis cyp51 mutant shows postembryonic seedling lethality associated with lack of membrane integrity
- auteur
- Ho Bang Kim, Hubert Schaller, Chang-Hyo Goh, Mi Kwon, Sunghwa Choe, Chung Sun An, Francis Durst, Kenneth A. Feldmann, René Feyereisen
- article
- Plant Physiology, 2005, 138 (4), pp.2033-2047. ⟨10.1104/pp.105.061598⟩
- Accès au bibtex
-
- titre
- Real-Time system verification techniques based on abstraction/deduction and model checking
- auteur
- Eunyoung Kang
- article
- Doctoral Symposium of the Fifth International Conference on Integrated Formal Methods - IFM'2005, Judi Romijn, Nov 2005, Eindhoven/The Netherlands
- Accès au texte intégral et bibtex
-
- titre
- Refinement and Reachability in Event_B
- auteur
- Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
- article
- ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users, Apr 2005, Guilford/UK, pp.222-241, ⟨10.1007/11415787_14⟩
- Accès au bibtex
-
- titre
- DIXIT: a Graphical Toolkit for Predicate Abstractions
- auteur
- Loïc Fejoz, Dominique Méry, Stephan Merz
- article
- Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48
- Accès au texte intégral et 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
- Accès au bibtex
-
- titre
- Predicate Diagrams for the Verification of Real-Time Systems
- auteur
- Eunyoung Kang, Stephan Merz
- article
- The Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS'05, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK
- Accès au texte intégral et 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
-
2004
- 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
-
- 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
- Accès au texte intégral et 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
- Accès au 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
-
- 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, Michael Backes, David Basin, and Michael Waidner, Oct 2004, Washington D.C./USA, pp.13-22, ⟨10.1145/1029133.1029136⟩
- Accès au texte intégral et 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
-
- titre
- Transformation des spécifications B en des diagrammes UML
- auteur
- Houda Fekih, Leila Jemni, Stephan Merz
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'2004, Université de Franche-Comté, 2004, Besançon, France, pp.131-145
- Accès au texte intégral et bibtex
-
- titre
- Refining Mobile UML State Machines
- auteur
- Alexander Knapp, Stephan Merz, Martin Wirsing
- article
- 10th International Conference on Algebraic Methodology and Software Technology - AMAST'2004, 2004, Stirling, Scotland, UK, pp.274--288
- Accès au 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
-
- 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", Club des Enseignants et des Chercheurs en Electronique, Electrotechnique et Automatique, Section Automatique, 2004, Cachan, France
- Accès au 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
-
- 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
-
- 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
-
- 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
-
- titre
- Tutorial on the event-based B method : Concepts and Case Studies
- auteur
- Dominique Cansell, Dominique Méry
- article
- Logics of Formal Software Specification Languages - LFSL'2004, 2004, The High Tatras, Slovakia
- Accès au bibtex
-
- titre
- Construction sûre de systèmes électroniques
- auteur
- Dominique Cansell, Stefan Hallerstede, Yann Zimmermann
- article
- Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2004, 69, pp.38-44
- Accès au 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
- Accès au bibtex
-
- titre
- Circuit Design by Refinement in EventB
- auteur
- Stefan Hallerstede, Yann Zimmermann
- article
- Forum on Specification and Design Languages - FDL'04, Pierre Boulet, 2004, Lille, France, 13 p
- Accès au bibtex
-
2003
- 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
- Accès au texte intégral et 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
- Accès au 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
-
- titre
- Formal derivation of spanning trees algorithms
- auteur
- Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
- article
- Third International Conference of B and Z Users - ZB'2003, Marina Walden, 2003, Turku, Finland, pp.457-476
- Accès au bibtex
-
- titre
- Modélisation des systèmes réactifs
- auteur
- Dominique Méry, Nidhal Rezg, Xiaolan Xie
- article
- 4ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2003, 2003, Metz, France, 568 p
- Accès au bibtex
-
- titre
- Click'n'Prove: Interactive Proofs Within Set Theory
- auteur
- Jean-Raymond Abrial, Dominique Cansell
- article
- 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, 2003, Rome, Italy, pp.1-24
- Accès au 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
- Accès au 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, 2003, 14 (3), pp.215-227
- Accès au bibtex
-
- titre
- Foundations of the B method
- auteur
- Dominique Cansell, Dominique Méry
- article
- Computing and Informatics, 2003, 22, 31 p
- Accès au bibtex
-
- 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
-
- titre
- On the Logic of TLA+
- auteur
- Stephan Merz
- article
- Computing and Informatics, 2003, 22 (4), 27 p
- Accès au bibtex
-
- titre
- Solving Layout Problems Concurrently With TeX and Java
- auteur
- Denis Roegel
- article
- Tugboat, 2003, 8 p
- Accès au texte intégral et 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
- Accès au bibtex
-
- titre
- A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems
- auteur
- Stephan Merz, Martin Wirsing, Julia Zappe
- article
- Fundamental Approaches to Software Engineering '03 - FASE 2003, Lecture Notes in Computer Sciences, 2003, Warsaw, Poland, pp.87-101
- Accès au 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. pp.93-101
- Accès au texte intégral et 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
- Accès au 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
- 4th International Conference on Formal Engineering Methods - ICFEM 2002, Oct 2002, Shanghai, China. pp.216-220, ⟨10.1007/3-540-36103-0_23⟩
- Accès au texte intégral et bibtex
-
- titre
- Higher-Order" Mathematics in B
- auteur
- Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte
- article
- 2nd International Conference of B and Z Users - ZB'2002, D. Bert, J.P. Bowen, M.C. Henson, K. Robinson, Jan 2002, Grenoble, France, pp.370-393
- Accès au 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 Péraud, 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 Atifi, Michel Marcoccia, Émilie Moreau, Michel Moatti, Lionel Dax
- article
- Université de Rennes 2, 486p., 2002
- Accès au texte intégral et 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
-
- 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
- 2nd International Conference of B and Z Users - ZB 2002, 2002, Grenoble, France, pp.22-41
- Accès au bibtex
-
- titre
- Integration of the proof process in the system development through refinement steps
- auteur
- Dominique Cansell, Dominique Méry
- article
- 5th Forum on Specification and Design Language - Workshop SFP in FDL'02, 2002, Marseille, France, 12 p
- Accès au bibtex
-
2001
- titre
- Développement Incrémental Prouvé de Systèmes
- auteur
- Airy Weinzoepflen
- article
- [Internship report] A01-R-315 || weinzoepflen01a, 2001, 51 p
- Accès au bibtex
-
- titre
- Specification and Design of the Leader Election Protocol of IEEE 1394
- auteur
- Jean-Raymond Abrial, Dominique Cansell, Dominique Méry
- article
- IEEE 1394 (FireWire) Workshop: International Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001, Berlin, Germany, 3 p
- Accès au 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, 16 p
- Accès au bibtex
-
- titre
- La géométrie dans l'espace avec METAPOST
- auteur
- Denis Roegel
- article
- Cahiers Gutenberg, 2001, 39-40, pp.107-138
- Accès au 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
-
- titre
- The METAOBJ tutorial and reference manual
- auteur
- Denis Roegel
- article
- 2001
- Accès au texte intégral et 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
- Accès au bibtex
-
- titre
- Anatomy of a macro
- auteur
- Denis Roegel
- article
- Tugboat, 2001, 22 (1-2), pp.78-82
- Accès au bibtex
-
- titre
- Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Integrating Diagrammatic and Formal Specification Techniques, GI Fachgruppe 0.1.7 Specification and Semantics, 2001, Wien, Austria, pp.39-45
- Accès au bibtex
-
- titre
- METAPOST, l'intelligence graphique
- auteur
- Denis Roegel
- article
- Cahiers Gutenberg, 2001, 41, pp.5-16
- Accès au bibtex
-
- titre
- Space geometry with MetaPost
- auteur
- Denis Roegel
- article
- Tugboat, 2001, 22 (4), pp.298-314
- Accès au bibtex
-
2000
- titre
- Predicate diagrams for the verification of reactive systems
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, pp.380-397
- Accès au bibtex
-
- titre
- Predicate diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Workshop on Requirement, Design, Correct Construction & Verification, M.V. Cengarle, 2000, Munich, Germany
- Accès au 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
- International Conference on B & Z Users - ZB'2000, 2000, York, GB, pp.148-167
- Accès au 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
-
- 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
-
- 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
-
- titre
- Diagrams Refinement for the Design of Reactive Systems
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Journal of Universal Computer Science, 2000, 7 (2), pp.159-174
- Accès au bibtex
-
- titre
- Parallel Molecular Dynamics Using OpenMP on a Shared Memory Machine
- auteur
- Raphael Couturier, Christophe Chipot
- article
- Computer Physics Communications, 2000, 124 (1), pp.49-59
- Accès au 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
-
- titre
- Abstraction and Refinement of Concurrent Programs and Formal Specification
- auteur
- Dominique Cansell, Dominique Méry, Christophe Tabacznyj
- article
- Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, Dominique Méry & Beverly Sanders, 2000, Cancun, Mexico, pp.1037-1038
- Accès au bibtex
-
- titre
- A taxonomy for triggered interactions using fair object semantics
- auteur
- Paul Gibson, Geoff Hamilton, Dominique Méry
- article
- Feature Interactions in Telecommunications & Software Systems VI, 2000, Glasgow, UK, 20 p
- Accès au 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
-
- titre
- Verifying Reactive Systems Using Predicate Diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- FM-TOOLS'2000, Wolfgang Reif & Gerhard Schellhorn, 2000, Ulm, 5 p
- Accès au bibtex
-
1999
- 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
- Accès au 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, pp.139--145
- Accès au texte intégral et 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
- Andrei Ershov Third International Conference, Perspectives of system Informatics - PSI'99, 1999, Novosibirsk, Russia, pp.155-179
- Accès au bibtex
-
- titre
- Abstract animator for temporal specifications Application to TLA
- auteur
- Dominique Cansell, Dominique Méry
- article
- International Symposium on Static Analysis - SAS'99, Gilberto Fil{é} & Agostino Cortesi, 1999, Venise, Italie, pp.284-299
- Accès au bibtex
-
- titre
- Lazy Caching in TLA
- auteur
- Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
- article
- Distributed Computing, 1999, 12 (2-3), pp.151-174
- Accès au bibtex
-
- 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, 1999, 19 (5), pp.625-648
- Accès au bibtex
-
- titre
- Special Issue FMPPTA'98
- auteur
- Dominique Méry
- article
- World Scientific, 1999, Parallel Processing Letters
- Accès au 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
- Accès au texte intégral et bibtex
-
- titre
- Integration Problems in Telephone Feature requirements
- auteur
- John Paul Gibson, Geoff Hamilton, Dominique Méry
- article
- Workshop on Integrated Formal Methods - IFM'99, 1999, York, England, 19 p
- Accès au 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
- Integrated Formal Methods - IFM'99, A. Galloway, 1999, York, UK, 20 p
- Accès au bibtex
-
- titre
- Validation of formal specifications
- auteur
- Dominique Méry, Yassine Mokhtari
- article
- AAAI'99, Fall Symposium, Nov 1999, none, 5 p
- Accès au texte intégral et 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, 8 p
- Accès au bibtex
-
- titre
- Edition Spéciale RenPar'10
- auteur
- Dominique Méry, Guy-René Perrin
- article
- Hermès, 1999, TSI
- Accès au bibtex
-
- titre
- Animating TLA Specifications
- auteur
- Yassine Mokhtari, Stephan Merz
- article
- International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, pp.92--110
- Accès au bibtex
-
- titre
- Abstract Animator for Temporal Specifications
- auteur
- Dominique Cansell, Dominique Méry
- article
- Workshop on Modelling & Verification, Françoise Bellegarde, Olga Kouchnarenko & Jacques Julliand, 1999, Besançon, France
- Accès au bibtex
-
1998
- 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, 6 p
- Accès au 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
-
- 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
- Accès au bibtex
-
- titre
- Anatomie d'une macro
- auteur
- Denis Roegel
- article
- Cahiers Gutenberg, 1998, 31, pp.19-27
- Accès au 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
- Accès au 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
-
- titre
- The invoice system problem in TLA+
- auteur
- Yassine Mokhtari
- article
- International Workshop on Specification Techniques & Formal Methods, Habrias, Henri, 1998, Nantes, France, 16 p
- Accès au bibtex
-
- titre
- An experiment in parallelizing an application using formal methods
- auteur
- Raphaël Couturier, Dominique Méry
- article
- International Conference on Computer Aided Verification - CAV'98, 1998, Vancouver, Canada, 10 p
- Accès au bibtex
-
- titre
- Parallélisation d'une simulation Monte Carlo d'un système de spins et preuve
- auteur
- Raphaël Couturier
- article
- Renpar'10, 1998, Strasbourg, France, 4 p
- Accès au 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
- The 2nd International B Conference, 1998, Montpellier, France. pp.198-209
- Accès au bibtex
-
- titre
- RenPar'10
- auteur
- Guy-René Perrin, Dominique Méry
- article
- ULP, 264 p, 1998
- Accès au 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
-
- titre
- Always and Eventually in Object Requirements
- auteur
- Jean-Paul Gibson, Dominique Méry
- article
- Rigorous Object Oriented Methods, 1998, none, 20 p
- Accès au bibtex
-
- titre
- Formal engineering of the bitonic sort using pvs
- auteur
- Raphaël Couturier
- article
- 2nd Irish Workshop in Formal Methods - IWFM'98, 1998, Cork, irlande, 16 p
- Accès au 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, 8 p
- Accès au bibtex
-
- titre
- Parallelization of a Monte Carlo simulation of a spins system
- auteur
- Raphaël Couturier, Dominique Méry
- article
- Parallel and Distributed Processing Techniques and Applications - PDPTA'98, 1998, Las Vegas, USA, 5 p
- Accès au bibtex
-
- 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, 1998, 17 (9), pp.1157-1180
- Accès au 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
- Accès au bibtex
-