Publications HAL du labo/EPI 107895

2017

titre
Satisfiability Modulo Bounded Checking
auteur
Simon Cruanes
article
International Conference on Automated Deduction (CADE), Aug 2017, Gothenburg, Sweden. 26, pp.114-129, 2017, 〈10.1007/978-3-319-63046-5_8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01572531/file/paper.pdf BibTex
titre
Subtropical Satisfiability
auteur
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Vu
article
Clare Dixon and Marcelo Finger. Frontiers of Combining Systems (FroCoS), 2017, Brazilia, Brazil. Springer, 10483, pp.481 - 206, 2017, 〈10.1007/978-3-642-17511-4_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590899/file/Fontaine17.pdf BibTex
titre
Congruence Closure with Free Variables
auteur
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
article
Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2017, Uppsala, Sweden. 205, pp.220 - 230, 2017, 〈10.1007/10721959_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590918/file/Barbosa1.pdf BibTex
titre
Scalable Fine-Grained Proofs for Formula Processing
auteur
Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine
article
Proc. Conference on Automated Deduction (CADE), 2017, Gotenburg, Sweden. 228, pp.140 - 412, 2017, 〈10.1007/978-3-642-02959-2_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01590922/file/Barbosa2.pdf BibTex
titre
A Formal Proof of the Expressiveness of Deep Learning
auteur
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
article
ITP 2017: 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. 〈10.1007/3-540-48256-3_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599172/file/paper.pdf BibTex
titre
Foundational nonuniform (Co)datatypes for higher-order logic
auteur
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
article
LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005071〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599174/file/conf.pdf BibTex
titre
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
auteur
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
article
FSCD 2017: 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. 11, pp.1 - 11, 〈10.4230/LIPIcs.FSCD.2017.11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599176/file/paper.pdf BibTex
titre
On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic
auteur
Matthias Horbach, Marco Voigt, Christoph Weidenbach
article
Leonardo de Moura. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.77-94, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_6〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592160/file/HorbachVoigtWeidenbachCADE.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
auteur
Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach
article
Carles Sierra. 26th International Joint Conference on Artificial Intelligence, Aug 2017, Melbourne, Australia. pp.4786-4790, 〈10.24963/ijcai.2017/667〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592164/file/BlanchetteFleuryWeidenbachIJCAI.pdf BibTex
titre
The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable
auteur
Marco Voigt
article
Clare Dixon and Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.244-261, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592169/file/VoigtFroCoS.pdf BibTex
titre
A fine-grained hierarchy of hard problems in the separated fragment
auteur
Marco Voigt
article
Joël Ouaknine. LICS 2017 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. IEEE Computer Society, pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005094〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592172/file/VoigtLICS.pdf BibTex
titre
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
auteur
Matthias Horbach, Marco Voigt, Christoph Weidenbach
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592177/file/HorbachVoigtWeidenbachCoRR.pdf BibTex
titre
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
auteur
Heiko Becker, Jasmin Blanchette, Uwe Waldmann, Daniel Wand
article
Leonardo de Moura. CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.432-453, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592186/file/BeckerBlanchetteWaldmannWandCADE.pdf BibTex
titre
A Lambda-Free Higher-Order Recursive Path Order
auteur
Jasmin Blanchette, Uwe Waldmann, Daniel Wand
article
Javier Esparza and Andrzej S. Murawski. Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. Springer, 10203, pp.461-479, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-662-54458-7_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592189/file/BlanchetteWaldmannWandFoSSaCS.pdf BibTex
titre
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
auteur
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
article
Clare Dixon and Marcelo Finger. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.3-21, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01592196/file/BiendarraBlanchetteEtAl-FroCos.pdf BibTex
titre
Scalable Fine-Grained Proofs for Formula Processing
auteur
Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine
article
[Research Report] Universite de Lorraine, CNRS, Inria, LORIA, Nancy, France; Universidade Federal do Rio Grande do Norte, Natal, Brazil; Vrije Universiteit Amsterdam, Amsterdam, The Netherlands; Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2017, pp.25
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01526841/file/rep.pdf BibTex
titre
Automated Verification of Security Chains in Software-Defined Networks with Synaptic
auteur
Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
article
NetSoft 2017 - IEEE Conference on Network Softwarization, Jul 2017, Bologna, Italy. IEEE Computer Society, pp.1-9, 2017, 〈10.1109/NETSOFT.2017.8004195〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630806/file/camera-ready.pdf BibTex
titre
Satisfiability techniques for computing minimal tie sets in reliability assessment
auteur
Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
article
10th International Conference on Mathematical Methods in Reliability, MMR 2017, Jul 2017, Grenoble, France. pp.1-8, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630851/file/resubmission-Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf BibTex
titre
Contextualization and Dependency in State-Based Modelling - Application to Event-B
auteur
Dominique Méry, Souad Kherroubi
article
MEDI 2017 - International Conference on Model and Data Engineering, Oct 2017, Barcelona, Spain. Springer, 10563, pp.137--152, 2017, Lecture Notes in Computer Science. 〈http://dblp.org/rec/bib/conf/medi/KherroubiM17〉. 〈10.1007/978-3-319-66854-3_11〉
Accès au bibtex
BibTex
titre
Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
auteur
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
article
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Apr 2017, Uppsala, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01599167/file/conf.pdf BibTex
titre
Auxiliary Variables in TLA+
auteur
Leslie Lamport, Stephan Merz
article
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01488617/file/auxiliary.pdf BibTex
titre
Satisfiability techniques for computing minimal tie sets in reliability assessment
auteur
Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01518920/file/Techreport%20-%20Satisfiability%20techniques%20for%20computing%20minimal%20tie%20sets%20in%20reliability%20assessment.pdf BibTex
titre
Congruence Closure with Free Variables
auteur
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
article
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01442691/file/main.pdf BibTex

2016

