2025
Journal articles
- auteur
- Rosalie Defourné
- titre
- Encoding TLA+ proof obligations safely for SMT
- article
- Science of Computer Programming, 2025, Selected Papers From the Rigorous State-Based Methods 9th International Conference( ABZ 2023), 239 (103178), ⟨10.1016/J.SCICO.2024.103178⟩
- Accès au texte intégral et bibtex
-
2024
Journal articles
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
- titre
- Fully Abstract Encodings of Lambda-Calculus in HOcore through Abstract Machines
- article
- Logical Methods in Computer Science, 2024, Volume 20, Issue 3, ⟨10.46298/lmcs-20(3:3)2024⟩
- Accès au bibtex
-
- auteur
- Aurélien Desoeuvres, Alexandru Iosif, Christoph Lüders, Ovidiu Radulescu, Hamid Rahkooy, Matthias Seiß, Thomas Sturm
- titre
- A Computational Approach to Polynomial Conservation Laws
- article
- SIAM Journal on Applied Dynamical Systems, 2024, 23 (1), pp.813-854. ⟨10.1137/22M1544014⟩
- Accès au bibtex
-
- auteur
- Bineet Ghosh, Étienne André
- titre
- Offline and online energy-efficient monitoring of scattered uncertain logs using a bounding model
- article
- Logical Methods in Computer Science, 2024, Volume 20, Issue 1, ⟨10.46298/lmcs-20(1:2)2024⟩
- Accès au bibtex
-
- auteur
- Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell
- titre
- Porous invariants for linear systems
- article
- Formal Methods in System Design, 2024, 63 (1-3), pp.235-271. ⟨10.1007/s10703-024-00444-3⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Raschke, Dominique Méry
- titre
- An automotive case study
- article
- International Journal on Software Tools for Technology Transfer, 2024, 26 (3), pp.327-330. ⟨10.1007/s10009-024-00753-2⟩
- Accès au bibtex
-
Conference papers
- auteur
- Étienne André, Sarah Dépernet, Engel Lefaucheux
- titre
- The Bright Side of Timed Opacity (extended version)
- article
- ICFEM 2024, Dec 2024, Hiroshima, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Étienne André, Marie Duflot, Laetitia Laversa, Engel Lefaucheux
- titre
- Execution-time opacity control for timed automata ⋆
- article
- SEFM 2024, Nov 2024, Aveiro (Portugal), Portugal
- Accès au texte intégral et bibtex
-
- auteur
- Étienne André, Johan Arcile, Engel Lefaucheux
- titre
- Execution-time opacity problems in one-clock parametric timed automata
- article
- FSTTCS 2024, Dec 2024, Gandhinagar, India
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Bagrel
- titre
- Destination-passing style programming: a Haskell implementation
- 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
-
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt
- titre
- Optimizing a Non-Deterministic Abstract Machine with Environments
- article
- FSCD 2024 – 9th International Conference on Formal Structures for Computation and Deduction, Jul 2024, Tallinn, Estonia. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2024.11⟩
- Accès au texte intégral et bibtex
-
- auteur
- Horatiu Cirstea, Markus A Kuppe, Benjamin Loillier, Stephan Merz
- titre
- Validating Traces of Distributed Programs Against TLA+ Specifications
- article
- Software Engineering and Formal Methods, Nov 2024, Aveiro, Portugal. pp.126-143
- Accès au texte intégral et bibtex
-
- auteur
- Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret
- titre
- A Modular Formalization of Superposition in Isabelle/HOL
- article
- 15th International Conference on Interactive Theorem Proving, Sep 2024, Tbilisi, Georgia. ⟨10.4230/LIPIcs.ITP.2024.12⟩
- Accès au texte intégral et bibtex
-
- auteur
- Isabela Drămnesc, Tudor Jebelean, Sorin Stratulat
- titre
- Certification of Sorting Algorithms Using Theorema and Coq
- article
- SCSS 2024 (Symbolic Computation in Software Science), Aug 2024, Tokyo (Japan), Japan. pp.38–56, ⟨10.1007/978-3-031-69042-6_3⟩
- Accès au texte intégral et bibtex
-
- auteur
- Isabela Drȃmnesc, Erika Ábrahám, Tudor Jebelean, Nikolaos Fachantidis, Gábor Kusper, Sorin Stratulat
- titre
- A European Project on AI-based Robotics
- article
- TALE2024 (International Conference on Teaching, Assessment and Learning for Engineering), Dec 2024, Bengalore, India
- Accès au texte intégral et bibtex
-
- auteur
- Marie Duflot, Engel Lefaucheux, Isaline Plaid
- titre
- Diagnosis of Stochastic Systems: Optimising Costs and Delays
- article
- QEST-FORMATS 2024, Sep 2024, Calgary, Alberta, Canada, Canada
- Accès au texte intégral et bibtex
-
- auteur
- Nicolas Faroß, Simon Schwarz
- titre
- Gröbner Bases for Boolean Function Minimization
- article
- Proceedings of the 8th SC-Square Workshop, Jul 2024, Tromsø, Norway
- Accès au texte intégral et bibtex
-
- auteur
- Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, James Worrell
- titre
- The 2-Dimensional Constraint Loop Problem Is Decidable
- article
- 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), Tallinn University of Technology, Jul 2024, Tallin, Estonia. pp.21, ⟨10.4230/LIPIcs.ICALP.2024.140⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sergueï Lenglet, Alan Schmitt
- titre
- Leaf-First Zipper Semantics
- article
- FORTE 2024 – 44th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Jun 2024, Groningen, Netherlands. ⟨10.1007/978-3-031-62645-6_7⟩
- Accès au texte intégral et bibtex
-
- auteur
- Dominique Méry
- titre
- Checking Contracts in Event-B
- article
- Formal Methods Teaching – 6th Formal Methods Teaching Workshop, FMTea 2024, Emil Sekerinski; Leila Ribeiro, Sep 2024, MILAN, France. pp.91-105, ⟨10.1007/978-3-031-71379-8_6⟩
- Accès au bibtex
-
- auteur
- Sophie Tourret
- titre
- Invited Talk: The Hows and Whys of Higher-Order SMT
- article
- 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Giles Reger and Yoni Zohar, Jul 2024, Montréal, Canada
- Accès au bibtex
-
- auteur
- Hao Wu, Thomas Flinkow, Dominique Méry
- titre
- Cyclone: A New Tool for Verifying/Testing Graph-Based Structures
- article
- Tests and Proofs – 18th International Conference, {TAP} 2024, Marieke Huisman; Falk Howar, Sep 2024, MILAN, Italy. pp.107-124
- Accès au bibtex
-
Preprints, Working Papers, …
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt
- titre
- Optimizing a Non-Deterministic Abstract Machine with Environments
- article
- 2024
- Accès au texte intégral et bibtex
-
- auteur
- Horatiu Cirstea, Markus A Kuppe, Benjamin Loillier, Stephan Merz
- titre
- Validating Traces of Distributed Programs Against TLA+ Specifications
- article
- 2024
- Accès au texte intégral et bibtex
-
- auteur
- Engel Lefaucheux
- titre
- When are two Parametric Semi-linear Sets Equal?
- article
- 2024
- Accès au texte intégral et bibtex
-
- auteur
- Sergueï Lenglet, Alan Schmitt
- titre
- Leaf-First Zipper Semantics
- article
- 2024
- Accès au texte intégral et bibtex
-
2023
Journal articles
- auteur
- Étienne André, Engel Lefaucheux, Didier Lime, Dylan Marinho, Jun Sun
- titre
- Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
- 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
-
- auteur
- Étienne André, Shuang Liu, Yang Liu, Christine Choppy, Jun Sun, Jin Song Dong
- titre
- Formalizing UML State Machines for Automated Verification – A Survey
- article
- ACM Computing Surveys, 2023, 55 (13s), pp.1-47. ⟨10.1145/3579821⟩
- Accès au bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann
- titre
- Complete and Efficient Higher-Order Reasoning via Lambda-Superposition
- article
- ACM SIGLOG News, 2023, 10 (4), pp.25-40. ⟨10.1145/3636362.3636367⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- titre
- Mechanical Mathematicians
- article
- Communications of the ACM, 2023, 66 (4), pp.80-90. ⟨10.1145/3557998⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović
- titre
- Superposition for Higher-Order Logic
- article
- Journal of Automated Reasoning, 2023, 67 (1), pp.10. ⟨10.1007/s10817-022-09649-9⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Blanchette, Petar Vukmirović
- titre
- SAT-Inspired Higher-Order Eliminations
- article
- Logical Methods in Computer Science, 2023, 19 (2), ⟨10.48550/arXiv.2208.07775⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
- titre
- Unifying Splitting
- article
- Journal of Automated Reasoning, 2023, 67 (2), pp.16. ⟨10.1007/s10817-023-09660-8⟩
- Accès au texte intégral et bibtex
-
- auteur
- Bineet Ghosh, Étienne André
- titre
- MoULDyS: Monitoring of autonomous systems in the presence of uncertainties
- article
- Science of Computer Programming, 2023, 230, pp.102976. ⟨10.1016/j.scico.2023.102976⟩
- Accès au bibtex
-
- auteur
- Vineeta Jain, Ulf Wetzker, Vijay Laxmi, Manoj Singh Gaur, Mohamed Mosbah, Dominique Méry
- titre
- SAP: A Secure Low-Latency Protocol for Mitigating High Computation Overhead in WI-FI Networks
- article
- IEEE Access, 2023, 11, pp.84620-84635. ⟨10.1109/ACCESS.2023.3302529⟩
- Accès au bibtex
-
- auteur
- Hendrik Leidinger, Christoph Weidenbach
- titre
- SCL(EQ): SCL for First-Order Logic with Equality
- article
- Journal of Automated Reasoning, 2023, 67 (3), pp.22. ⟨10.1007/s10817-023-09673-3⟩
- Accès au texte intégral et bibtex
-
- auteur
- Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Guillaume Dupont, Dominique Méry, Philippe Palanque
- titre
- Formal domain-driven system development in Event-B: Application to interactive critical systems
- article
- Journal of Systems Architecture, 2023, 135, pp.102798. ⟨10.1016/j.sysarc.2022.102798⟩
- Accès au bibtex
-
- auteur
- Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
- titre
- Synchronization modulo P in dynamic networks
- article
- Theoretical Computer Science, 2023, 942, pp.200-212. ⟨10.1016/J.TCS.2022.11.033⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sorin Stratulat
- titre
- Mechanical certification of FOLID cyclic proofs
- 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
-
- auteur
- Petar Vukmirović, Jasmin Blanchette, Marijn J H Heule
- titre
- SAT-Inspired Eliminations for Superposition
- article
- ACM Transactions on Computational Logic, 2023, 24 (1), pp.1-25. ⟨10.1145/3565366⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Étienne André, Engel Lefaucheux, Dylan Marinho
- titre
- Expiring opacity problems in parametric timed automata
- article
- 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS), Jun 2023, Toulouse, France. pp.89-98, ⟨10.1109/ICECCS59891.2023.00020⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Blanchette, Qi Qiu, Sophie Tourret
- titre
- Verified Given Clause Procedures
- 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
-
- auteur
- Yasmine Briefs, Hendrik Leidinger, Christoph Weidenbach
- titre
- KBO Constraint Solving Revisited
- 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
-
- auteur
- Martin Bromberger, Chaahat Jain, Christoph Weidenbach
- titre
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- 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
-
- auteur
- Martin Bromberger, Simon Schwarz, Christoph Weidenbach
- titre
- Exploring Partial Models with SCL
- 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
-
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- titre
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- 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
-
- auteur
- Horatiu Cirstea, Stephan Merz
- titre
- Extending PlusCal for Modeling Distributed Algorithms
- 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
-
- auteur
- Mathieu D’aquin, Renata Bunoiu, Horatiu Cirstea, Michel Lenczner, Jean Lieber, Frédéric Zamkotsian
- titre
- Combining representation formalisms for reasoning upon mathematical knowledge
- 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
-
- auteur
- Rosalie Defourné
- titre
- Encoding TLA$^{+}$ Proof Obligations Safely for SMT
- 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
-
- auteur
- Martin Dvorak, Jasmin Blanchette
- titre
- Closure Properties of General Grammars – Formally Verified
- article
- ITP 2023, 2023, Białystok, Poland. ⟨10.4230/LIPIcs.ITP.2023.15⟩
- Accès au texte intégral et bibtex
-
- auteur
- Aman Goel, Stephan Merz, Karem A. Sakallah
- titre
- Towards an Automatic Proof of the Bakery Algorithm
- article
- 43th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal. pp.21-28, ⟨10.1007/978-3-031-35355-0_2⟩
- Accès au texte intégral et bibtex
-
- auteur
- Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi
- titre
- Model Checking Linear Dynamical Systems under Floating-point Rounding
- 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
-
- auteur
- Sibylle Möhle
- titre
- An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
- 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
-
- auteur
- Visa Nummelin, Jasmin Blanchette, Sander Dahmen
- titre
- Recurrence-Driven Summations in Automated Deduction
- 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
-
- auteur
- Andreas Plank, Sibylle Möhle, Martina Seidl
- titre
- Enumerative Level-2 Solution Counting for Quantified Boolean Formulas
- 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
-
- auteur
- Petar Vukmirović, Jasmin Blanchette, Stephan Schulz
- titre
- Extending a High-Performance Prover to Higher-Order Logic
- 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
-
Special issue
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- titre
- Computer Algebra in Scientific Computing 2022
- article
- Mathematics in Computer Science, 17 (3-4), 2023
- Accès au bibtex
-
Other publications
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- titre
- Foreword. Special issue on CASC 2022
- article
- 2023, pp.22. ⟨10.1007/s11786-023-00565-8⟩
- Accès au bibtex
-
Proceedings
- auteur
- Erika Ábrahám, Thomas Sturm
- titre
- Satisfiability Checking and Symbolic Computation 2023
- article
- CEUR Workshop Proceedings, 3455, 2023
- Accès au bibtex
-
- auteur
- Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque
- titre
- Rigorous State-Based Methods – 9th International Conference, ABZ 2023, Nancy, France, May 30 – June 2, 2023, Proceedings
- 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
-
Reports
- auteur
- Martin Bromberger, Chaahat Jain, Christoph Weidenbach
- titre
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
- auteur
- Martin Bromberger, Simon Schwarz, Christoph Weidenbach
- titre
- SCL(FOL) Revisited
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- titre
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- article
- Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Rosalie Defourné
- titre
- Encoding TLA+’s Set Theory for Automated Theorem Provers
- article
- Computer Science [cs]. Université de Lorraine, 2023. English. ⟨NNT : 2023LORR0263⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Zheng Cheng, Dominique Méry
- titre
- A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions
- article
- 2023
- Accès au texte intégral et bibtex
-
- auteur
- Zheng Cheng, Dominique Méry
- titre
- From System Events to Software Operations for Refinement-based Modeling of Hybrid Systems *
- article
- 2023
- Accès au texte intégral et bibtex
-
2022
Journal articles
- auteur
- Étienne André, Didier Lime, Olivier Henri Roux
- titre
- Reachability and liveness in parametric timed automata
- article
- Logical Methods in Computer Science, 2022, 18 (1), ⟨10.46298/lmcs-18(1:31)2022⟩
- Accès au bibtex
-
- auteur
- Étienne André, Didier Lime, Dylan Marinho, Jun Sun
- titre
- Guaranteeing Timed Opacity using Parametric Timed Model Checking
- article
- ACM Transactions on Software Engineering and Methodology, 2022, 31 (4), pp.1-36. ⟨10.1145/3502851⟩
- Accès au texte intégral et bibtex
-
- auteur
- Johan Arcile,, Étienne André
- titre
- Timed automata as a formalism for expressing security: A survey on theory and practice
- article
- ACM Computing Surveys, 2022, ⟨10.1145/3534967⟩
- Accès au bibtex
-
- auteur
- Ladjel Bellatreche, Carlos Ordonez, Dominique Méry, Matteo Golfarelli, El Hassan Abdelwahed
- titre
- The central role of data repositories and data models in Data Science and Advanced Analytics
- article
- Future Generation Computer Systems, 2022, 129, pp.13-17. ⟨10.1016/j.future.2021.11.027⟩
- Accès au bibtex
-
- auteur
- Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, Benjamin Monmege
- titre
- One-Clock Priced Timed Games with Arbitrary Weights
- article
- Logical Methods in Computer Science, 2022, 18 (3), pp.51
- Accès au texte intégral et bibtex
-
- auteur
- Isabela Drămnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
- titre
- Automated Reasoning in the Class
- article
- Computer-Algebra-Rundbrief, 2022, 71, pp.21-26
- Accès au texte intégral et bibtex
-
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- titre
- Foreword
- article
- Mathematics in Computer Science, 2022, 16 (2-3), pp.16. ⟨10.1007/s11786-022-00533-8⟩
- Accès au bibtex
-
- auteur
- Leslie Lamport, Stephan Merz
- titre
- Prophecy Made Simple
- 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
-
- auteur
- Christoph Lüders, Thomas Sturm, Ovidiu Radulescu
- titre
- ODEbase: A Repository of ODE Systems for Systems Biology
- article
- Bioinformatics Advances, 2022, 2 (1), ⟨10.1093/bioadv/vbac027⟩
- Accès au bibtex
-
- auteur
- Dominique Méry, Alexander Raschke
- titre
- Selected papers from the Rigorous State-Based Methods 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020
- article
- Science of Computer Programming, 2022, 216, pp.102780. ⟨10.1016/j.scico.2022.102780⟩
- Accès au bibtex
-
- auteur
- Dominique Méry, Shengchao Qin
- titre
- Selected papers from The 13th International Symposium on Theoretical Aspects of Software Engineering 29 July – 1 August 2019, Guilin, China
- article
- Science of Computer Programming, 2022, 218, pp.102804. ⟨10.1016/j.scico.2022.102804⟩
- Accès au bibtex
-
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- titre
- Polite Combination of Algebraic Datatypes
- article
- Journal of Automated Reasoning, 2022, 66 (3), pp.331-355. ⟨10.1007/s10817-022-09625-3⟩
- Accès au bibtex
-
- auteur
- Sorin Stratulat
- titre
- Récurrence noethérienne pour le raisonnement de premier ordre
- 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
-
- auteur
- Sophie Tourret, Christoph Weidenbach
- titre
- A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column
- article
- Journal of Automated Reasoning, 2022, 66 (4), pp.575-584. ⟨10.1007/s10817-022-09617-3⟩
- Accès au bibtex
-
- auteur
- Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
- titre
- Making Higher-Order Superposition Work
- 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
-
- auteur
- Petar Vukmirović, Jasmin Blanchette, Simon Cruanes, Stephan Schulz
- titre
- Extending a brainiac prover to lambda-free higher-order logic
- 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
-
- auteur
- Masaki Waga, Étienne André, Ichiro Hasuo
- titre
- Model-bounded Monitoring of Hybrid Systems
- article
- ACM Transactions on Cyber-Physical Systems, 2022, 6 (4), pp.1-26. ⟨10.1145/3529095⟩
- Accès au bibtex
-
- auteur
- Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
- titre
- A Comprehensive Framework for Saturation Theorem Proving
- 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
-
Conference papers
- auteur
- Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille Noûs
- titre
- Certified Derivation of Small-Step From Big-Step Skeletal Semantics
- 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
-
- auteur
- Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
- titre
- Certified Abstract Machines for Skeletal Semantics
- 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
-
- auteur
- Étienne André, Shapagat Bolat, Engel Lefaucheux, Dylan Marinho
- titre
- strategFTO: Untimed control for timed opacity
- 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 texte intégral et bibtex
-
- auteur
- Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol
- titre
- Efficient Convex Zone Merging in Parametric Timed Automata
- 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
-
- auteur
- Étienne André, Masaki Waga, Natuski Urabe, Ichiro Hasuo
- titre
- Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior
- 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
-
- auteur
- Johan Arcile,, Étienne André
- titre
- Zone Extrapolations in Parametric Timed Automata
- 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
-
- auteur
- Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joel Ouaknine, David Purser, Markus A. Whiteland, James Worrell
- titre
- Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
- 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
-
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt
- titre
- Non-Deterministic Abstract Machines
- 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
-
- auteur
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
- titre
- An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
- 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
-
- auteur
- Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish Murali, Christoph Weidenbach
- titre
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- 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
-
- auteur
- Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, David Purser, Markus A Whiteland
- titre
- The boundedness and zero isolation problems for weighted automata over nonnegative rationals
- 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
-
- auteur
- Julian d’Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell
- titre
- Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set
- 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
-
- auteur
- Alexander Demin, Hamid Rahkooy, Thomas Sturm
- titre
- F5: A REDUCE Package for Signature-based Gröbner Basis Computation
- article
- CASC 2022 – Computer Algebra in Scientific Computing, Aug 2022, Gezbe, Turkey
- Accès au texte intégral et bibtex
-
- auteur
- Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, Makarius Wenzel
- titre
- Seventeen Provers under the Hammer
- 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
-
- auteur
- Isabela Drămnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
- titre
- Experiments with Automated Reasoning in the Class
- 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
-
- auteur
- Isabela Drămnesc, Tudor Jebelean, Erika Ábrahám, Gábor Kusper, Sorin Stratulat
- titre
- ARC: An Educational Project on Automated Reasoning in the Class
- article
- EdMedia + Innovate Learning 2022 – AACE Conferences, Jun 2022, New York, United States
- Accès au texte intégral et bibtex
-
- auteur
- Bineet Ghosh, Étienne André
- titre
- Offline and Online Monitoring of Scattered Uncertain Logs Using Uncertain Linear Dynamical Systems
- 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
-
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- titre
- Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract)
- article
- 35th International Workshop on Description Logics (DL 2022), Aug 2022, Haifa, Israel
- Accès au texte intégral et bibtex
-
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- titre
- Connection-Minimal Abduction in EL via Translation to FOL
- 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
-
- auteur
- Fajar Haifani, Christoph Weidenbach
- titre
- Semantic Relevance
- 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
-
- auteur
- Toghrul Karimov, Engel Lefaucheux, Joel Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell
- titre
- What’s decidable about linear loops?
- 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
-
- auteur
- Igor Konnov, Markus Kuppe, Stephan Merz
- titre
- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
- 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
-
- auteur
- Hendrik Leidinger, Christoph Weidenbach
- titre
- SCL(EQ): SCL for First-Order Logic with Equality
- 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
-
- auteur
- Ismail Mendil, Peter Riviere, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- titre
- Non-Intrusive Annotation-Based Domain-Specific Analysis to Certify Event-B Models Behaviours
- article
- 29th Asia-Pacific Software Engineering Conference (APSEC 2022), Dec 2022, Virtual conference, Japan. pp.129-138, ⟨10.1109/APSEC57359.2022.00025⟩
- Accès au texte intégral et bibtex
-
Book sections
- auteur
- Yamine Aït-Ameur, Ismail Mendil, Guillaume Dupont, Dominique Méry, Marc Pantel, Peter Riviere, Neeraj Kumar Singh
- titre
- Empowering the Event-B Method Using External Theories
- 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
-
Reports
- auteur
- Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt
- titre
- Non-Deterministic Abstract Machines
- article
- [Research Report] RR-9475, Inria. 2022, pp.1-33
- Accès au texte intégral et bibtex
-
- auteur
- Margarida Romero, Thierry Viéville, Marie Duflot-Kremer
- titre
- Activity for learning computational thinking in plugged and unplugged mode
- article
- [Research Report] 006, UCA – INSPE Académie de Nice. 2022
- Accès au texte intégral et bibtex
-
Software
- auteur
- Tony Ribeiro, Maxime Folschette, Morgan Magnin, Katsumi Inoue, Chiaki Sakama, Olivier Roux, Sophie Tourret, Madeleine Eyraud
- titre
- pylfit
- 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
-
Theses
- auteur
- Pierre Lermusiaux
- titre
- Static analysis of pattern eliminating transformations
- article
- Langage de programmation [cs.PL]. Université de Lorraine, 2022. Français. ⟨NNT : 2022LORR0372⟩
- Accès au texte intégral et bibtex
-
- auteur
- Hans-Jörg Schurr
- titre
- Stronger SMT Solvers for Proof Assistants : Proofs, Quantifier Simplification, Strategy Schedules
- article
- Logic in Computer Science [cs.LO]. Université de Lorraine, 2022. English. ⟨NNT : 2022LORR0135⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Aurélien Desoeuvres, Alexandru Iosif, Christoph Lüders, Ovidiu Radulescu, Hamid Rahkooy, Matthias Seiß, Thomas Sturm
- titre
- A Computational Approach to Complete Exact and Approximate Conservation Laws of Chemical Reaction Networks
- article
- 2022
- Accès au bibtex
-
- auteur
- Aurélien Desoeuvres, Alexandru Iosif, Christoph Lüders, Ovidiu Radulescu, Hamid Rahkooy, Matthias Seiß, Thomas Sturm
- titre
- Reduction of Chemical Reaction Networks with Approximate Conservation Laws
- article
- 2022
- Accès au bibtex
-
2021
Journal articles
- auteur
- Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, David Lesens
- titre
- Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints
- article
- Fundamenta Informaticae, 2021, 182 (1), pp.31-67. ⟨10.3233/FI-2021-2065⟩
- Accès au bibtex
-
- auteur
- Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga
- titre
- Parametric Analyses of Attack-fault Trees
- article
- Fundamenta Informaticae, 2021, 182 (1), pp.69 – 94. ⟨10.3233/fi-2021-2066⟩
- Accès au texte intégral et bibtex
-
- auteur
- Étienne André, Didier Lime, Mathias Ramparison
- titre
- Parametric updates in parametric timed automata
- article
- Logical Methods in Computer Science, 2021, 17 (2), pp.13:1-13:67. ⟨10.23638/LMCS-17(2:13)2021⟩
- Accès au texte intégral et bibtex
-
- auteur
- Étienne André, Hoang Gia Nguyen, Laure Petrucci, Jun Sun
- titre
- Distributed parametric model checking timed automata under non-Zenoness assumption
- article
- Formal Methods in System Design, 2021, 59 (1-3), pp.253-290. ⟨10.1007/s10703-022-00400-z⟩
- Accès au bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
- titre
- Superposition for Lambda-Free Higher-Order Logic
- article
- Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:1)2021⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- titre
- Superposition with Lambdas
- 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
-
- auteur
- Matthew England, Wolfram Koepf, Timur Sadykov, Werner M Seiler, Thomas Sturm
- titre
- Foreword, with a Dedication to Andreas Weber
- 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
-
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- titre
- Foreword, with a Dedication to Vladimir Gerdt
- 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
-
- auteur
- Dima Grigoriev, Alexandru Iosif, Hamid Rahkooy, Thomas Sturm, Andreas Weber
- titre
- Efficiently and Effectively Recognizing Toricity of Steady State Varieties
- 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
-
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- titre
- An Approximation of Minimax Control using Random Sampling and Symbolic Computation
- 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
-
- auteur
- Niclas Kruff, Christoph Lüders, Ovidiu Radulescu, Thomas Sturm, Sebastian Walcher
- titre
- Algorithmic Reduction of Biological Networks with Multiple Time Scales
- 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
-
- auteur
- Werner M Seiler, Matthias Seiss, Thomas Sturm
- titre
- A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations
- 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
-
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Romain Geniet, Dominique Méry, Philippe Palanque
- titre
- On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications
- article
- Interacting with Computers, 2021, ⟨10.1093/iwcomp/iwab016⟩
- Accès au bibtex
-
- auteur
- Marco Voigt
- titre
- Decidable $\exists$*$\forall$* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates
- article
- Journal of Automated Reasoning, 2021, 65 (3), pp.357-423. ⟨10.1007/s10817-020-09567-8⟩
- Accès au bibtex
-
Conference papers
- auteur
- Étienne André, Dylan Marinho, Jaco van de Pol
- titre
- A Benchmarks Library for Extended Parametric Timed Automata
- 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
-
- auteur
- Étienne André
- titre
- IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability
- 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
-
- auteur
- Étienne André, Aleksander Kryukov
- titre
- Parametric non-interference in timed automata
- 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
-
- auteur
- Étienne André, Jaime Arias, Laure Petrucci, Jaco van De Pol
- titre
- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
- 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
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović
- titre
- Superposition for Full Higher-order Logic
- 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
-
- auteur
- Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
- titre
- A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- 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
-
- auteur
- Martin Bromberger, Alberto Fiori, Christoph Weidenbach
- titre
- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
- 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
-
- auteur
- Zheng Cheng, Dominique Méry
- titre
- A Refinement Strategy for Hybrid System Design with Safety Constraints
- 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
-
- auteur
- Horatiu Cirstea, Pierre Lermusiaux, Pierre-Etienne Moreau
- titre
- Static analysis of pattern-free properties
- 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
-
- auteur
- Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
- titre
- Synchronization Modulo k in Dynamic Networks
- 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
-
- auteur
- Antoine Defourné
- titre
- Improving Automation for Higher-Order Proof Steps
- 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
-
- auteur
- Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
- titre
- A Unifying Splitting Framework
- 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
-
- auteur
- Rasha Faqeh, Christof Fetzer, Holger Herrmanns, Jörg Hoffmann, Michaela Klauck, Maximilian Koehl, Marcel Steinmetz, Christoph Weidenbach
- titre
- Towards Dynamic Dependable Systems through Evidence-Based Continuous Certification
- 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
-
- auteur
- Pascal Fontaine, Hans-Jörg Schurr
- titre
- Quantifier Simplification by Unification in SMT
- 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
-
- auteur
- Fajar Haifani, Sophie Tourret, Christoph Weidenbach
- titre
- Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
- 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
-
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret
- titre
- Abduction inELvia Translation to FOL
- 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
-
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- titre
- Robust optimal periodic control using guaranteed Euler’s method
- 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
-
- auteur
- Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque
- titre
- Standard Conformance-by-Construction with Event-B
- 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
-
- auteur
- Dominique Méry
- titre
- Refinement-based Construction of Correct Distributed Algorithms
- article
- ICI2ST 2021 – 2nd International Conference on Information Systems and Software Technologies, Mar 2021, Quito / Virtual, Ecuador. ⟨10.1109/ICI2ST51859.2021.00015⟩
- Accès au texte intégral et bibtex
-
- auteur
- Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirović
- titre
- Superposition with First-class Booleans and Inprocessing Clausification
- 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
-
- auteur
- Hamid Rahkooy, Thomas Sturm
- titre
- Parametric Toricity of Steady State Varieties of Reaction Networks
- 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
-
- auteur
- Hamid Rahkooy, Thomas Sturm
- titre
- Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems
- 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
-
- auteur
- Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
- titre
- Alethe: Towards a Generic SMT Proof Format (extended abstract)
- 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
-
- auteur
- Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
- titre
- Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
- 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
-
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- titre
- Politeness for the Theory of Algebraic Datatypes (Extended Abstract)
- 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
-
- auteur
- Sorin Stratulat
- titre
- E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning
- 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
-
- auteur
- Sophie Tourret, Jasmin Blanchette
- titre
- A modular Isabelle framework for verifying saturation provers
- 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
-
- auteur
- Petar Vukmirović, Jasmin Blanchette, Marijn J H Heule
- titre
- SAT-Inspired Eliminations for Superposition
- 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
-
- auteur
- Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
- titre
- Making Higher-Order Superposition Work
- 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
-
- auteur
- Masaki Waga, Étienne André, Ichiro Hasuo
- titre
- Model-bounded monitoring of hybrid systems
- 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
-
Book sections
- auteur
- Yamine Aït-Ameur, Régine Laleau, Dominique Méry, Neeraj Kumar Singh
- titre
- Towards Leveraging Domain Knowledge in State-Based Formal Methods
- 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
-
- auteur
- Dominique Méry, Souad Kherroubi
- titre
- Contextual Dependency in State-based Modelling
- 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
-
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Automated Orchestration of Security Chains Driven by Process Learning
- 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
-
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry
- titre
- Formal Ontological Analysis for Medical Protocols
- 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
-
Habilitation à diriger des recherches
- auteur
- Sorin Stratulat
- titre
- Noetherian Induction for Computer-Assisted First-Order Reasoning
- article
- Symbolic Computation [cs.SC]. Université de Lorraine, 2021
- Accès au texte intégral et bibtex
-
Special issue
- auteur
- Matthew England, Wolfram Koepf, Timur Sadykov, Werner Seiler, Thomas Sturm
- titre
- Computer Algebra in Scientific Computing 2019
- article
- Mathematics in Computer Science, 15 (2), 2021
- Accès au bibtex
-
- auteur
- Matthew England, François Boulier, Timur Sadykov, Thomas Sturm
- titre
- Computer Algebra in Scientific Computing 2020
- article
- Mathematics in Computer Science, 15 (3), 2021
- Accès au bibtex
-
- auteur
- Matthew England, Wolfram Koepf, Timur M. Sadykov, Werner Seiler, Thomas Sturm
- titre
- Special Issue
- article
- Aug 2019, Moscow, Russia. Mathematics in Computer Science, 2021
- Accès au bibtex
-
Books
- auteur
- Yamine Aït-Ameur, Shin Nakajima, Dominique Méry
- titre
- Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems
- article
- Springer Singapore, 2021, 978-981-15-5053-9. ⟨10.1007/978-981-15-5054-6⟩
- Accès au bibtex
-
Proceedings
- auteur
- Alexander Raschke, Dominique Méry
- titre
- Rigorous State-Based Methods-8th International Conference, ABZ 2021, Ulm, Germany, June 9–11, 2021, Proceedings
- 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
-
- auteur
- Arunkumar S, Dominique Méry, Indranil Saha, Lijun Zhang
- titre
- MEMOCODE ’21: Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design
- 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
-
Theses
- auteur
- Daniel El Ouraoui
- titre
- Methods for Higher-Order reasoning in SMT
- article
- Logique en informatique [cs.LO]. Université de Lorraine, 2021. Français. ⟨NNT : 2021LORR0023⟩
- Accès au texte intégral et bibtex
-
2020
Journal articles
- auteur
- Étienne André, Tian Huat Tan, Manman Chen, Shuang Liu, Jun Sun, Yang Liu, Jin Song Dong
- titre
- Automated synthesis of local time requirement for service composition
- article
- Software and Systems Modeling, 2020, 19, pp.983-1013. ⟨10.1007/s10270-020-00787-5⟩
- Accès au bibtex
-
- auteur
- Étienne André, Didier Lime, Nicolas Markey
- titre
- Language Preservation Problems in Parametric Timed Automata
- article
- Logical Methods in Computer Science, 2020, 16 (1), ⟨10.23638/LMCS-16⟩
- Accès au bibtex
-
- auteur
- Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, Pascal Fontaine
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- 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
-
- auteur
- Armin Biere, Cesare Tinelli, Christoph Weidenbach
- titre
- Preface to the Special Issue on Automated Reasoning Systems
- article
- Journal of Automated Reasoning, 2020, 64 (3), pp.361-362. ⟨10.1007/s10817-019-09531-1⟩
- Accès au bibtex
-
- 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
- titre
- Identifying the parametric occurrence of multiple steady states for some biological networks
- 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
-
- auteur
- Martin Bromberger, Thomas Sturm, Christoph Weidenbach
- titre
- A complete and terminating approach to linear integer solving
- 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
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- Politeness and Combination Methods for Theories with Bridging Functions
- article
- Journal of Automated Reasoning, 2020, 64, pp.97-134. ⟨10.1007/s10817-019-09512-4⟩
- Accès au texte intégral et bibtex
-
- auteur
- Andrew Cropper, Sophie Tourret
- titre
- Logical reduction of metarules
- article
- Machine Learning, 2020, 109 (7), pp.1323 – 1369. ⟨10.1007/s10994-019-05834-x⟩
- Accès au texte intégral et bibtex
-
- auteur
- James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
- titre
- Symbolic computation and satisfiability checking (Editorial)
- 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
-
- auteur
- Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
- titre
- Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
- 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
-
- auteur
- Andreas Teucke, Christoph Weidenbach
- titre
- SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment
- 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
-
Conference papers
- auteur
- Heba Alkayed, Horatiu Cirstea, Stephan Merz
- titre
- An Extension of PlusCal for Modeling Distributed Algorithms
- article
- TLA+ Community Event 2020, Oct 2020, Freiburg (online), Germany
- Accès au texte intégral et bibtex
-
- auteur
- Gilbert Busana, Brigitte Denis, Marie Duflot-Kremer, Sarah Higuet, Lara Kataja, Yves Kreis, Christophe Laduron, Christian Meyers, Yannick Parmentier, Robert Reuter, Armin Weinberger
- titre
- PIAF: promoting computational thinking and algorithmics in fundamental education
- 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
-
- auteur
- Horatiu Cirstea, Alexis Grall, Dominique Méry
- titre
- Generating Distributed Programs from Event-B Models
- article
- International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
- Accès au bibtex
-
- auteur
- Horatiu Cirstea, Pierre Lermusiaux, Pierre-Etienne Moreau
- titre
- Pattern eliminating transformations
- 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
-
- auteur
- Antoine Defourné
- titre
- Better Automation for TLA+ Proofs
- 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
-
- auteur
- Antoine Defourné, Petar Vukmirovic
- titre
- Higher-order Automation in TLAPS
- article
- TLA+ Community Event 2020, Oct 2020, Virtual, France
- Accès au texte intégral et bibtex
-
- auteur
- Marie Duflot, Yann Duplouy
- titre
- Statistical Model Checking of Distributed Programs within SimGrid
- 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
-
- auteur
- Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
- titre
- On a Notion of Relevance
- article
- Proceedings of the 33rd International Workshop on Description Logics (DL 2020), Sep 2020, Online, Greece
- Accès au texte intégral et bibtex
-
- auteur
- Jawher Jerray, Laurent Fribourg, Étienne André
- titre
- Guaranteed phase synchronization of hybrid oscillators using symbolic Euler’s method (verification challenge)
- 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
-
- auteur
- Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, Renate Schmidt
- titre
- Signature-Based Abduction for Expressive Description Logics
- 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
-
- auteur
- Ismail Mendil, Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry, Philippe Palanque
- titre
- An Integrated Framework for the Formal Analysis of Critical Interactive Systems
- article
- The 27th Asia-Pacific Software Engineering Conference, Jun Sun, Dec 2020, Singapour, Singapore. pp.10
- Accès au bibtex
-
- auteur
- Yannick Parmentier, Robert Reuter, Sarah Higuet, Lara Kataja, Yves Kreis, Marie Duflot-Kremer, Christophe Laduron, Christian Meyers, Gilbert Busana, Armin Weinberger, Brigitte Denis
- titre
- PIAF: Developing Computational and Algorithmic Thinking in Fundamental Education
- article
- AACE 2020 – EdMedia + Innovate Learning, Jun 2020, Amsterdam / Virtual, Netherlands. pp.315-322
- Accès au texte intégral et bibtex
-
- auteur
- Hamid Rahkooy, Cristian Vargas Montero
- titre
- A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks
- article
- 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing – SYNASC 2020, Sep 2020, Timisoara/Virtual, Romania
- Accès au bibtex
-
- auteur
- Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
- titre
- Politeness for the Theory of Algebraic Datatypes
- 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
-
- auteur
- Sorin Stratulat
- titre
- SPIKE, an automatic theorem prover — revisited
- 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
-
- auteur
- Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
- titre
- Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding
- article
- SMT 2020 – 18th International Workshop on Satisfiability Modulo Theories, Jul 2020, Online COVID-19, France
- Accès au texte intégral et bibtex
-
- auteur
- Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
- titre
- A Comprehensive Framework for Saturation Theorem Proving
- 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
-
Book sections
- auteur
- Hamid Rahkooy, Ovidiu Radulescu, Thomas Sturm
- titre
- A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks
- 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
-
- auteur
- Hamid Rahkooy, Thomas Sturm
- titre
- First-Order Tests for Toricity
- 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
-
- auteur
- Louis Viard, Laurent Ciarletta, Pierre-Etienne Moreau
- titre
- A Mission Definition, Verification and Validation Architecture
- 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
-
Special issue
- auteur
- James Harold Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
- titre
- Special Issue : Symbolic Computation and Satisfiability Checking
- article
- Journal of Symbolic Computation, 100, 2020
- Accès au bibtex
-
Proceedings
- auteur
- Alexander Raschke, Dominique Méry, Frank Houdek
- titre
- Rigorous State-Based Methods – 7th International Conference, {ABZ} 2020, Ulm, Germany, May 27-29, 2020, Proceedings
- 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
-
Reports
- auteur
- Zheng Cheng, Dominique Méry
- titre
- A Refinement Strategy for Hybrid System Design with Safety Constraints
- article
- [Research Report] Université de Lorraine; INRIA; CNRS. 2020
- Accès au texte intégral et bibtex
-
- auteur
- Horatiu Cirstea, Alexis Grall, Dominique Méry
- titre
- Generating Distributed Programs from Event-B Models
- article
- [Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Margaux Duroeulx
- titre
- Reliability assessment of systems modeled by fault trees thanks to satisfiability techniques
- article
- Performance et fiabilité [cs.PF]. Université de Lorraine, 2020. Français. ⟨NNT : 2020LORR0026⟩
- Accès au texte intégral et bibtex
-
- auteur
- Mathias Fleury
- titre
- Formalization of Logical Calculi in Isabelle/HOL
- article
- Logic in Computer Science [cs.LO]. Universität des Saarlandes Saarbrücken, 2020. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Martin Bromberger, Alberto Fiori, Christoph Weidenbach
- titre
- SCL with Theory Constraints
- article
- 2020
- Accès au texte intégral et bibtex
-
- auteur
- Niclas Kruff, Christoph Lüders, Ovidiu Radulescu, Thomas Sturm, Sebastian Walcher
- titre
- Algorithmic Reduction of Biological Networks With Multiple Time Scales
- article
- 2020
- Accès au bibtex
-
- auteur
- Hamid Rahkooy, Thomas Sturm
- titre
- First-Order Tests for Toricity
- article
- 2020
- Accès au bibtex
-
- auteur
- Hamid Rahkooy, Ovidiu Radulescu, Thomas Sturm
- titre
- A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks
- article
- 2020
- Accès au bibtex
-
- auteur
- Werner M. Seiler, Matthias Seiss, Thomas Sturm
- titre
- A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations
- article
- 2020
- Accès au bibtex
-
2019
Journal articles
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Dietrich Klakow
- titre
- A Formal Proof of the Expressiveness of Deep Learning
- 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
-
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- titre
- Selected Extended Papers of ITP 2016: Preface
- 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
-
- auteur
- Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
- titre
- Bindings as Bounded Natural Functors
- 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
-
- auteur
- Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat
- titre
- Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques
- article
- Journal of Symbolic Computation, 2019, 90, pp.3-41. ⟨10.1016/j.jsc.2018.04.002⟩
- Accès au texte intégral et bibtex
-
- auteur
- Igor Konnov, Jure Kukovec, Thanh-Hai Tran
- titre
- TLA+ Model Checking Made Symbolic
- 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
-
- auteur
- Igor Konnov
- 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.
- article
- Formal Aspects of Computing, 2019, pp.455-456. ⟨10.1007/s00165-019-00486-z⟩
- Accès au texte intégral et bibtex
-
- auteur
- Margarida Romero, Marie Duflot, Thierry Viéville
- titre
- The robot game : analysis of a computational thinking unplugged activity under the perspective of embodied cognition.
- article
- Review of science, mathematics and ICT education, 2019, 13 (1), ⟨10.26220/rev.3089⟩
- Accès au texte intégral et bibtex
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- article
- Electronic Communications of the EASST, 2019, 076, ⟨10.14279/tuj.eceasst.76.1075.1042⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark Barrett
- titre
- Extending SMT Solvers to Higher-Order Logic
- 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
-
- auteur
- Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, Hans-Jörg Schurr
- titre
- Better SMT Proofs for Easier Reconstruction
- article
- AITP 2019 – 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann
- titre
- Superposition with Lambdas
- 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
-
- auteur
- Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
- titre
- Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries
- 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
-
- auteur
- Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine, Cezary Kaliszyk
- titre
- Machine Learning for Instance Selection in SMT Solving
- article
- AITP 2019 – 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette
- titre
- Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
- 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
-
- auteur
- Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
- titre
- SPASS-SATT: A CDCL(LA) Solver
- 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
-
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry
- titre
- Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
- 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
-
- auteur
- Horatiu Cirstea, Pierre-Etienne Moreau
- titre
- Generic Encodings of Constructor Rewriting Systems
- 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
-
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- titre
- Integrating satisfiability solving in the assessment of system reliability modeled by dynamic fault trees
- 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
-
- auteur
- Alberto Fiori, Christoph Weidenbach
- titre
- SCL: Clause Learning from Simple Models
- 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
-
- auteur
- Mathias Fleury, Hans-Jörg Schurr
- titre
- Reconstructing veriT Proofs in Isabelle/HOL
- 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
-
- auteur
- Pierre Lermusiaux, Horatiu Cirstea, Pierre-Etienne Moreau
- titre
- Pattern eliminating transformations
- article
- CIEL 2019 – 8ème Conférence en IngénieriE du Logiciel, Jun 2019, Toulouse, France
- Accès au texte intégral et bibtex
-
- auteur
- Dominique Méry
- titre
- Verification by Construction of Distributed Algorithms
- 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
-
- auteur
- Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
- titre
- A Verified Prover Based on Ordered Resolution
- 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
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Automated Factorization of Security Chains in Software-Defined Networks
- 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
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- A Tool Suite for the Automated Synthesis of Security Function Chains
- 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
-
- auteur
- Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
- titre
- Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
- 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
-
- auteur
- Andreas Teucke, Marco Voigt, Christoph Weidenbach
- titre
- On the Expressivity and Applicability of Model Representation Formalisms
- 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
-
- auteur
- Sophie Tourret, Andrew Cropper
- titre
- SLD-Resolution Reduction of Second-Order Horn Fragments
- 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
-
- auteur
- Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz
- titre
- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
- 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
-
- auteur
- Christoph Weidenbach
- titre
- The Challenge of Unifying Semantic and Syntactic Inference Restrictions
- 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
-
Book sections
- auteur
- Peter Baumgartner, Uwe Waldmann
- titre
- Hierarchic Superposition Revisited
- 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
-
- auteur
- Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
- titre
- Theory Combination: Beyond Equality Sharing
- 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
-
- auteur
- Stephan Merz
- titre
- Formal specification and verification
- 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
-
Proceedings
- auteur
- Pascal Fontaine
- titre
- Automated Deduction – CADE-27
- 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
-
- auteur
- Dominique Méry, Shengchao Qin
- titre
- 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE)
- 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
-
Theses
- auteur
- Martin Bromberger
- titre
- Decision Procedures for Linear Arithmetic
- article
- Logic in Computer Science [cs.LO]. Saarland University, 2019. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Nicolas Schnepf
- titre
- Orchestration and verification of security functions for smart devices
- 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
-
- auteur
- Marco Voigt
- titre
- Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
- article
- Logic in Computer Science [cs.LO]. Universität des Saarlandes, 2019. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
- titre
- Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
- article
- 2019
- Accès au texte intégral et bibtex
-
- auteur
- Gilbert Busana, Brigitte Denis, Marie Duflot-Kremer, Sarah Higuet, Lara Kataja, Yves Kreis, Christophe Laduron, Christian Meyers, Yannick Parmentier, Robert Reuter, Armin Weinberger
- titre
- PIAF : développer la Pensée Informatique et Algorithmique dans l’enseignement Fondamental
- article
- 2019
- Accès au texte intégral et bibtex
-
- auteur
- Dima Grigoriev, Alexandru Iosif, Hamid Rahkooy, Thomas Sturm, Andreas Weber
- titre
- Efficiently and Effectively Recognizing Toricity of Steady State Varieties
- article
- 2019
- Accès au bibtex
-
2018
Journal articles
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- titre
- A Machine-Checked Correctness Proof for Pastry
- 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
-
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- article
- Journal of Automated Reasoning, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩
- Accès au texte intégral et bibtex
-
- auteur
- Stephan Merz, Hernán Vanzetto
- titre
- Encoding TLA+ into unsorted and many-sorted first-order logic
- 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
-
Conference papers
- 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
- titre
- On the importance of explicit domain modelling in refinement-based modelling design: experiments with Event-B
- 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
-
- auteur
- Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, Cesare Tinelli
- titre
- Higher-Order SMT Solving (Work in Progress)
- article
- SMT 2018 – 16th International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Alexander Bentkamp, Simon Cruanes, Jasmin Christian Blanchette, Uwe Waldmann
- titre
- Superposition for Lambda-Free Higher-Order Logic
- article
- IJCAR 2018 – 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
- titre
- Superposition with Datatypes and Codatatypes
- article
- IJCAR 2018 – 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Martin Bromberger
- titre
- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
- 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
-
- auteur
- Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
- titre
- An Automation-Friendly Set Theory for the B Method
- 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
-
- auteur
- Guillaume Bury, Simon Cruanes, David Delahaye
- titre
- SMT Solving Modulo Tableau and Rewriting Theories
- article
- SMT 2018 – 16th International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Andrew Cropper, Sophie Tourret
- titre
- Derivation Reduction of Metarules in Meta-interpretive Learning
- 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
-
- auteur
- Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
- titre
- A verified SAT solver with watched literals using imperative HOL
- 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
-
- auteur
- Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To, Xuan Tung Vu
- titre
- Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
- 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
-
- auteur
- Hoon Hong, Thomas Sturm
- titre
- Positive Solutions of Systems of Signed Parametric Polynomial Inequalities
- 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
-
- auteur
- Igor Konnov, Josef Widder
- titre
- ByMC: Byzantine Model Checker
- 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
-
- auteur
- Jure Kukovec, Thanh-Hai Tran, Igor Konnov
- titre
- Extracting Symbolic Transitions from $TLA+$ Specifications
- 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
-
- auteur
- Jure Kukovec, Igor Konnov, Josef Widder
- titre
- Reachability in Parameterized Systems: All Flavors of Threshold Automata
- 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
-
- auteur
- Dominique Méry
- titre
- Modelling by Patterns for Correct-by-Construction Process.
- 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
-
- auteur
- Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
- titre
- Revisiting Enumerative Instantiation
- 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
-
- auteur
- Margarida Romero, Benjamin Lille, Thierry Viéville, Marie Duflot-Kremer, Cindy De Smet, David Belhassein
- titre
- Analyse comparative d’une activité d’apprentissage de la programmation en mode branché et débranché
- 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
-
- auteur
- Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
- titre
- Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
- article
- IJCAR 2018 – 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- 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
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Synaptic: A formal checker for SDN-based security policies
- 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
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Generation of SDN policies for protecting Android environments based on automata learning
- 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
-
- auteur
- Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Mery
- titre
- Formal Ontology Driven Model Refactoring
- 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
-
- auteur
- Sorin Stratulat
- titre
- Validating Back-links of FOLID Cyclic Pre-proofs
- 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
-
- auteur
- Thomas Sturm
- titre
- Thirty Years of Virtual Substitution
- 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
-
Habilitation à diriger des recherches
- auteur
- Pascal Fontaine
- titre
- Satisfiability Modulo Theories: state-of-the-art, contributions, project
- article
- Logic in Computer Science [cs.LO]. Université de lorraine, 2018
- Accès au texte intégral et bibtex
-
Special issue
- auteur
- El Hassan Abdelwahed, Ladjel Bellatreche, Djamal Benslimane, Matteo Golfarelli, Stéphane Jean, Dominique Méry, Kazumi Nakamatsu, Carlos Ordonez
- titre
- New Trends in Model and Data Engineering
- 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
-
- auteur
- Régine Laleau, Dominique Méry, Shin Nakajima, Elena Troubitsyna
- 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)
- article
- Electronic Proceedings in Theoretical Computer Science, 271, 2018, ⟨10.4204/EPTCS.271⟩
- Accès au bibtex
-
Other publications
- auteur
- François Boulier, François Fages, Ovidiu Radulescu, Satya S Samal, Andreas Schuppert, Werner M. Seiler, Thomas Sturm, Sebastian Walcher, Andreas Weber
- titre
- The SYMBIONT Project: Symbolic Methods for Biological Networks
- article
- 2018
- Accès au texte intégral et bibtex
-
Poster communications
- auteur
- François Boulier, Francois Fages, Ovidiu Radulescu, Satya Swarup Samal, Andreas Schuppert, Werner Seiler, Thomas Sturm, Sebastian Walcher, Andreas Weber
- titre
- The SYMBIONT Project: Symbolic Methods for Biological Networks
- article
- ISSAC 2018, Jul 2018, New York City, NY, United States
- Accès au bibtex
-
Documents associated with scientific events
- auteur
- Igor Konnov, Jure Kukovec, Thanh Hai Tran
- titre
- BmcMT: Bounded Model Checking of TLA + Specifications with SMT
- article
- TLA+ Community Meeting 2018, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Igor Konnov, Stephan Merz
- titre
- Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary
- article
- BCRB 2018 – DSN Workshop on Byzantine Consensus and Resilient Blockchains, Jun 2018, Luxembourg, Luxembourg
- Accès au texte intégral et bibtex
-
Proceedings
- auteur
- El Hassan Abdelwahed, Ladjel Bellatreche, Matteo Golfarelli, Dominique Méry, Carlos Ordonez
- titre
- Model and Data Engineering. 8th International Conference, MEDI 2018, Proceedings
- article
- Springer, 2018, Lecture Notes in Computer Science, 978-3-030-00855-0. ⟨10.1007/978-3-030-00856-7⟩
- Accès au bibtex
-
Reports
- auteur
- Andrew J Reynolds, Haniel Barbosa, Pascal Fontaine
- titre
- Revisiting Enumerative Instantiation
- article
- [Research Report] University of Iowa; Inria. 2018
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery
- titre
- Formal Proofs of Tarjan’s Algorithm in Why3, Coq, and Isabelle
- article
- 2018
- Accès au texte intégral et bibtex
-
2017
Journal articles
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- titre
- Soundness and Completeness Proofs by Coinductive Methods
- 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
-
- auteur
- Martin Bromberger, Christoph Weidenbach
- titre
- New Techniques for Linear Arithmetic: Cubes and Equalities
- 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
-
- auteur
- Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
- titre
- NP-completeness of small conflict set generation for congruence closure
- article
- Formal Methods in System Design, 2017, 51 (3), pp.533 – 544. ⟨10.1007/s10703-017-0283-x⟩
- Accès au texte intégral et bibtex
-
- auteur
- Dominique Méry, Mike Poppleton
- titre
- Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
- article
- Software and Systems Modeling, 2017, 16 (4), pp.1083–1115. ⟨10.1007/s10270-015-0504-y⟩
- Accès au bibtex
-
- auteur
- Dominique Méry
- titre
- Playing with State-Based Models for Designing Better Algorithms
- article
- Future Generation Computer Systems, 2017, 68, pp.445-455. ⟨10.1016/j.future.2016.04.019⟩
- Accès au bibtex
-
- auteur
- Thomas Sturm
- titre
- A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
- article
- Mathematics in Computer Science, 2017, 11 (3-4), pp.483 – 502. ⟨10.1007/s11786-017-0319-z⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Étienne André, Hoang Gia Nguyen, Laure Petrucci
- titre
- Efficient Parameter Synthesis Using Optimized State Exploration Strategies
- 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
-
- auteur
- Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- 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
-
- auteur
- Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
- titre
- Congruence Closure with Free Variables
- 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
-
- auteur
- Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
- titre
- A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
- 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
-
- auteur
- Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
- titre
- A Formal Proof of the Expressiveness of Deep Learning
- 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
-
- 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
- titre
- Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
- 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
-
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
- titre
- Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
- 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
-
- auteur
- Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
- titre
- Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
- article
- Programming Languages and Systems – 26th European Symposium on Programming, ESOP 2017, Apr 2017, Uppsala, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- 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
-
- auteur
- Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
- titre
- Foundational nonuniform (Co)datatypes for higher-order logic
- 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
-
- auteur
- Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
- titre
- A Lambda-Free Higher-Order Recursive Path Order
- 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
-
- auteur
- Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
- titre
- Towards Strong Higher-Order Automation for Fast Interactive Verification
- 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
-
- 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
- titre
- A Case Study on the Parametric Occurrence of Multiple Steady States
- 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
-
- auteur
- Simon Cruanes
- titre
- Satisfiability Modulo Bounded Checking
- 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
-
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- titre
- Satisfiability techniques for computing minimal tie sets in reliability assessment
- 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
-
- auteur
- Matthew England, Hassan Errami, Dima Grigoriev, Ovidiu Radulescu, Thomas Sturm, Andreas Weber
- titre
- Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
- 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
-
- auteur
- Faten Fakhfakh, Mohamed Tounsi, Mohamed Mosbah, Ahmed Hadj Kacem, Dominique Méry
- titre
- A Formal Approach for Maintaining Forest Topologies in Dynamic Networks
- 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
-
- auteur
- Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Vu
- titre
- Subtropical Satisfiability
- 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
-
- auteur
- Paul J. Gibson, Souad Kherroubi, Dominique Méry
- titre
- Applying a Dependency Mechanism for Voting Protocol Models Using Event-B
- 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
-
- auteur
- John Paul Gibson, Dominique Méry
- titre
- Explicit modelling of physical measures: from Event-B to Java
- 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
-
- auteur
- Sara Himmiche, Alexis Aubry, Pascale Marangé, Jean-François Pétin, Marie Duflot
- titre
- Using statistical-model-checking-based simulation for evaluating the robustness of a production schedule
- 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
-
- auteur
- Sara Himmiche, Pascale Marangé, Alexis Aubry, Marie Duflot, Jean-François Pétin
- titre
- Evaluation de la robustesse d’un ordonnancement par Automates Temporisés Stochastiques
- 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
-
- auteur
- Matthias Horbach, Marco Voigt, Christoph Weidenbach
- titre
- On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic
- 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
-
- auteur
- Souad Kherroubi, Dominique Méry
- titre
- Contextualization and Dependency in State-Based Modelling – Application to Event-B
- 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
-
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- titre
- Automated Verification of Security Chains in Software-Defined Networks with Synaptic
- 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
-
- auteur
- Sorin Stratulat
- titre
- Cyclic Proofs with Ordering Constraints
- 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
-
- auteur
- Andreas Teucke, Christoph Weidenbach
- titre
- Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
- 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
-
- auteur
- Marco Voigt
- titre
- A fine-grained hierarchy of hard problems in the separated fragment
- 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
-
- auteur
- Marco Voigt
- titre
- The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable
- 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
-
Book sections
- auteur
- Simon Cruanes
- titre
- Superposition with Structural Induction
- 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
-
Special issue
- auteur
- Catherine Dubois, Paolo Masci, Dominique Méry
- titre
- Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016, Limassol, Cyprus, November 8, 2016
- article
- Nov 2016, Cyprus. Electronic Proceedings in Theoretical Computer Science, 240, 2017, ⟨10.4204/EPTCS.240⟩
- Accès au bibtex
-
Reports
- auteur
- Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
- titre
- Scalable Fine-Grained Proofs for Formula Processing
- 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
-
- auteur
- Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
- titre
- Congruence Closure with Free Variables
- article
- [Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
- Accès au texte intégral et bibtex
-
- auteur
- Leslie Lamport, Stephan Merz
- titre
- Auxiliary Variables in TLA+
- article
- [Research Report] Inria Nancy – Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Haniel Barbosa
- titre
- New techniques for instantiation and proof production in SMT solving
- article
- Artificial Intelligence [cs.AI]. Université de Lorraine, 2017. English. ⟨NNT : 2017LORR0091⟩
- Accès au texte intégral et bibtex
-
- auteur
- Daniel Wand
- titre
- Superposition: Types and Induction
- article
- Computer Science [cs]. Saarland University, 2017. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- titre
- Satisfiability techniques for computing minimal tie sets in reliability assessment
- article
- 2017
- Accès au texte intégral et bibtex
-
- auteur
- Matthias Horbach, Marco Voigt, Christoph Weidenbach
- titre
- The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
- article
- 2017
- Accès au texte intégral et bibtex
-
2016
Journal articles
- auteur
- Yamine Aït-Ameur, Dominique Méry
- titre
- Making explicit domain knowledge in formal system development
- article
- Science of Computer Programming, 2016, 121 (100–127), ⟨10.1016/j.scico.2015.12.004⟩
- Accès au bibtex
-
- auteur
- Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
- titre
- A Learning-Based Fact Selector for Isabelle/HOL
- article
- Journal of Automated Reasoning, 2016, 57, pp.219 – 244. ⟨10.1007/s10817-016-9362-8⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
- titre
- Hammering towards QED
- 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
-
- auteur
- Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
- titre
- Semi-intelligible Isar Proofs from Machine-Generated Proofs
- article
- Journal of Automated Reasoning, 2016, ⟨10.1007/s10817-015-9335-3⟩
- Accès au texte intégral et bibtex
-
- auteur
- Marek Košta, Thomas Sturm, Andreas Dolzmann
- titre
- Better answers to real questions
- article
- Journal of Symbolic Computation, 2016, 74, pp.255 – 275. ⟨10.1016/j.jsc.2015.07.002⟩
- Accès au bibtex
-
- auteur
- Stephan Merz, Jun Pang
- titre
- Editorial
- 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
-
- auteur
- Stephan Merz, Jun Pang
- titre
- Editorial
- 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
-
- auteur
- Mohamed Mosbah, Mohamed Tounsi, Dominique Mery
- titre
- From Event-B specifications to programs for distributed algorithms
- 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
-
- 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
- titre
- Satisfiability Checking and Symbolic Computation
- article
- ACM Communications in Computer Algebra, 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
- Accès au bibtex
-
Conference papers
- 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
- titre
- SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
- article
- Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland
- Accès au texte intégral et bibtex
-
- auteur
- Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
- titre
- Proving Determinacy of the PharOS Real-Time Operating System
- 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
-
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- titre
- A Rigorous Correctness Proof for Pastry
- 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
-
- auteur
- Haniel Barbosa
- titre
- Efficient Instantiation Techniques in SMT (Work In Progress)
- 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
-
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- 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
-
- auteur
- Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
- titre
- Friends with Benefits
- article
- Isabelle Workshop 2016, Aug 2016, Nancy, France
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
- titre
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)
- article
- Isabelle Workshop 2016, Aug 2016, Nancy, France
- Accès au texte intégral et bibtex
-
- auteur
- Martin Bromberger, Christoph Weidenbach
- titre
- Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
- article
- 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. pp.15-30
- Accès au texte intégral et bibtex
-
- auteur
- Martin Bromberger, Christoph Weidenbach
- titre
- Fast Cube Tests for LIA Constraint Solving
- 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
-
- auteur
- Simon Cruanes, Jasmin Christian Blanchette
- titre
- Extending Nunchaku to Dependent Type Theory
- 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
-
- auteur
- Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski
- titre
- Compliance, Functional Safety and Fault Detection by Formal Methods
- 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
-
- auteur
- Jon Haël Brenas, Rachid Echahed, Martin Strecker
- titre
- Ensuring Correctness of Model Transformations While Remaining Decidable
- 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
-
- auteur
- Dominique Méry, Rosemary Monahan, Cheng Zheng
- titre
- On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin
- 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
-
- auteur
- Stephan Merz, Hernán Vanzetto
- titre
- Encoding TLA+ into Many-Sorted First-Order Logic
- 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
-
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
- titre
- Model Finding for Recursive Functions in SMT
- 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
-
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette
- titre
- A Decision Procedure for (Co)datatypes in SMT Solvers
- article
- IJCAI 2016 – 25th International Joint Conference on Artificial Intelligence, Jul 2016, New York, United States
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Sturm, Marco Voigt, Christoph Weidenbach
- titre
- Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
- article
- LICS 2016, Jul 2016, New York, United States. pp.86 – 95, ⟨10.1145/2933575.2934532⟩
- Accès au bibtex
-
- auteur
- Andreas Teucke, Christoph Weidenbach
- titre
- Ordered Resolution with Straight Dismatching Constraints
- 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
-
Book sections
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Incremental Proof-Based Development for Resilient Distributed Systems
- article
- Trustworthy Cyber-Physical Systems Engineering, Taylor and Francis Group, 2016, Trustworthy Cyber-Physical Systems Engineering
- Accès au bibtex
-
Habilitation à diriger des recherches
- auteur
- Didier Fass
- titre
- L’homme augmenté : Épistémologie et bio-ingénierie de l’humain machine
- article
- Life Sciences [q-bio]. Université de Lorraine, 2016
- Accès au texte intégral et bibtex
-
Books
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- titre
- Interactive Theorem Proving
- article
- Springer, 9807, 2016, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-43144-4⟩
- Accès au bibtex
-
2015
Journal articles
- auteur
- Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
- titre
- HASL: A new approach for performance evaluation and model checking from concepts to experimentation
- article
- Performance Evaluation, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩
- Accès au texte intégral et bibtex
-
- auteur
- Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, Andreas Weber
- titre
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- article
- Journal of Computational Physics, 2015, 291, pp.279-302. ⟨10.1016/j.jcp.2015.02.050⟩
- Accès au bibtex
-
Conference papers
- auteur
- Gábor Alagi, Christoph Weidenbach
- titre
- {NRCL} – a model building approach to the {Bernays-Schönfinkel} fragment
- 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
-
- auteur
- Haniel Barbosa, Pascal Fontaine
- titre
- Congruence Closure with Free Variables (Work in Progress)
- article
- QUANTIFY 2015 – 2nd International Workshop on Quantification, Aug 2015, Berlin, Germany
- Accès au texte intégral et bibtex
-
- auteur
- Peter Baumgartner, Joshua Bax, Uwe Waldmann
- titre
- Beagle – A Hierarchic Superposition Prover
- 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
-
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- titre
- Witnessing (Co)datatypes
- article
- ESOP 2015, Apr 2015, London, United Kingdom. ⟨10.1007/978-3-662-46669-8_15⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
- titre
- Foundational Extensible Corecursion: A Proof Assistant Perspective
- article
- ICFP 2015, Aug 2015, Vancouver, Canada. ⟨10.1145/2784731.2784732⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow
- titre
- Mining the Archive of Formal Proofs
- 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
-
- auteur
- Martin Bromberger, Thomas Sturm, Christoph Weidenbach
- titre
- Linear Integer Arithmetic Revisited
- article
- 25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. pp.623-637
- Accès au bibtex
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- 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
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- A Rewriting Approach to the Combination of Data Structures with Bridging Theories
- 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
-
- auteur
- David Déharbe, Stephan Merz
- titre
- Software Component Design with the B Method — A Formalization in Isabelle/HOL
- 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
-
- auteur
- Marie Duflot, Martin Quinson, Florent Masseglia, Didier Roy, Julien Vaubourg, Thierry Viéville
- titre
- When sharing computer science with everyone also helps avoiding digital prejudices
- article
- SCRATCH, Aug 2015, Amsterdam, Netherlands
- Accès au texte intégral et bibtex
-
- auteur
- Didier Fass, Dominique Méry
- titre
- Integrated human systems design : bridging the gap between formal and experimental approaches
- article
- NASA AMES Research Center, Human Systems Integration Division,, 2015, MOFETT FIELD – Etats-Unis d’Amérique, Unknown Region
- Accès au bibtex
-
- auteur
- Marion Guthmuller, Martin Quinson, Gabriel Corona
- titre
- System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
- 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
-
- auteur
- Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
- titre
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation
- 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
-
- auteur
- Dominique Méry, Sawant Rushikesh, Anton Tarasyuk
- titre
- Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study
- article
- Model and Data Engineering – 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. pp.89-102
- Accès au bibtex
-
- auteur
- Dominique Mery, Neeraj Kumar Singh
- titre
- Analyzing Requirements Using Environment Modelling
- 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
-
- auteur
- Martin Quinson, Gérald Oster
- titre
- A Teaching System To Learn Programming: the Programmer’s Learning Machine
- 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
-
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette
- titre
- A Decision Procedure for (Co)datatypes in SMT Solvers
- 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
-
- auteur
- Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli
- titre
- Model Finding for Recursive Functions in SMT
- 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
-
- auteur
- Renate Schmidt, Uwe Waldmann
- titre
- Modal Tableau Systems with Blocking and Congruence Closure
- 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
-
- auteur
- Thomas Sturm
- titre
- Subtropical Real Root Finding
- article
- Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ACM, Jul 2015, Bath, United Kingdom
- Accès au bibtex
-
Book sections
- auteur
- Carlos Areces, Pascal Fontaine, Stephan Merz
- titre
- Modal Satisfiability via SMT Solving
- 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
-
- auteur
- Christoph Weidenbach
- titre
- Automated Reasoning Building Blocks
- 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
-
Other publications
- auteur
- Marek Kosta, Thomas Sturm
- titre
- A Generalized Framework for Virtual Substitution
- article
- 2015, pp.17
- Accès au bibtex
-
- auteur
- Marco Voigt, Christoph Weidenbach
- titre
- Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
- article
- 2015
- Accès au bibtex
-
Books
- auteur
- Catherine Dubois, Paolo Masci, Dominique Méry
- titre
- Second International Workshop on Formal Integrated Development Environment
- article
- EPTCS, 187, 2015, EPTCS ⟨10.4204/EPTCS.187⟩
- Accès au bibtex
-
- auteur
- Pascal Fontaine, Thomas Sturm, Uwe Waldmann
- titre
- Foreword to the Special Focus on Constraints and Combinations
- article
- Dongming Wang. Springer, 9 (3), 2015, Mathematics in Computer Science, ⟨10.1007/s11786-015-0239-8⟩
- Accès au bibtex
-
Proceedings
- auteur
- Jasmin Christian Blanchette, Nikolai Kosmatov
- titre
- Tests and Proofs
- 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
-
Theses
- auteur
- Manamiary Bruno Andriamiarina
- titre
- Developing correct-by-construction distributed algorithms
- article
- Modélisation et simulation. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0181⟩
- Accès au texte intégral et bibtex
-
- auteur
- Marion Guthmuller
- titre
- Dynamic formal verification of temporal properties on legacy distributed applications
- article
- Informatique [cs]. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0090⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- auteur
- Martin Bromberger, Thomas Sturm, Christoph Weidenbach
- titre
- Linear Integer Arithmetic Revisited
- article
- 2015
- Accès au bibtex
-
- auteur
- Marion Guthmuller, Gabriel Corona, Martin Quinson
- titre
- System-Level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
- article
- 2015
- Accès au texte intégral et bibtex
-
- auteur
- Marek Kosta, Thomas Sturm, Andreas Dolzmann
- titre
- Better Answers to Real Questions
- article
- 2015
- Accès au bibtex
-
- auteur
- Stephan Merz, Hernán Vanzetto
- titre
- Encoding TLA+ set theory into many-sorted first-order logic
- article
- 2015
- Accès au texte intégral et bibtex
-
2014
Journal articles
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version)
- article
- Computer Science and Information Systems, 2014, Computer Science and Information System, 11 (1), pp.251-270. ⟨10.2298/CSIS130122007A⟩
- Accès au bibtex
-
- auteur
- Myrto Arapinis, Marie Duflot
- titre
- Bounding messages for free in security protocols – extension to various security properties
- article
- Information and Computation, 2014, pp.34. ⟨10.1016/j.ic.2014.09.003⟩
- Accès au texte intégral et bibtex
-
- auteur
- Christopher W. Brown, Marek Kosta
- titre
- Constructing a single cell in cylindrical algebraic decomposition
- article
- Journal of Symbolic Computation, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩
- Accès au bibtex
-
- auteur
- Jingshu Chen, Marie Duflot, Stephan Merz
- titre
- Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
- article
- Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14
- Accès au texte intégral et bibtex
-
- auteur
- David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
- titre
- Integrating SMT solvers in Rodin
- 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
-
- auteur
- Marek Kosta, Pavol Duris
- titre
- Flip-Pushdown Automata with $k$ Pushdown Reversals and E0L Systems are Incomparable
- article
- Information Processing Letters, 2014, 114 (8), pp.417-420. ⟨10.1016/j.ipl.2014.03.003⟩
- Accès au bibtex
-
- auteur
- Manuel Lamotte-Schubert, Christoph Weidenbach
- titre
- BDI: a new decidable clause class
- article
- Journal of Logic and Computation, 2014, 24 (6), pp.28
- Accès au bibtex
-
- auteur
- Gerald Lüttgen, Stephan Merz
- titre
- Editorial: Special Issue of Automated Verification of Critical Systems
- article
- Science of Computer Programming, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
- Accès au bibtex
-
- auteur
- Dominique Méry, Bernhard Schätz, Alan Wassyng
- titre
- The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
- article
- Dagstuhl Reports, 2014, 4 (2), pp.17–37
- Accès au bibtex
-
Conference papers
- auteur
- Yamine Aït-Ameur, John Paul Gibson, Dominique Méry
- titre
- On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
- 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
-
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Analysis of Self-* and P2P Systems using Refinement
- article
- ABZ 2014 – 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Yamine AIT AMEUR and Klaus-Dieter SCHEWE, Jun 2014, Toulouse, France. pp.117-123, ⟨10.1007/978-3-662-43652-3_9⟩
- Accès au bibtex
-
- auteur
- Clark Barrett, Leonardo de Moura, Pascal Fontaine
- titre
- Proofs in satisfiability modulo theories
- article
- APPA (All about Proofs, Proofs for All), Jul 2014, Vienna, Austria
- Accès au bibtex
-
- auteur
- Peter Baumgartner, Joshua Bax, Uwe Waldmann
- titre
- Finite Quantification in Hierarchic Theorem Proving
- article
- 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. pp.152-167
- Accès au bibtex
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
- article
- Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, Jul 2014, Vienna, Austria
- Accès au bibtex
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- A Gentle Non-Disjoint Combination of Satisfiability Procedures
- article
- Automated Reasoning – 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. pp.122-136, ⟨10.1007/978-3-319-08587-6_9⟩
- Accès au bibtex
-
- auteur
- Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
- titre
- Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
- article
- ARQNL 2014 – 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
-
- auteur
- Konstantin Korovin, Marek Kosta, Thomas Sturm
- titre
- Towards Conflict-Driven Learning for Virtual Substitution
- article
- Computer Algebra in Scientific Computing – 16th International Workshop, CASC 2014, 2014, Warsaw, Poland. pp.256-270
- Accès au bibtex
-
- auteur
- Marek Kosta, Thomas Sturm, Andreas Dolzmann
- titre
- Better Answers to Real Questions
- article
- 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Philipp Rümmer and Christoph M. Wintersteiger, Jul 2014, Vienna, Austria. pp.69
- Accès au bibtex
-
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Formal Evaluation of Landing Gear System
- article
- SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam
- Accès au bibtex
-
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Modeling an Aircraft Landing System in Event-B
- article
- ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. pp.154-159
- Accès au bibtex
-
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- The Semantics of Refinement Chart
- article
- HCI International, Jun 2014, Heraklion, Greece. pp.415-426, ⟨10.1007/978-3-319-07725-3_42⟩
- Accès au bibtex
-
- auteur
- Dominique Méry
- titre
- Playing with State-Based Models for Designing Better Algorithms
- article
- Model and Data Engineering – 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. pp.1-3
- Accès au bibtex
-
- auteur
- Stephan Merz, Hernán Vanzetto
- titre
- Refinement Types for TLA+
- article
- NASA Formal Methods – 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩
- Accès au bibtex
-
- auteur
- Daniel Wand
- titre
- Polymorphic+Typeclass Superposition
- article
- 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
- Accès au texte intégral et bibtex
-
Book sections
- auteur
- Neeraj Kumar Singh, Dominique Méry
- titre
- Event B (english version)
- article
- Jean-Louis Boulanger. Formal Methods Applied to Complex Systems, Wiley, 2014, Formal Methods Applied to Complex Systems, 9781119002727. ⟨10.1002/9781119002727.ch10⟩
- Accès au bibtex
-
Books
- auteur
- Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry
- titre
- Proceedings 1st Workshop on Formal Integrated Development Environment
- article
- Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. EPTCS, 149, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩
- Accès au bibtex
-
- auteur
- Gerald Lüttgen, Stephan Merz
- titre
- Science of Computer Programming Special Issue: Automated Verification of Critical Systems
- article
- Elsevier, 96 (3), 2014, Science of Computer Programming, Jan Bergstra
- Accès au bibtex
-
Proceedings
- auteur
- Gabriel Ciobanu, Dominique Méry
- titre
- Theoretical Aspects of Computing – ICTAC 2014
- article
- Gabriel Ciobanu; Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, Sep 2014, Bucharest, Romania. 8687, Springer, 2014, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-10882-7⟩
- Accès au bibtex
-
- auteur
- Stéphane Demri, Deepak Kapur, Christoph Weidenbach
- titre
- Automated Reasoning – Seventh International Joint Conference (IJCAR 2014)
- article
- Stéphane Demri; Deepak Kapur; Christoph Weidenbach. 7th International Joint Conference – IJCAR 2014, Jun 2014, Vienna, Austria. 8562, Springer, 2014, LNCS – Lecture Notes in Computer Science, 978-3-319-08586-9. ⟨10.1007/978-3-319-08587-6⟩
- Accès au bibtex
-
- auteur
- Stephan Merz, Jun Pang
- titre
- Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014)
- article
- Stephan Merz; Jun Pang. 16th International Conference on Formal Engineering Methods – ICFEM 2014, Nov 2014, Luxembourg, Luxembourg. 8829, Springer, pp.460, 2014, LNCS – Lecture Notes in Computer Science, 978-3-319-11737-9. ⟨10.1007/978-3-319-11737-9⟩
- Accès au bibtex
-
Reports
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Analysis of Self-* and P2P Systems using Refinement (Full Report)
- article
- [Research Report] 2014
- Accès au texte intégral et bibtex
-
- auteur
- Paula Chocron, Pascal Fontaine, Christophe Ringeissen
- titre
- A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)
- article
- [Research Report] RR-8529, INRIA. 2014
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Hernán Vanzetto
- titre
- Proof automation and type synthesis for set theory in the context of TLA+
- article
- Computer Science [cs]. Université de Lorraine, 2014. English. ⟨NNT : 2014LORR0208⟩
- Accès au texte intégral et bibtex
-
2013
Journal articles
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Formal Specification of Medical Systems by Proof-Based Refinement
- article
- ACM Transactions on Embedded Computing Systems (TECS), 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩
- Accès au bibtex
-
Conference papers
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms
- article
- iFM – 10th International Conference on integrated Formal Methods – 2013, Jun 2013, Turku, Finland
- Accès au bibtex
-
- auteur
- Carlos Areces, David Déharbe, Pascal Fontaine, Orbe Ezequiel
- titre
- SyMT: finding symmetries in SMT formulas
- article
- 11th International Workshop on Satisfiability Modulo Theories – SMT, Jul 2013, Helsinki, Finland
- Accès au bibtex
-
- auteur
- Peter Baumgartner, Uwe Waldmann
- titre
- Hierarchic Superposition: Completeness without Compactness
- article
- MACIS 2013 – Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12
- Accès au bibtex
-
- auteur
- Peter Baumgartner, Uwe Waldmann
- titre
- Hierarchic Superposition With Weak Abstraction
- article
- 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. pp.39-57, ⟨10.1007/978-3-642-38574-2_3⟩
- Accès au bibtex
-
- auteur
- David Deharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
- titre
- Computing prime implicants
- 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
-
- auteur
- Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner Seiler, Thomas Sturm, Andreas Weber
- titre
- Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
- article
- CASC 2013 – 15th International Workshop on Computer Algebra in Scientific Computing, Sep 2013, Berlin, Germany. pp.88-99, ⟨10.1007/978-3-319-02297-0_7⟩
- Accès au bibtex
-
- auteur
- Ralf Karrenberg, Marek Kosta, Thomas Sturm
- titre
- Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
- article
- 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. pp.56-70, ⟨10.1007/978-3-642-40885-4_5⟩
- Accès au bibtex
-
- auteur
- Marek Kosta
- titre
- SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
- article
- Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), 2013, Nanning, China
- Accès au bibtex
-
- auteur
- Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
- titre
- Towards Certifying Network Calculus
- article
- ITP – 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.484-489, ⟨10.1007/978-3-642-39634-2_37⟩
- Accès au texte intégral et bibtex
-
- auteur
- Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
- titre
- Certifying Network Calculus in a Proof Assistant
- article
- EUCASS – 5th European Conference for Aeronautics and Space Sciences, Astrium and Technische Universität München, Jul 2013, Munich, Germany
- Accès au texte intégral et bibtex
-
- auteur
- Dominique Méry, Mike Poppleton
- titre
- Formal Modelling and Verification of Population Protocols
- article
- iFM – 10th International Conference on integrated Formal Methods – 2013, Jun 2013, Turku, Finland
- Accès au bibtex
-
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Ideal Mode Selection of a Cardiac Pacing System
- article
- 4th International Conference – Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management – DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. pp.258-267, ⟨10.1007/978-3-642-39173-6_31⟩
- Accès au bibtex
-
- auteur
- Dominique Méry, Monahan Rosemary
- titre
- Transforming EVENT B Models into Verified C# Implementations
- article
- VPT 2013 – First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
- Accès au bibtex
-
- auteur
- Mohammed Tounsi, Mohammed Mosbah, Dominique Méry
- titre
- From Event-B Specifications to Programs for Distributed Algorithms
- article
- WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. ⟨10.1109/WETICE.2013.44⟩
- Accès au bibtex
-
Book sections
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Event B
- article
- Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d’Informations, ISBN : 978-2-7462-3810-7
- Accès au bibtex
-
Books
- auteur
- Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
- titre
- Formal Verification of Distributed Algorithms
- article
- Bernadette Charron-Bost and Stephan Merz and Andrey Rybalchenko and Josef Widder. Dagstuhl, 3, pp.16, 2013, Dagstuhl Reports, ⟨10.4230/DagRep.3.4.1⟩
- Accès au bibtex
-
- auteur
- Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
- titre
- Frontiers of Combining Systems
- 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
-
2012
Journal articles
- auteur
- Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
- titre
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- article
- Science of Computer Programming, 2012, 77 (10-11), pp.1122-1150
- Accès au bibtex
-
Conference papers
- auteur
- Yamine Aït-Ameur, Dominique Méry
- titre
- Handling Heterogeneity in Formal Developments of Hardware and Software Systems
- 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
-
- auteur
- Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
- titre
- Revisiting Snapshot Algorithms by Refinement-based Techniques
- 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
-
- auteur
- Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, Camel Tanougast
- titre
- Formal Verification of Fault Tolerant NoC-based Architecture
- 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
-
- auteur
- Jasmin Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
- titre
- More SPASS with Isabelle — Superposition with Hard Sorts and Configurable Simplification
- article
- Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. pp.345-360
- Accès au bibtex
-
- auteur
- Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
- titre
- TLA+ Proofs
- article
- AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p
- Accès au bibtex
-
- auteur
- Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
- titre
- TLA+ Proofs
- 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
-
- auteur
- Tianxiang Lu, Stephan Merz, Christoph Weidenbach
- titre
- Formal Verification Of Pastry Using TLA+
- article
- International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France
- Accès au texte intégral et bibtex
-
- auteur
- Dominique Méry, Neeraj Kumar Singh
- titre
- Critical systems development methodology using formal techniques
- 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
-
- auteur
- Stephan Merz, Hernán Vanzetto
- titre
- Harnessing SMT Solvers for TLA+ Proofs
- article
- 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany
- Accès au texte intégral et bibtex
-
Master thesis
- auteur
- Martin Bromberger
- titre
- Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
- article
- Logic in Computer Science [cs.LO]. 2012
- Accès au bibtex
-
Books
- auteur
- Dimitra Giannakopoulou, Dominique Méry
- titre
- FM 2012: Formal Methods – 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings
- 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
-
Reports
- auteur
- Henri Debrat, Stephan Merz
- titre
- Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
- article
- [Research Report] 2012
- Accès au bibtex
-
- auteur
- Stephan Merz
- titre
- Stuttering Equivalence
- article
- [Research Report] 2012
- Accès au bibtex
-
Theses
- auteur
- Sabina Akhtar
- titre
- Formal Verification of Distributed Algorithms using PlusCal-2
- article
- Data Structures and Algorithms [cs.DS]. Université de Lorraine, 2012. English. ⟨NNT : 2012LORR0014⟩
- Accès au texte intégral et bibtex
-
2011
Conference papers
- auteur
- Thomas Sturm, Ashish Tiwari
- titre
- Verification and synthesis using real quantifier elimination
- article
- Proc. ISSAC 2011, Jun 2011, San Jose, United States. pp.329, ⟨10.1145/1993886.1993935⟩
- Accès au bibtex
-
