Publication 2005

article

D Méry, D Cansell, C Proch, D Abraham, P Ditsch. The challenge of QoS for digital television services apr 2005 EBU Technical Review A05-R-030
J -R Abrial, D Cansell. Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity) Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181) 2005 Journal of Universal Computer Science 11 744--770 Springer http://hal.inria.fr/inria-00000120/en/
D Cansell, D Méry, C Proch. Un système d'analyse de la qualité: de la norme au produit en passant par le raffinement 2005 Génie logiciel 44--50 CNAM - Paris, France http://hal.inria.fr/inria-00000196/en/
A Knapp, S Merz, M Wirsing, J Zappe. Specification and Refinement of Mobile Systems in MTLA and Mobile UML dec 2005 Theoretical Computer Science Elsevier http://hal.inria.fr/inria-00000754/en/
D Roegel. Kissing Circles: A French Romance in METAPOST 2005 TUGboat 26 10--17 TeX Users Group http://hal.inria.fr/inria-00000659/en/

inproceedings

D Cansell, D Méry. Formal and Incremental Construction of a Distributed Reference Counting Algorithm APPSEM 2005 sep 2005 Hoffmann, M. and Loidl, H.-W.
P Fontaine, Kant K Gupta, J -Y Marion, S Merz, Prensa L Nieto, A Tiu. Towards a Combination of Heterogeneous Deductive Tools for System Verification APPSEM 2005 sep 2005 Hoffmann, M. and Loidl, H.-W.
D Cansell, D Méry, C Proch. Proved Design of Hardware Architecture Formal Specification and Development in Z and B (ZB 2005). Poster session apr 2005
D Roegel. MP2GL: prototyping 3D objects with METAPOST and OpenGL 15e rencontre annuelle des utilisateurs européens de TeX - EuroTeX 2005 mar 2005 A05-R-021 http://www.loria.fr/publications/2005/A05-R-021/A05-R-021.ps
J -R Abrial, D Cansell, D Méry. Refinement and Reachability in Event\_B ZB 2005: Formal Specification and Development in Z and B apr 2005 H. Treharne and S. King and M. Henson 3455 Lecture Notes in Computer Science 222--241 Springer Verlag A05-R-031
D Abraham, D Cansell, P Ditsch, D Méry, C Proch. Synthesis of the QoS for digital TV services First International Workshop on Incentive Based Computing - IBC'05 2005 http://hal.inria.fr/inria-00000565/en/
D Barsotti, L Prensa Nieto, A Tiu. Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS '05 2005 http://hal.inria.fr/inria-00000638/en/
D Cansell, D Méry, C Proch. Modelling SystemC scheduler by refinement IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05 2005 http://hal.inria.fr/inria-00000564/en/
L Fejoz, D Méry, S Merz. DIXIT: a Graphical Toolkit for Predicate Abstractions Fourth International Workshop on Automated Verification of Infinite-State Systems (AVIS 2005) 2005 R. Bharadwaj and S. Mukhopadhyay 39--48 http://hal.inria.fr/inria-00000767/en/
P Fontaine, S Ranise, C Zarba. Combining Lists with Non-Stably Infinite Theories 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04) 2005 F. Baader and A. Voronkov 3452 Lecture Notes in Computer Science 51--66 Springer-Verlag http://hal.inria.fr/inria-00000481/en/
M Hammer, A Knapp, S Merz. Truly On-The-Fly LTL Model Checking Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) 2005 N. Halbwachs, L. D. Zuck 3440 Lecture Notes in Computer Science 191--205 Springer-Verlag http://hal.inria.fr/inria-00000753/en/
E Kang. Real-Time system verification techniques based on abstraction/deduction and model checking Doctoral Symposium of the Fifth International Conference on Integrated Formal Methods - IFM'2005. Technical Report of MCS, TU-Eindhoven 2005 J. Romijn http://hal.inria.fr/inria-00000641/en/
E Kang, S Merz. Predicate Diagrams for the Verification of Real-Time Systems The Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS'05 2005 R. Lazic, R. Nagarajan, N. Papanikolaou Elsevier http://hal.inria.fr/inria-00000631/en/
Y Zimmermann, D Toma. Component Reuse in B Using ACL2 ZB 2005: Formal Specification and Development in Z and B: 4th International Conference of B and Z Users 2005 H. Treharne and S. King and M. Henson and S. Schneider 3455 Lecture Notes in Computer Science 280--299 Springer-Verlag http://hal.inria.fr/inria-00000755/en/

mastersthesis

L Fejoz. Typage de TLA\textsuperscript+ 2005
N Benaïssa. Conception de systèmes avec le B événementiel à partir de modèles ORBAC 2005

misc

A Tiu. Formalization of a Generalized Protocol for Clock Synchronization jun 2005 http://afp.sourceforge.net/entries/GenClock.shtml
M Jaskelioff, S Merz. Proving the Correctness of DiskPaxos jun 2005 http://afp.sourceforge.net/entries/DiskPaxos.shtml