titre
On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin
auteur
Dominique Méry, Rosemary Monahan, Cheng Zheng
article
Bernhard Steffen and Tiziana Margaria. ISOLA 2016 , Oct 2016, CORFU, Greece. Springer, I (9952), pp.18, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_57〉
Accès au bibtex
BibTex
titre
Model Finding for Recursive Functions in SMT
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
article
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. 〈10.1007/978-3-319-40229-1_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01336082/file/conf.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
auteur
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
article
8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. 2016, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. 〈10.1007/978-3-319-40229-1_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01336074/file/main.pdf BibTex
titre
Better answers to real questions
auteur
Marek Košta, Thomas Sturm, Andreas Dolzmann
article
Journal of Symbolic Computation, Elsevier, 2016, 74, pp.255 - 275. 〈10.1016/j.jsc.2015.07.002〉
Accès au bibtex
BibTex
titre
SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)
auteur
Eriká Abrahám, John Abbott, Bernd Becker, Anna Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner Seiler, Thomas Sturm
article
Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland. 〈http://www.cicm-conference.org/2016/cicm.php〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377655/file/SCSC-CICM16.pdf BibTex
titre
Making explicit domain knowledge in formal system development
auteur
Yamine Ait Ameur, Dominique Méry
article
Science of Computer Programming, Elsevier, 2016, 121 (100--127), 〈ELSEVIER〉. 〈10.1016/j.scico.2015.12.004〉
Accès au bibtex
BibTex
titre
Fast Cube Tests for LIA Constraint Solving
auteur
Martin Bromberger, Christoph Weidenbach
article
Nicola Olivetti and Ashish Tiwari. Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. Springer, 9706, pp.116-132, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-40229-1_9〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403200/file/IJCAR2016.pdf BibTex
titre
Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
auteur
Martin Bromberger, Christoph Weidenbach
article
Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. 1617, pp.15-30, 2016, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403214/file/SMT2016.pdf BibTex
titre
Ensuring Correctness of Model Transformations While Remaining Decidable
auteur
Jon Haël Brenas, Rachid Echahed, Martin Strecker
article
Theoretical Aspects of Computing - ICTAC, Oct 2016, Taipei, Taiwan. pp.315 - 332, 2016, Theoretical Aspects of Computing – ICTAC 2016 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings. 〈10.1007/978-3-319-46750-4_18〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01403585/file/paper61-procversion.pdf BibTex
titre
Compliance, Functional Safety and Fault Detection by Formal Methods
auteur
Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski
article
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016), 2016, Corfu, Greece. Springer, 9953, pp.626 - 632, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-47169-3_48〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403190/file/mypaper.pdf BibTex
titre
Ordered Resolution with Straight Dismatching Constraints
auteur
Andreas Teucke, Christoph Weidenbach
article
Pascal Fontaine and Stephan Schulz and Josef Urban. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, Coimbra, Portugal. 1635, pp.95-109, 2016, CEUR Workshop Proceedings
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01403206/file/paar.pdf BibTex
titre
A Learning-Based Fact Selector for Isabelle/HOL
auteur
Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57, pp.219 - 244. 〈10.1007/s10817-016-9362-8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386986/file/paper.pdf BibTex
titre
Semi-intelligible Isar Proofs from Machine-Generated Proofs
auteur
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
article
Journal of Automated Reasoning, Springer Verlag, 2016, 〈10.1007/s10817-015-9335-3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01211748/file/paper.pdf BibTex
titre
Friends with Benefits
auteur
Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
article
Isabelle Workshop 2016, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401812/file/amico_abs.pdf BibTex
titre
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)
auteur
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
article
Isabellle Workshop 2016, Aug 2016, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401807/file/sat_abs.pdf BibTex
titre
Extending Nunchaku to Dependent Type Theory
auteur
Simon Cruanes, Jasmin Blanchette
article
Hammers for Type Theories (HaTT 2016), Jul 2016, Coimbra, Portugal. EPTCS, 210, pp.3 - 12, 2016, Proceedings First International Workshop on Hammers for Type Theories 〈http://eptcs.web.cse.unsw.edu.au/content.cgi?HaTT2016〉. 〈10.4204/EPTCS.210.3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01401696/file/nunchaku_tt.pdf BibTex
titre
Interactive Theorem Proving
auteur
Jasmin Christian Blanchette, Stephan Merz
article
Nancy, France. 9807, Springer, 2016, Lecture Notes in Computer Science, 〈10.1007/978-3-319-43144-4〉
Accès au bibtex
BibTex
titre
A Rigorous Correctness Proof for Pastry
auteur
Noran Azmy, Stephan Merz, Christoph Weidenbach
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.86-101, 2016, 〈10.1007/978-3-319-33600-8_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322342/file/Main.pdf BibTex
titre
Encoding TLA+ into Many-Sorted First-Order Logic
auteur
Stephan Merz, Hernán Vanzetto
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. Springer, 9675, pp.54-69, 2016, 〈10.1007/978-3-319-33600-8_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322328/file/tla2smt.pdf BibTex
titre
Proving Determinacy of the PharOS Real-Time Operating System
auteur
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. Springer, 9675, pp.70-85, 2016, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-33600-8_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322335/file/final.pdf BibTex
titre
Hammering towards QED
auteur
Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, Josef Urban
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (1), pp.101-148
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01386988/file/h4qed-clean.pdf BibTex
titre
Incremental Proof-Based Development for Resilient Distributed Systems
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Trustworthy Cyber-Physical Systems Engineering, Taylor and Francis Group, 2016, Trustworthy Cyber-Physical Systems Engineering
Accès au bibtex
BibTex
titre
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
auteur
Thomas Sturm, Marco Voigt, Christoph Weidenbach
article
LICS 2016, Jul 2016, New York, United States. pp.86 - 95, 2016, 〈10.1145/2933575.2934532〉
Accès au bibtex
BibTex
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
auteur
Andrew Reynolds, Jasmin Blanchette
article
IJCAI 2016, Jul 2016, New York City, United States. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01397082/file/sister.pdf BibTex
titre
Playing with State-Based Models for Designing Better Algorithms
auteur
Dominique Méry
article
Future Generation Computer Systems, Elsevier, 2016, pp.25. 〈ELSEVIER〉
Accès au bibtex
BibTex
titre
Editorial
auteur
Stephan Merz, Jun Pang
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. 〈10.1007/s00165-016-0390-2〉
Accès au bibtex
BibTex
titre
Editorial
auteur
Stephan Merz, Jun Pang
article
Formal Aspects of Computing, Springer Verlag, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. 〈10.1007/s00165-016-0390-2〉
Accès au bibtex
BibTex

