MOSEL - Publications 2010

[1] Sabina Akhtar, Stephan Merz, and Martin Quinson. Extending pluscal: A language for describing concurrent and distributed algorithms. In Eric Cariou, Laurence Duchien, and Yves Ledru, editors, Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, France Pau, March 2010. [ bib ]
[2] Sabina Akhtar, Stephan Merz, and Martin Quinson. A high-level language for modeling algorithms and their properties. In 13th Brazilian Symposium on Formal Methods - SBMF'2010, Brazil Natal, November 2010. [ bib ]
[3] Projet ANR-RIMEL. Tools. Livrable RIMEL, LORIA, Juin 2010. [ bib ]
[4] Nazim Benaïssa. La composition des protocoles de sécurité avec la méthode B événementielle. PhD thesis, Université Henri Poincaré Nancy 1, Nancy, France, 2010. [ bib ]
[5] Nazim Benaissa and Dominique Méry. Proof-based design of security protocols. In Ernst W. Mayr, editor, 5th International Computer Science Symposium in Russia, CSR 2010, volume 6072 of Lecture Notes in Computer Science, pages 25-36, Russian Federation Kazan, June 2010. Farid Ablayev, Springer. [ bib ]
[6] Thomas Bouton, Diego Caminha B. De Oliveira, David Déharbe, and Pascal Fontaine. Gridtpt: a distributed platform for theorem prover testing. In 2nd Workshop on Practical Aspects of Automated Reasoning (PAAR), United Kingdom Edinburgh, 2010. [ bib ]
[7] Diego Caminha B. De Oliveira, David Déharbe, and Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Science of Computer Programming, 2010. [ bib ]
[8] Dominique Cansell and Dominique Méry. Designing old and new distributed algorithms by replaying an incremental proof-based development. In Jean-Raymond Abrial and Uwe Glässer, editors, Rigorous Methods for Software Construction and Analysis - Papers Dedicated to Egon Börger on the Occasion of His 60th Birthday, number 5115, 2010. [ bib ]
[9] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. The tla+ proof system: Building a heterogeneous verification platform. In Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock, editors, International Conference on Theoretical Aspects of Computing - ICTAC 2010, volume 6255 of Lecture Notes in Computer Science, page 44, Brazil Natal, 2010. Springer. The original publication is available at www.springerlink.com. [ bib | DOI ]
[10] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. Verifying safety properties with the tla+ proof system. In Jürgen Giesl and Reiner Haehnle, editors, Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, volume 6173 of Lecture Notes in Artificial Intelligence, pages 142-148, United Kingdom Edinburgh, 2010. Springer. The original publication is available at www.springerlink.com. [ bib | DOI ]
[11] Henri Debrat, Bernadette Charron-Bost, and Stephan Merz. Formal verification of consensus algorithms in a proof assistant. In Michael Backes and Ralf Küsters, editors, 2010 Grande Region Security and Reliability Day, Germany Saarbrücken, March 2010. [ bib ]
[12] Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, and Bruno Woltzenlogel Paleo. System description: The proof transformation system ceres. In Jürgen Giesl and Reiner Hähnle, editors, International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Computer Science / Lecture Notes in ArtificiaI Intelligence, pages 427-433, United Kingdom Edinburgh, 2010. Springer. The original publication is available at www.springerlink.com. [ bib | DOI ]
[13] D. Fass. From integrative neurosciences to augmented human engineering. In NeuroTalk 2010, 25th-28th june 2010. [ bib ]
[14] Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo. Exploring and exploiting algebraic and graphical properties of resolution. In Aarti Gupta and Daniel Kroening, editors, 8th Intl. Workshop Satisfiability Modulo Theory (SMT 2010), page ???, Edinburgh, UK, 2010. ??? bibentry TBC. [ bib ]
[15] Tianxiang Lu, Stephan Merz, and Christoph Weidenbach. Model checking the pastry routing protocol. In Jens Bendisposto, Michael Leuschel, and Markus Roggenbach, editors, 10th International Workshop Automated Verification of Critical Systems, pages 19-21, Germany Düsseldorf, September 2010. Universität Düsseldorf. short communication. [ bib ]
[16] D. Méry, M. Mosbah, and M. Tounsi. Integrating local computation models by refinement. In Symbolic Computation in Software Science (SCSS 2010), RISC, 2010. [ bib ]
[17] Dominique Méry. Refinement-based guidelines for constructing algorithms. In Jean-Raymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. [ bib | http ]
[18] Dominique Méry and Stephan Merz, editors. Integrated Formal Methods, volume 6396 of Lecture Notes in Computer Science. Springer, October 2010. [ bib | DOI ]
[19] Dominique Méry, Mohammed Mosbah, and Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. In Markus Roggenbach Jens Bendisposto, Michael Leuschel, editor, AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Dusseldorf Germany, 09 2010. [ bib | http ]
[20] Dominique Méry and Neeraj Kumar Singh. Eb2c : A tool for event-b to c conversion support, September 2010. [ bib ]
[21] Dominique Méry and Neeraj Kumar Singh. Functional behavior of a cardiac pacing system. International Journal of Discrete Event Control Systems (IJDECS), December 2010. [ bib ]
[22] Dominique Méry and Neeraj Kumar Singh. Real-time animation for formal specification. In Marc Aiguier, Francis Bretaudeau, and Daniel Krob, editors, Complex Systems Design & Management 2010, pages 49-60, France Paris, October 2010. Springer. [ bib | DOI ]
[23] Dominique Méry and Neeraj Kumar Singh. Technical report on formal development of two-electrode cardiac pacing system. Research report, LORIA, February 2010. [ bib ]
[24] Dominique Méry and Neeraj Kumar Singh. Trustable formal specification for software certification. In T. Margaria and B. Steffen, editors, 4th International Symposium On Leveraging Applications of Formal Methods - ISOLA 2010, volume 6416 of Lecture Notes in Computer Science, pages 312-326, Greece Heraklion, Crete, October 2010. Springer. [ bib | DOI ]
[25] Joris Rehm. Proved development of the real-time properties of the ieee 1394 root contention protocol with the event b method. International Journal on Software Tools for Technology Transfer (STTT), 12(1):39-51, February 2010. [ bib | DOI ]
[26] Denis Roegel. Bürgi's Progress Tabulen (1620): logarithmic tables without logarithms. Research report, LORIA, 2010. [ bib ]
[27] Denis Roegel. A construction of edward sang's projected table of nine-place logarithms to one million (1872). Research report, LORIA, 2010. [ bib ]
[28] Denis Roegel. The great logarithmic and trigonometric tables of the french cadastre: a preliminary investigation. Research report, LORIA, 2010. [ bib ]
[29] Denis Roegel. Introduction to chinese and japanese tables of logarithms, with a review of secondary sources. Research report, LORIA, 2010. [ bib ]
[30] Denis Roegel. Napier's ideal construction of the logarithms. Research report, LORIA, 2010. [ bib ]
[31] Denis Roegel. A reconstruction of adriaan vlacq's tables in the Trigonometria artificialis (1633). Research report, LORIA, 2010. [ bib ]
[32] Denis Roegel. A reconstruction of briggs' Logarithmorum chilias prima (1617). Research report, LORIA, 2010. [ bib ]
[33] Denis Roegel. A reconstruction of charles babbage's table of logarithms (1827). Research report, LORIA, 2010. [ bib ]
[34] Denis Roegel. A reconstruction of de decker-vlacq's tables in the Arithmetica logarithmica (1628). Research report, LORIA, 2010. [ bib ]
[35] Denis Roegel. A reconstruction of edward sang's table of logarithms (1871). Research report, LORIA, 2010. [ bib ]
[36] Denis Roegel. A reconstruction of gunter's Canon triangulorum (1620). Research report, LORIA, 2010. [ bib ]
[37] Denis Roegel. A reconstruction of henri andoyer's table of logarithms (1911). Research report, LORIA, 2010. [ bib ]
[38] Denis Roegel. A reconstruction of henri andoyer's trigonometric tables (1915-1918). Research report, LORIA, 2010. [ bib ]
[39] Denis Roegel. A reconstruction of the tables des logarithmes à huit d{\'e}cimales'' from the french service géographique de l'armée” (1891). Research report, LORIA, 2010. [ bib ]
[40] Denis Roegel. A reconstruction of the tables of briggs and gellibrand's Trigonometria Britannica (1633). Research report, LORIA, 2010. [ bib ]
[41] Denis Roegel. A reconstruction of the tables of briggs' Arithmetica logarithmica (1624). Research report, LORIA, 2010. [ bib ]
[42] Denis Roegel. A reconstruction of the tables of pitiscus' Thesaurus Mathematicus (1613). Research report, LORIA, 2010. [ bib ]
[43] Denis Roegel. A reconstruction of the tables of rheticus' Canon doctrinæ triangulorum (1551). Research report, LORIA, 2010. [ bib ]
[44] Denis Roegel. A reconstruction of the tables of rheticus' Opus Palatinum (1596). Research report, LORIA, 2010. [ bib ]
[45] Denis Roegel. A sketch of mendizábal y tamborrel's table of logarithms (1891). Research report, LORIA, 2010. [ bib ]
[46] Cristian Rosa, Stephan Merz, and Martin Quinson. A simple model of communication apis - application to dynamic partial-order reduction. In 10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Germany Düsseldorf, September 2010. [ bib ]
[47] Bruno Woltzenlogel Paleo. Atomic cut introduction by resolution: Proof structuring and compression. In ???, page ??? ???, 2010. bibentry TBC. [ bib ]
[48] Bruno Woltzenlogel Paleo. Physics and proof theory. In International Workshop on Physics and Computation, Egypt Luxor, August 2010. [ bib ]
[49] Bruno Woltzenlogel Paleo. Proof compression with the cires method [abstract]. In Computability in Europa, Portugal Ponta Delgada, June 2010. [ bib ]
[50] Bruno Woltzenlogel Paleo and Ekaterina Lebedeva. Using proofs to compute implicatures [abstract]. In Computability in Europe, Portugal Ponta Delgada, June 2010. [ bib ]
[51] Hehua Zhang, Stephan Merz, and Ming Gu. Specifying and verifying plc systems with tla+: a case study. Computers & Mathematics with Applications, 60(3):695-705, August 2010. [ bib | DOI ]

This file has been generated by bibtex2html 1.87.