Publications

Publications HAL du labo/EPI 107895

2019

Journal articles

auteur
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
titre
Bindings as Bounded Natural Functors
article
Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), pp.1-34. ⟨10.1145/3290335⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01989726/file/bindings.pdf BibTex
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
titre
Politeness and Combination Methods for Theories with Bridging Functions
article
Journal of Automated Reasoning, Springer Verlag, In press
Accès au bibtex
BibTex
auteur
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat
titre
Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques
article
Journal of Symbolic Computation, Elsevier, 2019, 90, pp.3-41. ⟨10.1016/j.jsc.2018.04.002⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01590654/file/paper.pdf BibTex

Conference papers

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
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02191348/file/main.pdf 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
https://hal.archives-ouvertes.fr/hal-01937136/file/paper.pdf 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
https://hal.inria.fr/hal-02262205/file/final.pdf BibTex
auteur
Pierre Lermusiaux, Horatiu Cirstea, Pierre-Etienne Moreau
titre
Pattern eliminating transformations
article
CIEL 2019, Jun 2019, Toulouse, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02186325/file/main.pdf 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
https://hal.archives-ouvertes.fr/hal-01937141/file/paper.pdf 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
https://hal.inria.fr/hal-02111658/file/main.pdf 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
https://hal.inria.fr/hal-02111656/file/camera-ready.pdf BibTex
auteur
Petar Vukmirovic, 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
https://hal.inria.fr/hal-02178274/file/conf.pdf BibTex

Book sections

auteur
Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
titre
Theory Combination: Beyond Equality Sharing
article
Description Logic, Theory Combination, and All That – Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, pp.57-89, 2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02194001/file/paper.pdf 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
https://hal.inria.fr/hal-01925533/file/main.pdf BibTex

2018

Journal articles

auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
titre
A Machine-Checked Correctness Proof for Pastry
article
Science of Computer Programming, Elsevier, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01768758/file/paper.pdf BibTex
auteur
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
article
Journal of Automated Reasoning, Springer Verlag, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01904579/file/sat_article.pdf BibTex
auteur
Stephan Merz, Hernán Vanzetto
titre
Encoding TLA+ into unsorted and many-sorted first-order logic
article
Science of Computer Programming, Elsevier, 2018, 158, pp.3-20. ⟨10.1016/j.scico.2017.09.004⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01768750/file/tla2smt2_v3.pdf BibTex
auteur
Margarida Romero, Marie Duflot-Kremer, Thierry Viéville
titre
Le jeu du robot : analyse d’une activité d’informatique débranchée sous la perspective de la cognition incarnée
article
Review of science, mathematics and ICT education, Laboratory of Didactics of Sciences, Mathematics and ICT, Department of Educational Sciences and Early Childhood Education – University of Patras., A paraître
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01950335/file/RESMICTE-JeuDuRobot-R08.2-final.pdf BibTex

Conference papers

auteur
Yamine Ait Ameur, Idir Ait-Sadoune, Pierre Castéran, J. 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
ABZ 2018 – 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Jun 2018, Southampton, United Kingdom. pp.425–430, ⟨10.1007/978-3-319-91271-4_35⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01797538/file/AmeurACGHKMMSV18-1.pdf BibTex
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
https://hal.inria.fr/hal-01904595/file/lfhosup_paper.pdf 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
https://hal.inria.fr/hal-01904588/file/supdata_paper.pdf 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
https://hal.inria.fr/hal-01942228/file/paper.pdf BibTex
auteur
Guillaume Bury, Simon Cruanes, David Delahaye
titre
SMT Solving Modulo Tableau and Rewriting Theories
article
SMT: Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02083232/file/archsat.pdf BibTex
auteur
Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
titre
An Automation-Friendly Set Theory for the B Method
article
ABZ: 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
https://hal.archives-ouvertes.fr/hal-02082755/file/bset-auto.pdf 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
https://hal.inria.fr/hal-01904647/file/sat_2wl_paper.pdf 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
https://hal.inria.fr/hal-01946733/file/main.pdf 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
https://hal.inria.fr/hal-01889827/file/Hong-Sturm2018_Chapter_PositiveSolutionsOfSystemsOfSi.pdf 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
https://hal.inria.fr/hal-01909653/file/camera.pdf 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
https://hal.inria.fr/hal-01871131/file/camera.pdf 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
https://hal.inria.fr/hal-01871142/file/LIPIcs-CONCUR-2018-19.pdf BibTex
auteur
Sergueï Lenglet, Alan Schmitt
titre
HOπ in Coq
article
CPP 2018 – The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, ⟨10.1145/3167083⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01614987/file/cpp18.pdf 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
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
https://hal.archives-ouvertes.fr/hal-01877055/file/conf.pdf 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
https://hal.inria.fr/hal-01861732/file/Educode%20_UnPlugged-CDS06_soumis.pdf 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
https://hal.inria.fr/hal-01904610/file/rp_paper.pdf 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
https://hal.archives-ouvertes.fr/hal-01892390/file/main.pdf 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
https://hal.archives-ouvertes.fr/hal-01892423/file/main.pdf 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
https://hal.archives-ouvertes.fr/hal-01892397/file/main.pdf BibTex
auteur
Neeraj Kumar Singh, Yamine Ait Ameur, Dominique Méry
titre
Formal Ontological Driven Model Refactoring
article
ICECCS 2018 – 23rd International Conference on Engineering of Complex Computer Systems, Dec 2018, Melbourne, Australia
Accès au bibtex
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
https://hal.archives-ouvertes.fr/hal-01883826/file/Str__2018.pdf 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
https://hal.inria.fr/hal-01889817/file/p11-sturm.pdf BibTex