2015

titre
System-Level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
auteur
Marion Guthmuller, Gabriel Corona, Martin Quinson
article
2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01558049/file/journal.pdf BibTex
titre
Encoding TLA+ set theory into many-sorted first-order logic
auteur
Stephan Merz, Hernán Vanzetto
article
2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244627/file/sets2015.pdf BibTex
titre
Vérification dynamique formelle de propriétés temporelles sur des applications distribuées réelles
auteur
Marion Guthmuller
article
Informatique [cs]. Université de Lorraine, 2015. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01231868/file/manuscrit.pdf https://tel.archives-ouvertes.fr/tel-01231868/file/annexe-soutenance.pdf BibTex
titre
Linear Integer Arithmetic Revisited
auteur
Martin Bromberger, Thomas Sturm, Christoph Weidenbach
article
25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. Springer, 9195, pp.623-637
Accès au bibtex
BibTex
titre
Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
auteur
Marco Voigt, Christoph Weidenbach
article
preprint. 2015
Accès au bibtex
https://arxiv.org/pdf/1501.07209 BibTex
titre
Automated Reasoning Building Blocks
auteur
Christoph Weidenbach
article
Roland Meyer and André Platzer and Heike Wehrheim. Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog, 9360, Springer, pp.172-188, 2015, 〈10.1007/978-3-319-23506-6_12〉
Accès au bibtex
BibTex
titre
Subtropical Real Root Finding
auteur
Thomas Sturm
article
Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, Jul 2015, Bath, United Kingdom
Accès au bibtex
BibTex
titre
A Generalized Framework for Virtual Substitution
auteur
Marek Kosta, Thomas Sturm
article
preprint. 2015, pp.17
Accès au bibtex
https://arxiv.org/pdf/1501.05826 BibTex
titre
Foreword to the Special Focus on Constraints and Combinations
auteur
Pascal Fontaine, Thomas Sturm, Uwe Waldmann
article
Dongming Wang. Switzerland. 9 (3), Springer, 2015, Mathematics in Computer Science, 〈10.1007/s11786-015-0239-8〉
Accès au bibtex
BibTex
titre
Congruence Closure with Free Variables (Work in Progress)
auteur
Haniel Barbosa, Pascal Fontaine
article
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France). 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01235912/file/main.pdf BibTex
titre
Software Component Design with the B Method — A Formalization in Isabelle/HOL
auteur
David Déharbe, Stephan Merz
article
Christiano Braga and Peter Csaba Ölveczky. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. Springer, 9539, pp.31-47, 2016, 〈10.1007/978-3-319-28934-2_2〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01305026/file/paper.pdf BibTex
titre
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction, CADE-25, Aug 2015, Berlin, Germany. Springer, 9195, pp.419-433, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_29〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01157898/file/bridging-nd-compact.pdf BibTex
titre
A Rewriting Approach to the Combination of Data Structures with Bridging Theories
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.275--290, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01206187/file/ds-bridging.pdf BibTex
titre
Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, Andreas Weber
article
Journal of Computational Physics, Elsevier, 2015, 291, pp.279-302. 〈10.1016/j.jcp.2015.02.050〉
Accès au bibtex
BibTex
titre
Modal Satisfiability via SMT Solving
auteur
Carlos Areces, Pascal Fontaine, Stephan Merz
article
Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, 〈10.1007/978-3-319-15545-6_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01127966/file/main.pdf BibTex
titre
Applications of an expressive statistical model checking approach to the analysis of genetic circuits
auteur
Paolo Ballarini, Marie Duflot
article
Journal of Theoretical Computer Science (TCS), Elsevier, 2015, 599, pp.30. 〈10.1016/j.tcs.2015.05.018〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01250521/file/TCS_CMSB12.pdf BibTex
titre
Beagle – A Hierarchic Superposition Prover
auteur
Peter Baumgartner, Joshua Bax, Uwe Waldmann
article
Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. Springer, 9195, pp.367-377, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_25〉
Accès au bibtex
BibTex
titre
Modal Tableau Systems with Blocking and Congruence Closure
auteur
Renate Schmidt, Uwe Waldmann
article
de Nivelle, Hans. 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wroclaw, Poland. Springer, 9323, pp.38-53, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24312-2_4〉
Accès au bibtex
BibTex
titre
HASL: A new approach for performance evaluation and model checking from concepts to experimentation
auteur
Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin
article
Performance Evaluation, Elsevier, 2015, 90, pp.53-77. 〈10.1016/j.peva.2015.04.003〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01221815/file/main.pdf BibTex
titre
A Teaching System To Learn Programming: the Programmer's Learning Machine
auteur
Martin Quinson, Gérald Oster
article
ACM Conference on Innovation and Technology in Computer Science Education 2015, Jul 2015, Vilnius, Lithuania. ACM, 〈http://www.iticse2015.mii.vu.lt/〉. 〈10.1145/2729094.2742626〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238377/file/plm-iticse-HAL.pdf BibTex
titre
Développement d'algorithmes répartis corrects par construction
auteur
Manamiary Bruno Andriamiarina
article
Modélisation et simulation. Université de Lorraine; Loria & Inria Grand Est, 2015. Français
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01258363/file/these-Andriamiarina-Manamiary-Bruno.pdf BibTex
titre
Mining the Archive of Formal Proofs
auteur
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow
article
CICM 2015, Jul 2015, Washington DC, United States. Lecture Notes in Computer Science, 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 〈10.1007/978-3-319-20615-8_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212594/file/paper.pdf BibTex
titre
A Decision Procedure for (Co)datatypes in SMT Solvers
auteur
Andrew Reynolds, Jasmin Christian Blanchette
article
CADE-25, Aug 2015, Berlin, Germany. Lecture Notes in Computer Science, 2015, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. 〈10.1007/978-3-319-21401-6_13〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212585/file/conf.pdf BibTex
titre
Witnessing (Co)datatypes
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
article
ESOP 2015, Apr 2015, London, United Kingdom. Lecture Notes in Computer Science, 2015, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 〈10.1007/978-3-662-46669-8_15〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212587/file/wit.pdf BibTex
titre
Foundational Extensible Corecursion: A Proof Assistant Perspective
auteur
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
article
ICFP 2015, Aug 2015, Vancouver, Canada. 2015, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. 〈10.1145/2784731.2784732〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01212589/file/fouco.pdf BibTex
titre
Model Finding for Recursive Functions in SMT
auteur
Andrew Reynolds, Jasmin Christian Blanchette, Cesare Tinelli
article
SMT Workshop 2015, Jul 2015, San Francisco, United States. 2015, 〈http://smt2015.csl.sri.com〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242509/file/shortv.pdf BibTex
titre
Analyzing Requirements Using Environment Modelling
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference, DHM 2015, Aug 2015, Los Angeles, United States. Springer, Lecture Notes in Computer Science 9185,, 2015, Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference, DHM 2015, Held as Part of HCI International 2015,. 〈http://link.springer.com/book/10.1007%2F978-3-319-21070-4〉
Accès au bibtex
BibTex
titre
Adapting Real Quantifier Elimination Methods for Conflict Set Computation
auteur
Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
article
Carsten Lutz; Silvio Ranise. Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. Springer, 9322, pp.151-166, 2015, LNCS. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_10〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240343/file/article.pdf BibTex
titre
Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study
auteur
Dominique Méry, Sawant Rushikesh, Anton Tarasyuk
article
Ladjel Bellatreche; Yannis Manolopoulos. Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. springer, lncs 9344, pp.89-102, 2015, Model and Data Engineering - 5th International Conference, MEDI 2015. 〈http://link.springer.com/book/10.1007%2F978-3-319-23781-7〉
Accès au bibtex
BibTex
titre
Congruence Closure with Free Variables (Work in Progress)
auteur
Haniel Barbosa, Pascal Fontaine
article
Quantify 2015 : 2nd International Workshop on Quantification, 2015, Berlin, Germany. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246036/file/BarbosaFontaine-QUANTIFY2015.pdf BibTex
titre
Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
auteur
Dominique Méry, Mike Poppleton
article
Software and Systems Modeling (SoSyM), Springer, 2015
Accès au bibtex
BibTex
titre
Second International Workshop on Formal Integrated Development Environment
auteur
Catherine Dubois, Paolo Masci, Dominique Méry
article
Jun 2015, France. EPTCS, 2015, EPTCS 〈10.4204/EPTCS.187〉
Accès au bibtex
BibTex
titre
System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications
auteur
Marion Guthmuller, Martin Quinson, Gabriel Corona
article
Formal Approaches to Parallel and Distributed Systems (4PAD) - Special Session of Parallel, Distributed and network-based Processing (PDP), Mar 2015, Turku, Finland. 2015
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01097204/file/paper.pdf BibTex
titre
{NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment
auteur
Gábor Alagi, Christoph Weidenbach
article
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), 2015, Wroclaw, Poland. Springer, Lecture Notes in Computer Science, 9322, pp.69-84, 〈10.1007/978-3-319-24246-0_5〉
Accès au bibtex
BibTex
titre
Better Answers to Real Questions
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
article
2015
Accès au bibtex
https://arxiv.org/pdf/1501.05098 BibTex
titre
When sharing computer science with everyone also helps avoiding digital prejudices.
auteur
Marie Duflot, Martin Quinson, Florent Masseglia, Didier Roy, Julien Vaubourg, Thierry Viéville
article
Scratch2015AMS, Aug 2015, Amsterdam, Netherlands. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01154767/file/When%20sharing%20computer%20science%20with%20everyone%20also%20helps%20avoiding%20digital%20prejudices%20%281%29.pdf BibTex

