MOSEL - Publications 2012

[1] Yamine Ait Ameur and Dominique Méry. Handling Heterogeneity in Formal Developments of Hardware and Software Systems. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, volume 7610 of Lecture Notes in Computer Science, pages 327-328, Heraklion, Greece, October 2012. Tiziana Margaria and Bernhard Steffen, Springer. [ bib | http ]
[2] Sabina Akhtar. Verification of Distributed Algorithms using PlusCal-2. PhD thesis, Université de Lorraine, May 2012. [ bib ]
[3] Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, and Camel Tanougast. Formal Verification of Fault Tolerant NoC-based Architecture. In First International Workshop on Mathematics and Computer Science (IWMCS2012), Tiaret, Algeria, December 2012. [ bib | http ]
[4] Manamiary Bruno Andriamiarina, Dominique Méry, and Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques. In PDCAT 2012 : The Thirteenth International Conference on Parallel and Distributed Computing, Applications and Technologies, Beijing, China, 2012. [ bib | http ]
[5] Jasmin Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving (ITP 2012), volume 7406 of LNCS, pages 345-360, Princeton, New Jersey, United States, 2012. Springer. [ bib | http ]
[6] Martin Bromberger. Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic. Final report of studies end, Universität des Saarlandes, Saarbrücken, 2012. [ bib | http ]
[7] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ Proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium On Formal Methods - FM 2012, volume 7436 of Lecture Notes in Computer Science, pages 147-154, Paris, France, 2012. Springer. The original publication is available at www.springerlink.com. [ bib | DOI | http ]
[8] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ Proofs. In AI meets Formal Software Development, page 16 p., Dagstuhl, Germany, 2012. [ bib | http ]
[9] Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming, 77(10-11):1122-1150, September 2012. [ bib | http ]
[10] Henri Debrat and Stephan Merz. Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Research report, Archive of Formal Proofs, July 2012. Published at http://afp.sourceforge.net/entries/Heard_Of.shtml. [ bib | http ]
[11] David Déharbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. SMT solvers for Rodin. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, volume 7316 of Lecture Notes in Computer Science, pages 194-207, Pisa, Italy, 2012. Springer. The original publication is available at www.springerlink.com. [ bib | DOI | http ]
[12] Jean-Marc Dupont, Romain Lieber, Gérard Morel, Dominique Méry, and Fabien Bouffaron. Spécification d'un Processus Technico-Physiologique de Perception de Fermeture et Verrouillage d'un capot moteur en situation de maintenance aéronautique. Rapport ISET, September 2012. [ bib | http ]
[13] Didier Fass. Augmented Human Engineering: A Theoretical and Experimental Approach to Human Systems Integration. In Boris Cogan, editor, Systems Engineering - Practice and Theory, Computer and Information Science - Numerical Analysis and Scientific Computing, pages 257-276. InTech Open Access Publisher, March 2012. 21 pages, open document. [ bib | DOI | http ]
[14] Didier Fass and Franci Janot. Le corps d'une «prophétesse» ? In Florence Calament, Ricardo Eichmann, and Christophe Vendries, editors, Le luth dans l'Égypte byzantine. La tombe de la «Prophétesse d'Antinoé» au Musée de Grenoble, Deutsches Archäologisches Institut Orient-Abteilung Orient-Archäologie Band 26, page 190. Verlag Marie Leidorf GmbH, Rahden/Westf., 2012. [ bib | http ]
[15] Arnaud Fietzke, Evgeny Kruglov, and Christoph Weidenbach. Automatic Generation of Invariants for Circular Derivations in SUP(LA). In Nikolaj Bjørner and Andrei Voronkov, editors, 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 7180 of LNCS, pages 197-211, Mérida, Venezuela, Bolivarian Republic Of, 2012. Springer. [ bib | http ]
[16] Pascal Fontaine, Stephan Merz, and Christoph Weidenbach. Combination of disjoint theories: beyond decidability. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, volume 7364 of Lecture Notes in Computer Science, pages 256-270, Manchester, United Kingdom, 2012. Springer. The original publication is available at www.springerlink.com. [ bib | DOI | http ]
[17] Dimitra Giannakopoulou and Dominique Méry, editors. FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, volume 7436 of LNCS. Springer, August 2012. [ bib | http ]
[18] Tianxiang Lu, Stephan Merz, and Christoph Weidenbach. Formal Verification Of Pastry Using TLA+. In Leslie Lamport and Stephan Merz, editors, International Workshop on the TLA+ Method and Tools, Paris, France, August 2012. [ bib | http | .pdf ]
[19] Dominique Méry and Neeraj Kumar Singh. Critical systems development methodology using formal techniques. In 3rd International Symposium on Information and Communication Technology - SoICT 2012, pages 3-12, Ha Long, Viet Nam, August 2012. ACM. [ bib | DOI | http ]
[20] Dominique Méry and Neeraj Kumar Singh. Formal Specification of Medical Systems by Proof-Based Refinement. ACM Transactions in Embedded Computing Systems, January 2012. [ bib | http ]
[21] Dominique Méry and Neeraj Kumar Singh. Formalization of Heart Models Based on the Conduction of Electrical Impulses and Cellular Automata. In Zhiming Liu and Alan Wassyng, editors, Foundations of Health Informatics Engineering and Systems, volume 7151 of Lecture Notes in Computer Science, pages 140-159. Springer Berlin Heidelberg, 2012. [ bib | DOI | http ]
[22] Dominique Méry and Neeraj Kumar Singh. Medical Protocol Diagnosis Using Formal Methods. In Zhiming Liu and Alan Wassyng, editors, Foundations of Health Informatics Engineering and Systems, volume 7151 of Lecture Notes in Computer Science, pages 1-20. Springer Berlin Heidelberg, 2012. [ bib | DOI | http ]
[23] Stephan Merz. Stuttering Equivalence. Research report, Archive of Formal Proofs, May 2012. Published at http://afp.sourceforge.net/entries/Stuttering_Equivalence.shtml. [ bib | http ]
[24] Stephan Merz and Hernán Vanzetto. Automatic Verification Of Proof Obligations With SMT Solvers. In Nikolaj Bjørner and Andrei Voronkov, editors, 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), volume 7180 of Lecture Notes in Computer Science, pages 289-303, Mérida, Venezuela, Bolivarian Republic Of, March 2012. Springer. [ bib | DOI | http ]
[25] Stephan Merz and Hernán Vanzetto. Harnessing SMT Solvers for TLA+ Proofs. In Gerald Lüttgen and Stephan Merz, editors, 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), volume 53 of ECEASST, Bamberg, Germany, December 2012. EASST. [ bib | http ]
[26] Denis Roegel. The LOCOMAT Project: Recomputing Mathematical and Astronomical Tables. IEEE Annals of the History of Computing, 34(2):74-79, 2012. [ bib | DOI | http ]

This file has been generated by bibtex2html 1.87.