Directions of work or proceedings

auteur
El Hassan Abdelwahed, Ladjel Bellatreche, Matteo Golfarelli, Dominique Méry, Carlos Ordonez
titre
Model and Data Engineering
article
MEDI 2018 – International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Oct 2018, Marrakech, Morocco. 11163, Springer, 2018, Lecture Notes in Computer Science, 978-3-030-00855-0. ⟨https://doi.org/10.1007/978-3-030-00856-7⟩
Accès au bibtex
BibTex
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 (929), Springer, 2018, 978-3-030-02851-0. ⟨10.1007/978-3-030-02852-7⟩
Accès au bibtex
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
https://arxiv.org/pdf/1805.04636 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
https://tel.archives-ouvertes.fr/tel-01968404/file/HDR-standalone.pdf BibTex

Documents associated with scientific events

auteur
Igor Konnov, Jure Kukovec, Thanh 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
https://hal.inria.fr/hal-01899719/file/kkt18-bmcmt.pdf 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
https://hal.inria.fr/hal-01899723/file/main.pdf BibTex

Reports

auteur
Andrew 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
https://hal.inria.fr/hal-01744956/file/rep.pdf 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
https://hal.inria.fr/hal-01906155/file/paper.pdf BibTex
auteur
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
titre
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01925653/file/syncTAs.pdf 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, Springer Verlag, 2017, 58 (1), pp.149 – 179. ⟨10.1007/s10817-016-9391-3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643157/file/compl.pdf BibTex
auteur
Martin Bromberger, Christoph Weidenbach
titre
New Techniques for Linear Arithmetic: Cubes and Equalities
article
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.433-461. ⟨10.1007/s10703-017-0278-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01656397/file/paper.pdf BibTex
auteur
Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
titre
NP-completeness of small conflict set generation for congruence closure
article
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.533 – 544. ⟨10.1007/s10703-017-0283-x⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01908684/file/SMT.pdf BibTex
auteur
Dominique Méry
titre
Playing with State-Based Models for Designing Better Algorithms
article
Future Generation Computer Systems, Elsevier, 2017, 68, pp.445-455. ⟨ELSEVIER⟩. ⟨10.1016/j.future.2016.04.019⟩
Accès au bibtex
BibTex
auteur
Dominique Méry, Mike Poppleton
titre
Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
article
Software & Systems Modeling, Springer Verlag, 2017, 16 (4), pp.1083–1115
Accès au bibtex
BibTex
auteur
Thomas Sturm
titre
A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
article
Mathematics in Computer Science, Springer, 2017, 11 (3-4), pp.483 – 502. ⟨10.1007/s11786-017-0319-z⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01648690/file/10.1007_s11786-017-0319-z.pdf BibTex

Conference papers