2014

titre
BDI: a new decidable clause class
auteur
Manuel Lamotte-Schubert, Christoph Weidenbach
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (6), pp.28. 〈http://logcom.oxfordjournals.org/content/early/2014/12/08/logcom.exu074〉
Accès au bibtex
BibTex
titre
Proofs in satisfiability modulo theories
auteur
Clark Barrett, Leonardo De Moura, Pascal Fontaine
article
APPA (All about Proofs, Proofs for All), Jul 2014, Vienna, Austria. 2014
Accès au bibtex
BibTex
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
Christoph Benzmüller and Jens Otten. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. 33, pp.1-16, 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf BibTex
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf BibTex
titre
Refinement Types for TLA+
auteur
Stephan Merz, Hernán Vanzetto
article
Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp.143-157, 2014, LNCS. 〈10.1007/978-3-319-06200-6_11〉
Accès au bibtex
BibTex
titre
Science of Computer Programming Special Issue: Automated Verification of Critical Systems
auteur
Gerald Lüttgen, Stephan Merz
article
Netherlands. 96 (3), Elsevier, 2014, Science of Computer Programming
Accès au bibtex
BibTex
titre
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
auteur
Jingshu Chen, Marie Duflot, Stephan Merz
article
Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14. 〈http://journal.ub.tu-berlin.de/eceasst/article/view/978〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087871/file/postproceedings.pdf BibTex
titre
Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Jul 2014, Vienna, Austria
Accès au bibtex
BibTex
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. Springer, 8562, pp.122-136, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08587-6_9〉
Accès au bibtex
BibTex
titre
Proceedings 1st Workshop on Formal Integrated Development Environment
auteur
Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry
article
Catherine Dubois; Dimitra Giannakopoulou; Dominique Méry. France. 149, EPTCS, pp.105, 2014, Electronic Proceedings in Theoretical Computer Science, 〈10.4204/EPTCS.149〉
Accès au bibtex
BibTex
titre
Constructing a single cell in cylindrical algebraic decomposition
auteur
Christopher W. Brown, Marek Kosta
article
Journal of Symbolic Computation, Elsevier, 2014, pp.35. 〈http://dx.doi.org/10.1016/j.jsc.2014.09.024〉
Accès au bibtex
BibTex
titre
A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)
auteur
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
article
[Research Report] RR-8529, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00985135/file/RR-8529.pdf BibTex
titre
Modeling an Aircraft Landing System in Event-B
auteur
Dominique Méry, Neeraj Kumar Singh
article
Frédéric Boniol. ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. Springer, 433, pp.154-159, 2014, CCIS
Accès au bibtex
BibTex
titre
Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Computer Science and Information Systems, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. 〈http://www.comsis.org/archive.php?show=pprpdcat1〉. 〈10.2298/CSIS130122007A〉
Accès au bibtex
BibTex
titre
Editorial: Special Issue of Automated Verification of Critical Systems
auteur
Gerald Lüttgen, Stephan Merz
article
Science of Computer Programming, Elsevier, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
Accès au bibtex
BibTex
titre
Integrating SMT solvers in Rodin
auteur
David Déharbe, Pascal Fontaine, Laurent Voisin, Yoann Guyot
article
Science of Computer Programming, Elsevier, 2014, Abstract State Machines, Alloy, B, VDM, and Z — Selected and extended papers from ABZ 2012, 94, pp.14
Accès au bibtex
BibTex
titre
Event B (english version)
auteur
Neeraj Kumar Singh, Dominique Méry
article
Jean-Louis Boulanger. Formal Methods Applied to Complex Systems, Wiley, 2014, Formal Methods Applied to Complex Systems, 9781119002727. 〈10.1002/9781119002727.ch10〉
Accès au bibtex
BibTex
titre
Analysis of Self-* and P2P Systems using Refinement (Full Report)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
[Research Report] 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01018162/file/paperv1.pdf BibTex
titre
Analysis of Self-* and P2P Systems using Refinement
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
Yamine AIT AMEUR and Klaus-Dieter SCHEWE. ABZ 2014 - 4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z, Jun 2014, Toulouse, France. Springer, 8477, pp.117-123, 2014, LNCS. 〈10.1007/978-3-662-43652-3_9〉
Accès au bibtex
BibTex
titre
Towards Conflict-Driven Learning for Virtual Substitution
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
article
Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov. Computer Algebra in Scientific Computing - 16th International Workshop, CASC 2014, 2014, Warsaw, Poland. Springer, 8660, pp.256-270, 2014, Lecture Notes in Computer Science. 〈http://dx.doi.org/10.1007/978-3-319-10515-4_19〉
Accès au bibtex
BibTex
titre
Better Answers to Real Questions
auteur
Marek Kosta, Thomas Sturm, Andreas Dolzmann
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Jul 2014, Vienna, Austria. pp.69, CEUR Workshop Proceedings
Accès au bibtex
BibTex
titre
Towards Conflict-Driven Learning for Virtual Substitution
auteur
Konstantin Korovin, Marek Kosta, Thomas Sturm
article
12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Jul 2014, Vienna, Austria. CEUR Workshop Proceedings
Accès au bibtex
BibTex
titre
Finite Quantification in Hierarchic Theorem Proving
auteur
Peter Baumgartner, Joshua Bax, Uwe Waldmann
article
Stéphane Demri and Deepak Kapur and Christoph Weidenbach. 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. Springer, 8562, pp.152-167, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
The Semantics of Refinement Chart
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. HCI International, Jun 2014, Heraklion, Greece. Springer, 8529, pp.415-426, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-07725-3_42〉
Accès au bibtex
BibTex
titre
Proof automation and type synthesis for set theory in the context of TLA+
auteur
Hernán Vanzetto
article
Computer Science [cs]. Université de Lorraine, 2014. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01096518/file/thesis.pdf BibTex
titre
Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014)
auteur
Stephan Merz, Jun Pang
article
Stephan Merz; Jun Pang. 16th International Conference on Formal Engineering Methods - ICFEM 2014, Nov 2014, Luxembourg, Luxembourg. 8829, Springer, pp.460, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-11737-9. 〈10.1007/978-3-319-11737-9〉
Accès au bibtex
BibTex
titre
Polymorphic+Typeclass Superposition
auteur
Daniel Wand
article
Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01098078/file/draft.pdf BibTex
titre
Formal Evaluation of Landing Gear System
auteur
Dominique Méry, Neeraj Kumar Singh
article
Ngo Hong Son; Yves Deville; Marc Bui. SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam. ACM, 2014, SoICT 2014 fifth symposium on Information and Communication Technology
Accès au bibtex
BibTex
titre
Theoretical Aspects of Computing – ICTAC 2014
auteur
Gabriel Ciobanu, Dominique Méry
article
Gabriel Ciobanu; Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, Sep 2014, Bucharest, Romania. 8687, Springer, 2014, Lecture Notes in Computer Science, 〈10.1007%2F978-3-319-10882-7〉
Accès au bibtex
BibTex
titre
Automated Reasoning – Seventh International Joint Conference (IJCAR 2014)
auteur
Stéphane Demri, Deepak Kapur, Christoph Weidenbach
article
Stéphane Demri; Deepak Kapur; Christoph Weidenbach. 7th International Joint Conference - IJCAR 2014, Jun 2014, Vienna, Austria. 8562, Springer, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-08586-9. 〈10.1007/978-3-319-08587-6〉. 〈http://link.springer.com/book/10.1007%2F978-3-319-08587-6〉
Accès au bibtex
BibTex
titre
On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems
auteur
Yamine Aït Ameur, J. Paul Gibson, Dominique Méry
article
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium,, Oct 2014, Corfu, Greece. Springer, 8803, pp.604-618, 2014, Lectures Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉
Accès au bibtex
BibTex
titre
Playing with State-Based Models for Designing Better Algorithms
auteur
Dominique Méry
article
Yamine Aït Ameur; Ladjel Bellatreche; George A. Papadopoulos. Model and Data Engineering - 4th International Conference, MEDI 2014, Sep 2014, Larrnaca, Greece. Springer, 8748, pp.1-3, 2014, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉
Accès au bibtex
BibTex
titre
The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)
auteur
Dominique Méry, Bernhard Schätz, Alan Wassyng
article
Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2014, 4 (2), pp.17--37
Accès au bibtex
BibTex
titre
Bounding messages for free in security protocols – extension to various security properties
auteur
Myrto Arapinis, Marie Duflot
article
Information and Computation, Elsevier, 2014, pp.34. 〈10.1016/j.ic.2014.09.003〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01083657/file/versionjournal.pdf BibTex
titre
Flip-Pushdown Automata with k Pushdown Reversals and E0L Systems are Incomparable
auteur
Marek Kosta, Pavol Duris
article
Information Processing Letters, Elsevier, 2014, 114 (8), pp.417-420
Accès au bibtex
BibTex

