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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
-
- 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
-
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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- Special Issue
- auteur
- Matthew England, Wolfram Koepf, Timur M. Sadykov, Werner Seiler, Thomas Sturm
- article
- Aug 2019, Moscow, Russia. Mathematics in Computer Science, Springer, 2021
- Accès au 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- É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
- 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
- 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
- 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
- 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 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
- 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
- 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 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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, 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
- 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
- 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
- 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
- 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
- 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
- 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 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
-
2015
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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 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
- 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
- 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
- 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 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- Stuttering Equivalence
- auteur
- Stephan Merz
- article
- [Research Report] 2012
- 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
- 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
- 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
-
2011
- 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
-