auteur
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
titre
Congruence Closure with Free Variables
article
Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2017, Uppsala, Sweden. pp.220 – 230, ⟨10.1007/10721959_17⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590918/file/Barbosa1.pdf BibTex
auteur
Haniel Barbosa, Jasmin 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
https://hal.inria.fr/hal-01590922/file/Barbosa2.pdf BibTex
auteur
Heiko Becker, Jasmin 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
https://hal.inria.fr/hal-01592186/file/BeckerBlanchetteWaldmannWandCADE.pdf 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
https://hal.inria.fr/hal-01599172/file/paper.pdf BibTex
auteur
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
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
https://hal.inria.fr/hal-01592196/file/BiendarraBlanchetteEtAl-FroCos.pdf BibTex
auteur
Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
article
26th International Joint Conference on Artificial Intelligence, Aug 2017, Melbourne, Australia. pp.4786-4790, ⟨10.24963/ijcai.2017/667⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592164/file/BlanchetteFleuryWeidenbachIJCAI.pdf BibTex
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
https://hal.inria.fr/hal-01599174/file/conf.pdf 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
https://hal.inria.fr/hal-01599176/file/paper.pdf BibTex
auteur
Jasmin 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
https://hal.inria.fr/hal-01592189/file/BlanchetteWaldmannWandFoSSaCS.pdf 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
https://hal.inria.fr/hal-01599167/file/conf.pdf BibTex
auteur
Russell Bradford, James 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
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
https://hal.inria.fr/hal-01572531/file/paper.pdf 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
https://hal.inria.fr/hal-01630851/file/resubmission-Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf 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
https://hal.inria.fr/hal-01648691/file/10.1007-978-3-319-66320-3_8.pdf 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
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
https://hal.inria.fr/hal-01590899/file/10.1007-978-3-319-66167-4_11.pdf BibTex
auteur
Paul 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
https://hal.inria.fr/hal-01658423/file/446833_1_En_9_Chapter.pdf 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
https://hal.inria.fr/hal-01652138/file/himmiche-al-msr2017-final.pdf 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
https://hal.inria.fr/hal-01652140/file/Himmiche_et_al_Sohoma2017_vf.pdf 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
https://hal.inria.fr/hal-01592160/file/HorbachVoigtWeidenbachCADE.pdf 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
BibTex
auteur
Tony Ribeiro, Sophie Tourret, Maxime Folschette, Morgan Magnin, Domenico Borzacchiello, Francisco Chinesta, Olivier Roux, Katsumi Inoue
titre
Inductive learning from state transitions over continuous domains
article
ILP 2017 – 27th International Conference on Inductive Logic Programming, Sep 2017, Orléans, France. pp.124-139, ⟨10.1007/978-3-319-78090-0_9⟩
Accès au bibtex
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
https://hal.inria.fr/hal-01630806/file/camera-ready.pdf 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
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01590651/file/Str_10501_2017a.pdf 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
https://hal.inria.fr/hal-01657026/file/authorcopy.pdf 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
https://hal.inria.fr/hal-01592169/file/VoigtFroCoS.pdf 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
https://hal.inria.fr/hal-01592172/file/VoigtLICS.pdf 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
https://hal.inria.fr/hal-02062459/file/frocos_17_paper.pdf BibTex

Directions of work or proceedings

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
BibTex

Reports

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
https://hal.inria.fr/hal-01442691/file/main.pdf BibTex
auteur
Haniel Barbosa, Jasmin 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
https://hal.inria.fr/hal-01526841/file/rep.pdf 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
https://hal.inria.fr/hal-01488617/file/auxiliary.pdf 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
https://tel.archives-ouvertes.fr/tel-01591108/file/DDOC_T_2017_0091_MOREIRA_BARBOSA.pdf BibTex
auteur
Daniel Wand
titre
Superposition: Types and Induction
article
Computer Science [cs]. Saarland University, 2017. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01592497/file/thesis_wand.pdf BibTex

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
https://hal.inria.fr/hal-01518920/file/Techreport%20-%20Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf 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
https://hal.inria.fr/hal-01592177/file/HorbachVoigtWeidenbachCoRR.pdf BibTex

2016

Journal articles

auteur
Yamine Ait Ameur, Dominique Méry
titre
Making explicit domain knowledge in formal system development
article
Science of Computer Programming, Elsevier, 2016, 121 (100–127), ⟨ELSEVIER⟩. ⟨10.1016/j.scico.2015.12.004⟩
Accès au bibtex
BibTex
auteur
Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
titre
A Learning-Based Fact Selector for Isabelle/HOL
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 – 244. ⟨10.1007/s10817-016-9362-8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386986/file/paper.pdf BibTex
auteur
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
titre
Semi-intelligible Isar Proofs from Machine-Generated Proofs
article
Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01211748/file/paper.pdf BibTex
auteur
Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, Josef Urban
titre
Hammering towards QED
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (1), pp.101-148
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386988/file/h4qed-clean.pdf BibTex
auteur
Marek Košta, Thomas Sturm, Andreas Dolzmann
titre
Better answers to real questions
article
Journal of Symbolic Computation, Elsevier, 2016, 74, pp.255 – 275. ⟨10.1016/j.jsc.2015.07.002⟩
Accès au bibtex
BibTex
auteur
Stephan Merz, Jun Pang
titre
Editorial
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. ⟨10.1007/s00165-016-0390-2⟩
Accès au bibtex
BibTex
auteur
Stephan Merz, Jun Pang
titre
Editorial
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. ⟨10.1007/s00165-016-0390-2⟩
Accès au bibtex
BibTex
auteur
Thomas Sturm, Erika Abraham, John Abbott, Bern W. Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler
titre
Satisfiability Checking and Symbolic Computation
article
ACM Communications in Computer Algebra, Association for Computing Machinery (ACM), 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
Accès au bibtex
BibTex