2013

titre
Frontiers of Combining Systems
auteur
Pascal Fontaine, Christophe Ringeissen, Renate Schmidt
article
Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. 8152, Springer, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
Accès au bibtex
BibTex
titre
Hierarchic Superposition With Weak Abstraction
auteur
Peter Baumgartner, Uwe Waldmann
article
Maria Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.39-57, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_3〉
Accès au bibtex
BibTex
titre
Computing Tiny Clause Normal Forms
auteur
Noran Azmy, Christoph Weidenbach
article
Maria-Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.109-125, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_7〉
Accès au bibtex
BibTex
titre
Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
auteur
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner Seiler, Thomas Sturm, Andreas Weber
article
Vladimir P. Gerdt and Wolfram Koepf and Ernst W. Mayr and Evgenii V. Vorozhtsov. Computer Algebra in Scientific Computing, Sep 2013, Berlin, Germany. Springer, 8136, pp.88-99, 2013, Computer Algebra in Scientific Computing. 〈10.1007/978-3-319-02297-0_7〉
Accès au bibtex
BibTex
titre
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
auteur
Ralf Karrenberg, Marek Kosta, Thomas Sturm
article
Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems. 〈10.1007/978-3-642-40885-4_5〉
Accès au bibtex
BibTex
titre
SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages
auteur
Marek Kosta
article
Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), 2013, Nanning, China. 2013
Accès au bibtex
BibTex
titre
Formal Specification of Medical Systems by Proof-Based Refinement
auteur
Dominique Méry, Neeraj Kumar Singh
article
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.15. 〈10.1145/2406336.2406351〉
Accès au bibtex
BibTex
titre
Formal Modelling and Verification of Population Protocols
auteur
Dominique Méry, Mike Poppleton
article
Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 2013, LNCS
Accès au bibtex
BibTex
titre
Hierarchic Superposition: Completeness without Compactness
auteur
Peter Baumgartner, Uwe Waldmann
article
Marek Kosta and Thomas Sturm. MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12, 〈http://resources.mpi-inf.mpg.de/conferences/macis2013/program.html〉
Accès au bibtex
BibTex
titre
SyMT: finding symmetries in SMT formulas
auteur
Carlos Areces, David Déharbe, Pascal Fontaine, Orbe Ezequiel
article
11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland. 2013
Accès au bibtex
BibTex
titre
Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. 2013
Accès au bibtex
BibTex
titre
Ideal Mode Selection of a Cardiac Pacing System
auteur
Dominique Méry, Neeraj Kumar Singh
article
Vincent G. Duffy. 4th International Conference - Digital Human Modeling and applications in Health, Safety, Ergonomics and Risk Management - DHM 2013 (HCI International 2013), Jul 2013, Las Vegas, United States. Springer, 8025, pp.258-267, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39173-6_31〉
Accès au bibtex
BibTex
titre
Certifying Network Calculus in a Proof Assistant
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
article
EUCASS - 5th European Conference for Aeronautics and Space Sciences, Jul 2013, Munich, Germany. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904817/file/submission.pdf BibTex
titre
Towards Certifying Network Calculus
auteur
Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
article
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.484-489, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_37〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00904796/file/final.pdf BibTex
titre
Formal Verification of Distributed Algorithms
auteur
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
article
Bernadette Charron-Bost and Stephan Merz and Andrey Rybalchenko and Josef Widder. 3, Dagstuhl, pp.16, 2013, Dagstuhl Reports, 〈10.4230/DagRep.3.4.1〉
Accès au bibtex
BibTex
titre
Computing prime implicant
auteur
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
article
FMCAD - Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. IEEE, pp.46-52, 2013, 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings/54418_IEEE%20FMCAD_Complete%20Book.pdf〉
Accès au bibtex
BibTex
titre
From Event-B Specifications to Programs for Distributed Algorithms
auteur
Mohammed Tounsi, Mohammed Mosbah, Dominique Méry
article
Sumitra Reddy and Mohammed Jmaiel. WETICE 2013: 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises., Jun 2013, Hammamet, Tunisia. IEEE, 2013, 22nd IEEE WETICE Conference. 〈10.1109/WETICE.2013.44〉
Accès au bibtex
BibTex
titre
Transforming EVENT B Models into Verified C# Implementations
auteur
Dominique Méry, Monahan Rosemary
article
Alexei Lisitsa and Andrei Nemytykh. VPT 2013 - First International Workshop on Verification and Program Transformation, Jul 2013, Saint Petersburg, Russia. 16, pp.57-73, 2013, EPIC. 〈http://www.easychair.org/publications/?page=692335489〉
Accès au bibtex
BibTex
titre
Event B
auteur
Dominique Méry, Neeraj Kumar Singh
article
Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7
Accès au bibtex
BibTex