Conference papers

auteur
Eriká Abrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler, Thomas Sturm
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
https://hal.inria.fr/hal-01377655/file/SCSC-CICM16.pdf 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
https://hal.inria.fr/hal-01322335/file/final.pdf 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
https://hal.inria.fr/hal-01322342/file/Main.pdf 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
https://hal.inria.fr/hal-01388976/file/paper-01.pdf 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
https://hal.inria.fr/hal-01336074/file/main.pdf BibTex
auteur
Jasmin 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
https://hal.inria.fr/hal-01401812/file/amico_abs.pdf BibTex
auteur
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)
article
Isabellle Workshop 2016, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401807/file/sat_abs.pdf BibTex
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
https://hal.inria.fr/hal-01403200/file/IJCAR2016.pdf 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
https://hal.inria.fr/hal-01403214/file/SMT2016.pdf BibTex
auteur
Simon Cruanes, Jasmin 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
https://hal.inria.fr/hal-01401696/file/nunchaku_tt.pdf 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
https://hal.inria.fr/hal-01403190/file/mypaper.pdf 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
https://hal.archives-ouvertes.fr/hal-01403585/file/paper61-procversion.pdf 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
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
https://hal.inria.fr/hal-01322328/file/tla2smt.pdf BibTex
auteur
Andrew Reynolds, Jasmin Blanchette
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
article
IJCAI 2016, Jul 2016, New York City, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01397082/file/sister.pdf BibTex
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
titre
Model Finding for Recursive Functions in SMT
article
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. ⟨10.1007/978-3-319-40229-1_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01336082/file/conf.pdf BibTex
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
BibTex
auteur
Thomas Sturm, Erika Ábrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler
titre
SC2: Satisfiability Checking Meets Symbolic Computation (Project Paper)
article
Proc. CICM 2016, Jul 2016, Bialystok, Poland. pp.28 – 43, ⟨10.1007/978-3-319-42547-4⟩
Accès au bibtex
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
https://hal.inria.fr/hal-01403206/file/paar.pdf 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
BibTex

Directions of work or proceedings

auteur
Jasmin Christian Blanchette, Stephan Merz
titre
Interactive Theorem Proving
article
Nancy, France. 9807, Springer, 2016, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-43144-4⟩
Accès au bibtex
BibTex

2015

Journal articles

auteur
Paolo Ballarini, Marie Duflot
titre
Applications of an expressive statistical model checking approach to the analysis of genetic circuits
article
Theoretical Computer Science, Elsevier, 2015, 599, pp.30. ⟨10.1016/j.tcs.2015.05.018⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01250521/file/TCS_CMSB12.pdf BibTex
auteur
Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
titre
HASL: A new approach for performance evaluation and model checking from concepts to experimentation
article
Performance Evaluation, Elsevier, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01221815/file/main.pdf BibTex
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, Andreas Weber
titre
Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
article
Journal of Computational Physics, Elsevier, 2015, 291, pp.279-302. ⟨10.1016/j.jcp.2015.02.050⟩
Accès au bibtex
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
BibTex
auteur
Haniel Barbosa, Pascal Fontaine
titre
Congruence Closure with Free Variables (Work in Progress)
article
Quantify 2015 : 2nd International Workshop on Quantification, 2015, Berlin, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246036/file/BarbosaFontaine-QUANTIFY2015.pdf 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
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
https://hal.inria.fr/hal-01212594/file/paper.pdf 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
https://hal.inria.fr/hal-01212589/file/fouco.pdf 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
https://hal.inria.fr/hal-01212587/file/wit.pdf 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
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
https://hal.inria.fr/hal-01206187/file/ds-bridging.pdf 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
https://hal.inria.fr/hal-01157898/file/bridging-nd-compact.pdf 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
https://hal.inria.fr/hal-01305026/file/paper.pdf 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
https://hal.inria.fr/hal-01154767/file/When%20sharing%20computer%20science%20with%20everyone%20also%20helps%20avoiding%20digital%20prejudices%20%281%29.pdf 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
https://hal.archives-ouvertes.fr/hal-01097204/file/paper.pdf 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
https://hal.inria.fr/hal-01240343/file/article.pdf BibTex
auteur
Dominique Méry, Neeraj Kumar Singh
titre
Analyzing Requirements Using Environment Modelling
article
Digital Human Modeling – Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health – 6th International Conference, DHM 2015, Aug 2015, Los Angeles, United States
Accès au bibtex
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
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
https://hal.inria.fr/hal-01238377/file/plm-iticse-HAL.pdf BibTex
auteur
Andrew Reynolds, Jasmin Christian Blanchette
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
article
CADE-25, Aug 2015, Berlin, Germany. ⟨10.1007/978-3-319-21401-6_13⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212585/file/conf.pdf BibTex
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli
titre
Model Finding for Recursive Functions in SMT
article
SMT Workshop 2015, Jul 2015, San Francisco, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242509/file/shortv.pdf 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
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
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
https://hal.inria.fr/hal-01127966/file/main.pdf 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
BibTex

Directions of work or 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
BibTex
auteur
Catherine Dubois, Paolo Masci, Dominique Méry
titre
Second International Workshop on Formal Integrated Development Environment
article
Jun 2015, France. EPTCS, 2015, EPTCS ⟨10.4204/EPTCS.187⟩
Accès au bibtex
BibTex
auteur
Pascal Fontaine, Thomas Sturm, Uwe Waldmann
titre
Foreword to the Special Focus on Constraints and Combinations
article
Dongming Wang. Switzerland. 9 (3), Springer, 2015, Mathematics in Computer Science, ⟨10.1007/s11786-015-0239-8⟩
Accès au bibtex
BibTex

Other publications

auteur
Marek Kosta, Thomas Sturm
titre
A Generalized Framework for Virtual Substitution
article
2015, pp.17
Accès au bibtex
https://arxiv.org/pdf/1501.05826 BibTex
auteur
Marco Voigt, Christoph Weidenbach
titre
Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
article
2015
Accès au bibtex
https://arxiv.org/pdf/1501.07209 BibTex

Reports

auteur
Haniel Barbosa, Pascal Fontaine
titre
Congruence Closure with Free Variables (Work in Progress)
article
[Research Report] Inria Nancy – Grand Est (Villers-lès-Nancy, France). 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01235912/file/main.pdf BibTex

Theses

auteur
Manamiary Bruno Andriamiarina
titre
Développement d’algorithmes répartis corrects par construction
article
Modélisation et simulation. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0181⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01752149/file/these-Andriamiarina-Manamiary-Bruno.pdf BibTex
auteur
Marion Guthmuller
titre
Vérification dynamique formelle de propriétés temporelles sur des applications distribuées réelles
article
Informatique [cs]. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0090⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01751786/file/manuscrit.pdf https://tel.archives-ouvertes.fr/tel-01751786/file/annexe-soutenance.pdf BibTex