2012

titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., 2012, 〈http://arxiv.org/abs/1208.5933〉
Accès au bibtex
BibTex
titre
Revisiting Snapshot Algorithms by Refinement-based Techniques
auteur
Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh
article
PDCAT 2012 : The Thirteenth International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2012, Beijing, China. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00734131/file/pdcat2012v14.pdf BibTex
titre
Formal Verification of Fault Tolerant NoC-based Architecture
auteur
Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, Camel Tanougast
article
First International Workshop on Mathematics and Computer Science (IWMCS2012), Dec 2012, Tiaret, Algeria. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00763092/file/iwmcsv5.pdf BibTex
titre
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
auteur
Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
article
Science of Computer Programming, Elsevier, 2012, 77 (10-11), pp.1122-1150
Accès au bibtex
BibTex
titre
Formal Verification of Distributed Algorithms using PlusCal-2
auteur
Sabina Akhtar
article
Data Structures and Algorithms [cs.DS]. Université de Lorraine, 2012. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00815570/file/ThA_se-Sabina_AKHTAR.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32759-9_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
Critical systems development methodology using formal techniques
auteur
Dominique Méry, Neeraj Kumar Singh
article
3rd International Symposium on Information and Communication Technology - SoICT 2012, Aug 2012, Ha Long, Vietnam. ACM, pp.3-12, 2012, SoICT '12 - Proceedings of the Third Symposium on Information and Communication Technology. 〈10.1145/2350716.2350720〉
Accès au bibtex
BibTex
titre
Medical Protocol Diagnosis Using Formal Methods
auteur
Dominique Méry, Neeraj Kumar Singh
article
Liu, Zhiming and Wassyng, Alan. Foundations of Health Informatics Engineering and Systems, 7151, Springer Berlin Heidelberg, pp.1-20, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. 〈10.1007/978-3-642-32355-3_1〉
Accès au bibtex
BibTex
titre
Formalization of Heart Models Based on the Conduction of Electrical Impulses and Cellular Automata
auteur
Dominique Méry, Neeraj Kumar Singh
article
Liu, Zhiming and Wassyng, Alan. Foundations of Health Informatics Engineering and Systems}, 7151, Springer Berlin Heidelberg, pp.140-159, 2012, Lecture Notes in Computer Science, 978-3-642-32354-6. 〈10.1007/978-3-642-32355-3_9〉
Accès au bibtex
BibTex
titre
Stuttering Equivalence
auteur
Stephan Merz
article
[Research Report] 2012
Accès au bibtex
BibTex
titre
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
auteur
Henri Debrat, Stephan Merz
article
[Research Report] 2012
Accès au bibtex
BibTex
titre
Harnessing SMT Solvers for TLA+ Proofs
auteur
Stephan Merz, Hernán Vanzetto
article
Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, 53, 2012, ECEASST
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760579/file/avocs2012.pdf BibTex
titre
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. Springer, 7180, pp.289-303, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28717-6_23〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00760570/file/tla2smt.pdf BibTex
titre
Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic
auteur
Martin Bromberger
article
Logic in Computer Science [cs.LO]. 2012
Accès au bibtex
BibTex
titre
Automatic Generation of Invariants for Circular Derivations in SUP(LA)
auteur
Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach
article
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mar 2012, Mérida, Venezuela. Springer, 7180, pp.197-211, 2012, LNCS
Accès au bibtex
BibTex
titre
More SPASS with Isabelle -- Superposition with Hard Sorts and Configurable Simplification
auteur
Jasmin Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
article
Lennart Beringer and Amy Felty. Interactive Theorem Proving (ITP 2012), Aug 2012, Princeton, New Jersey, United States. Springer, 7406, pp.345-360, 2012, LNCS
Accès au bibtex
BibTex
titre
Formal Verification Of Pastry Using TLA+
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Leslie Lamport and Stephan Merz. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00768812/file/paper.pdf BibTex
titre
FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings
auteur
Dimitra Giannakopoulou, Dominique Méry
article
Dimitra Giannakopoulou and Dominique Méry. Springer, 7436, pp.488, 2012, LNCS - Lecture Notes in Computer Science, 978-3-642-32758-2. 〈10.1007/978-3-642-32759-9〉
Accès au bibtex
BibTex
titre
Handling Heterogeneity in Formal Developments of Hardware and Software Systems
auteur
Yamine Ait Ameur, Dominique Méry
article
Tiziana Margaria and Bernhard Steffen. ISoLA - 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - 2012, Oct 2012, Amirandes, Heraklion, Greece. Springer, 7610, pp.327-328, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34032-1_33〉
Accès au bibtex
BibTex
titre
Combination of disjoint theories: beyond decidability
auteur
Pascal Fontaine, Stephan Merz, Christoph Weidenbach
article
Bernhard Gramlich and Dale Miller and Uli Sattler. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.256-270, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31365-3_21〉
Accès au bibtex
BibTex
titre
SMT solvers for Rodin
auteur
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
article
John Derrick and John A. Fitzgerald and Stefania Gnesi and Sarfraz Khurshid and Michael Leuschel and Steve Reeves and Elvinia Riccobene. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. Springer, 7316, pp.194-207, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-30885-7_14〉
Accès au bibtex
BibTex