Preprints, Working Papers, …

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
https://hal.inria.fr/hal-01558049/file/journal.pdf BibTex
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
titre
Better Answers to Real Questions
article
2015
Accès au bibtex
https://arxiv.org/pdf/1501.05098 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
https://hal.inria.fr/hal-01244627/file/sets2015.pdf 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, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. ⟨http://www.comsis.org/archive.php?show=pprpdcat1⟩. ⟨10.2298/CSIS130122007A⟩
Accès au bibtex
BibTex
auteur
Myrto Arapinis, Marie Duflot
titre
Bounding messages for free in security protocols – extension to various security properties
article
Information and Computation, Elsevier, 2014, pp.34. ⟨10.1016/j.ic.2014.09.003⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01083657/file/versionjournal.pdf BibTex
auteur
Christopher W. Brown, Marek Kosta
titre
Constructing a single cell in cylindrical algebraic decomposition
article
Journal of Symbolic Computation, Elsevier, 2014, pp.35. ⟨http://dx.doi.org/10.1016/j.jsc.2014.09.024⟩
Accès au bibtex
BibTex
auteur
Jingshu Chen, Marie Duflot, Stephan Merz
titre
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
article
Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14. ⟨http://journal.ub.tu-berlin.de/eceasst/article/view/978⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087871/file/postproceedings.pdf BibTex
auteur
David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
titre
Integrating SMT solvers in Rodin
article
Science of Computer Programming, Elsevier, 2014, Abstract State Machines, Alloy, B, VDM, and Z — Selected and extended papers from ABZ 2012, 94, pp.14
Accès au bibtex
BibTex
auteur
Marek Kosta, Pavol Duris
titre
Flip-Pushdown Automata with k Pushdown Reversals and E0L Systems are Incomparable
article
Information Processing Letters, Elsevier, 2014, 114 (8), pp.417-420
Accès au bibtex
BibTex
auteur
Manuel Lamotte-Schubert, Christoph Weidenbach
titre
BDI: a new decidable clause class
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (6), pp.28. ⟨http://logcom.oxfordjournals.org/content/early/2014/12/08/logcom.exu074⟩
Accès au bibtex
BibTex
auteur
Gerald Lüttgen, Stephan Merz
titre
Editorial: Special Issue of Automated Verification of Critical Systems
article
Science of Computer Programming, Elsevier, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
Accès au bibtex
BibTex
auteur
Dominique Méry, Bernhard Schätz, Alan Wassyng
titre
The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
article
Dagstuhl Reports, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2014, 4 (2), pp.17–37
Accès au bibtex
BibTex

Conference papers

auteur
Yamine Aït Ameur, J. Paul Gibson, Dominique Méry
titre
On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
article
Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications – 6th International Symposium,, Tiziana Margaria and Bernhard Steffen, Oct 2014, Corfu, Greece. pp.604-618
Accès au bibtex
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
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
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
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
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
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 – Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf BibTex
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
article
Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. pp.1-16
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf 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
BibTex
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
titre
Towards Conflict-Driven Learning for Virtual Substitution
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Philipp Rümmer and Christoph M. Wintersteiger, Jul 2014, Vienna, Austria
Accès au bibtex
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
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
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
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
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
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
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
https://hal.inria.fr/hal-01098078/file/draft.pdf 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
BibTex

Directions of work or 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%2F978-3-319-10882-7⟩
Accès au bibtex
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⟩. ⟨http://link.springer.com/book/10.1007%2F978-3-319-08587-6⟩
Accès au bibtex
BibTex
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. France. 149, EPTCS, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/EPTCS.149⟩
Accès au bibtex
BibTex
auteur
Gerald Lüttgen, Stephan Merz
titre
Science of Computer Programming Special Issue: Automated Verification of Critical Systems
article
Netherlands. 96 (3), Elsevier, 2014, Science of Computer Programming
Accès au bibtex
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
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
https://hal.inria.fr/hal-01018162/file/paperv1.pdf 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
https://hal.inria.fr/hal-00985135/file/RR-8529.pdf 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
https://hal.inria.fr/tel-01751181/file/thesis.pdf 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), ACM, 2013, 12 (1), pp.15. ⟨10.1145/2406336.2406351⟩
Accès au bibtex
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
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
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
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
BibTex
auteur
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
titre
Computing prime implicant
article
FMCAD – Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. pp.46-52
Accès au bibtex
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
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
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
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
https://hal.inria.fr/hal-00904817/file/submission.pdf 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
https://hal.inria.fr/hal-00904796/file/final.pdf 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
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
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
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
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
BibTex

Directions of work or proceedings

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. 3, Dagstuhl, pp.16, 2013, Dagstuhl Reports, ⟨10.4230/DagRep.3.4.1⟩
Accès au bibtex
BibTex
auteur
Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
titre
Frontiers of Combining Systems
article
Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. 8152, Springer, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
Accès au bibtex
BibTex

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, Elsevier, 2012, 77 (10-11), pp.1122-1150
Accès au bibtex
BibTex

Conference papers

auteur
Yamine Ait 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
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
https://hal.inria.fr/hal-00734131/file/pdcat2012v14.pdf 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
https://hal.inria.fr/hal-00763092/file/iwmcsv5.pdf 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
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
https://hal.inria.fr/hal-00726631/file/final.pdf 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
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
https://hal.inria.fr/hal-00768812/file/paper.pdf 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
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
https://hal.inria.fr/hal-00760579/file/avocs2012.pdf 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
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
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
BibTex
auteur
Stephan Merz
titre
Stuttering Equivalence
article
[Research Report] 2012
Accès au bibtex
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
https://tel.archives-ouvertes.fr/tel-01749162/file/ThA_se-Sabina_AKHTAR.pdf BibTex

 

Comments are closed.