2011

titre
Towards Verification of the Pastry Protocol using TLA+
auteur
Stephan Merz, Tianxiang Lu, Christoph Weidenbach
article
R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. 6722, 2011, FMOODS/FORTE 2011
Accès au bibtex
BibTex
titre
Stepwise Development of Distributed Algorithms (Research Abstract)
auteur
Manamiary Bruno Andriamiarina
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606204/file/_ANDRIAMIARINA_Abstract_FME_Symposium_FM2011_v4.pdf BibTex
titre
Stepwise Development of Distributed Vertex Colouring Algorithms (Abstract)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry
article
2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606201/file/_MERY-ANDRIAMIARINA_Abstract_Grande_Region_SECDAY_2011_v2.pdf BibTex
titre
Stepwise Development Of Distributed Vertex Coloring Algorithms (Full Report)
auteur
Manamiary Bruno Andriamiarina, Dominique Méry
article
[Technical Report] LORIA - Université de Lorraine. 2011, pp.90
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606254/file/Rapport_v0.pdf BibTex
titre
Compression of Propositional Resolution Proofs via Partial Regularization
auteur
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. Springer, 6803, pp.237-251, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-22438-6_19〉
Accès au bibtex
BibTex
titre
Exploiting Symmetry in SMT Problems
auteur
David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. Springer, 6803, pp.222-236, 2011, 〈10.1007/978-3-642-22438-6_18〉
Accès au bibtex
BibTex
titre
SimGrid MC: Verification Support for a Multi-API Simulation Platform
auteur
Stephan Merz, Martin Quinson, Cristian Rosa
article
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.274-288, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_18〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf BibTex
titre
Towards Verification of the Pastry Protocol Using TLA +
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.244-258, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_16〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf BibTex
titre
Formal Verification of Consensus Algorithms Tolerating Malicious Faults
auteur
Bernadette Charron-Bost, Henri Debrat, Stephan Merz
article
Xavier Défago and Franck Petit and Vincent Villain. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer, 6976, pp.120-134, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24550-3_11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00639048/file/main.pdf BibTex
titre
Fragments de l'arithmétique dans une combinaison de procédures de décision
auteur
Diego Caminha Barbosa de Oliveira
article
Génie logiciel [cs.SE]. Université Nancy II, 2011. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00578254/file/thesis_full.pdf BibTex
titre
Combining theories: the Ackerman and Guarded Fragments
auteur
Carlos Areces, Pascal Fontaine
article
Cesare Tinelli and Viorica Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Oct 2011, Saarbrücken, Germany. Springer Verlag, 6989, pp.40--54, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24364-6_4〉
Accès au bibtex
BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.pdf BibTex
titre
Quantifier Inference Rules for SMT proofs
auteur
David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642535/file/paper2.pdf BibTex
titre
Towards certification of TLA+ proof obligations with SMT solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00645458/file/tla2smt.pdf BibTex

2010

titre
A High-Level Language for Modeling Algorithms and their Properties
auteur
Sabina Akhtar, Stephan Merz, Martin Quinson
article
13th Brazilian Symposium on Formal Methods - SBMF'2010, Nov 2010, Natal, Brazil. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537779/file/final.pdf BibTex
titre
Integrated Formal Methods
auteur
Dominique Méry, Stephan Merz
article
Dominique Méry and Stephan Merz. 6396, Springer, pp.335, 2010, Lecture Notes in Computer Science, 978-3-642-16264-0. 〈10.1007/978-3-642-16265-7〉
Accès au bibtex
BibTex
titre
Verifying Safety Properties With the TLA+ Proof System
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-14203-1_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534821/file/tlaps.pdf BibTex
titre
A Simple Model of Communication APIs ­ - Application to Dynamic Partial-order Reduction
auteur
Cristian Rosa, Stephan Merz, Martin Quinson
article
10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Sep 2010, Düsseldorf, Germany. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00532889/file/avocs.pdf BibTex
titre
Model Checking the Pastry Routing Protocol
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
Jens Bendisposto and Michael Leuschel and Markus Roggenbach. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. Universität Düsseldorf, pp.19-21, 2010, 10th International Workshop Automated Verification of Critical Systems
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540811/file/article-new.pdf BibTex
titre
Formal Verification of Consensus Algorithms in a Proof Assistant
auteur
Henri Debrat, Bernadette Charron-Bost, Stephan Merz
article
Michael Backes and Ralf Küsters. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00539899/file/sho-isabelle.pdf BibTex
titre
Exploring and Exploiting Algebraic and Graphical Properties of Resolution
auteur
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
article
8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00544658/file/AlgebraicPropertiesOfResolution.pdf BibTex
titre
Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms
auteur
Sabina Akhtar, Stephan Merz, Martin Quinson
article
Eric Cariou, Laurence Duchien, Yves Ledru. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00544137/file/GDR-GDL_Sabina.pdf BibTex
titre
Physics and Proof Theory
auteur
Bruno Woltzenlogel Paleo
article
International Workshop on Physics and Computation, Aug 2010, Luxor, Egypt
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545462/file/PhysicsAndProofTheory_Elsevier_.pdf BibTex
titre
System Description: The Proof Transformation System CERES
auteur
Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo
article
Jürgen Giesl and Reiner Hähnle. International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.427-433, 2010, Lecture Notes in Computer Science / Lecture Notes in ArtificiaI Intelligence. 〈10.1007/978-3-642-14203-1_36〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545482/file/CEResSystemDescription.pdf BibTex
titre
Atomic Cut Introduction by Resolution: Proof Structuring and Compression
auteur
Bruno Woltzenlogel Paleo
article
Edmund M. Clarke and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Apr 2010, Dakar, Senegal. Springer, 6355, pp.463-480, 2011, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-17511-4_26〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545473/file/AtomicCutIntroduction_-_Submitted_Version.pdf BibTex
titre
Using Proofs to Compute Implicatures [Abstract]
auteur
Bruno Woltzenlogel Paleo, Ekaterina Lebedeva
article
Computability in Europe, Jun 2010, Ponta Delgada, Portugal
Accès au bibtex
BibTex
titre
Proof Compression with the CIRes Method [Abstract]
auteur
Bruno Woltzenlogel Paleo
article
Computability in Europa, Jun 2010, Ponta Delgada, Portugal
Accès au bibtex
BibTex

2002

titre
A Scalable Approach to Network Enabled Servers
auteur
Eddy Caron, Philippe Combes, Sylvain Contassot-Vivier, Frédéric Desprez, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
[Research Report] RR-2002-21, LIP - ENS Lyon. 2002
Accès au bibtex
BibTex
titre
A Scalable Approach to Network Enabled Servers
auteur
Eddy Caron, Frédéric Desprez, Frédéric Lombard, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
B. Monien and R. Feldmann. 8th International EuroPar Conference, 2002, Paderborn, Germany. Springer-Verlag, 2400, pp.4, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
Une approche hiérarchique des serveurs de calculs
auteur
Eddy Caron, Frédéric Desprez, Eric Fleury, Frédéric Lombard, Jean-Marc Nicod, Martin Quinson, Frédéric Suter
article
Françoise Baude. Calcul réparti à grande échelle, Hermès Science Paris, pp.23, 2002, 2-7462-0472-X
Accès au bibtex
BibTex

2001

titre
SCILAB to SCILAB// - The Ouragan Project
auteur
Eddy Caron, Serge Chaumette, Sylvain Contassot-Vivier, Frédéric Desprez, Eric Fleury, Claude Gomez, Maurice Goursat, Emmanuel Jeannot, Dominique Lazure, Frédéric Lombard, Jean-Marc Nicod, Laurent Philippe, Martin Quinson, Pierre Ramet, Jean Roman, Franck Rubi, Serge Steer, Frederic Suter, Gil Utard
article
[Research Report] RR-2001-24, LIP - ENS Lyon. 2001
Accès au bibtex
BibTex