Radu Mateescu Address: INRIA Grenoble - Rhône-Alpes / VASY Inovallée 655, avenue de l'Europe - Montbonnot F-38334 Saint Ismier FRANCE Email: Radu.Mateescu@inria.fr Phone: +(33) (0)4 76 61 54 86 Fax: +(33) (0)4 76 61 52 52 Web: http://www.inrialpes.fr/vasy/people/Radu.Mateescu

Curriculum

• Since 1998: Chargé de recherche at INRIA Rhône-Alpes in the VASY project-team.
  During 2007 and part of 2008, I was hosted by the University of Burgundy in Dijon.
  During part of 2005 and 2006, I was hosted by the PLUME team of the LIP laboratory of ENS Lyon.


• 1997-1998: Post-doctoral fellowship at CWI (Amsterdam) in the SEN2 group, under the direction of prof. Jan Friso Groote.
  The post-doctoral fellowship was funded by ERCIM.
  


• 1994-1997: PhD thesis, entitled "Vérification des propriétés temporelles des programmes parallèles", at the INPG doctoral school. Research activity carried out at the VERIMAG laboratory / SPECTRE project of INRIA (until 1996) and at the VASY action of INRIA Rhône-Alpes, under the direction of Hubert Garavel. The PhD thesis was funded by a grant of the French Ministry of National Education and Research (MENESR).


• 1993-1994: "DEA" (MSc), entitled "Définition et compilation d'un méta-langage pour l'implémentation des logiques temporelles", at the INPG doctoral school. Master thesis project carried out at the VERIMAG laboratory / SPECTRE project, under the direction of Hubert Garavel.


• 1988-1993: Graduate engineer diploma in computer science at the "POLITEHNICA" University of Bucharest (UPB), Faculty of Automatic Control and Computers. Graduate project, entitled "Optimisation de la compilation des types abstraits algébriques du langage LOTOS", carried out at the VERIMAG laboratory / SPECTRE project, under the direction of Hubert Garavel. The graduate project was funded by a grant of the European TEMPUS program.

Research

My main research topics concern the specification and verification of temporal properties of concurrent systems. As regards specification, I am interested in temporal logics and mu-calculi extended with data-handling primitives, which are well-adapted for specifying properties of action-based, value-passing description languages such as LOTOS and muCRL. As regards verification, I am interested in various techniques and algorithms: on-the-fly model checking and equivalence checking, diagnostic generation, partial order reduction, massively parallel verification, ...

Teaching

• 2007-2008: Postgraduate course entitled "Model Checking of Action-Based Concurrent Systems" at the Max Planck Institute Summer School on Verification Technology, Systems and Applications VTSA'2008 (Saarbruecken, Germany), September 15-19, 2008.
  
  Undergraduate (5ème année) course entitled "Méthodes formelles" at ESIREM (Dijon), together with Emilie Oudot in 2007 and Sylvain Rampacek in 2007-2008.


• 1999-2004: Undergraduate (3ème année) course entitled "Temps-Réel" at ENSIMAG (Grenoble), together with Hubert Garavel in 1999-2000 and 2000-2001, Nicolas Zuanon in 2000-2001, Frédéric Lang in 2001-2002, Aurore Collomb in 2003, and Wendelin Serwe in 2004.


• 1999-2001: DEA (MSc) course entitled "Spécification et Vérification de Protocoles" at Université de Savoie (Annecy), together with prof. Flavio Oquendo.
  


• 1996: Course and project entitled "Programmation Concurrente et Vérification" at Université Joseph Fourier (Grenoble), in the option "Programmation Concurrente" directed by Jean-Marc Vincent.

Software

I contribute to the development of the CADP toolbox for the specification and verification of communication protocols and distributed systems, as author of several verification tools:

• XTL 1.2 (eXecutable Temporal Language) [Mateescu-Garavel-98, Mateescu-98-a] is both a language and a model checker allowing to specify temporal logic properties involving data values and verify them on Labeled Transition Systems (LTSs). The XTL language provides functional-like primitives for exploring LTSs in various ways. It also allows to handle data values contained in transition labels and to define temporal logic operators as recursive functions computing sets of states and transitions of the LTS.

  The XTL model checker was developed using the BCG environment and consists of about 27,000 lines of code (SYNTAX, LOTOS, and C). Data-based extensions of several temporal logics (HML, CTL, ACTL, mu-calculus) were implemented as XTL libraries. Moreover, a model checker for the data-based modal logic FULL was developed using XTL.

  XTL was used for verifying several industrial critical applications:

  • Philips' Bounded Retransmission Protocol
  • Link Layer Protocol of the IEEE-1394 FireWire Serial Bus
  • Bull's Cluster File System
  • Invoicing System
  • Xpress Transfer Protocol
  • HAVi Leader Election Protocol
  • Synchronous hardware
  • Hardware/software codesign
  • Asynchronous hardware
  • Non-refinement transformations of software architectures
  • Abstraction and analysis of clinical guidance trees

• CAESAR_SOLVE [Mateescu-06-a, Mateescu-03-a] is a generic software library dedicated to the on-the-fly resolution of Boolean Equation Systems (BESs). The library uses a representation of BESs as boolean graphs, which provide a more intuitive way of reasoning about the dependencies between boolean variables. It currently offers 5 resolution algorithms, based on various exploration strategies of boolean graphs: depth-first search (with variants optimized in memory consumption for acyclic or disjunctive/conjunctive BESs), breadth-first search, etc. It also provides diagnostics (in the form of boolean subgraphs) explaining the truth value of a given boolean variable [Mateescu-00].

  The CAESAR_SOLVE library was developed using the OPEN/CAESAR environment [Garavel-98], and consists of about 11,500 lines of C code. It is currently used within CADP as verification engine for the EVALUATOR 3.6 model checker, the BISIMULATOR equivalence checker, and the REDUCTOR tool for on-the-fly reduction of LTSs.

• EVALUATOR 3.6 [Mateescu-06-a, Mateescu-03-a, Mateescu-Sighireanu-03, Mateescu-02, Mateescu-Sighireanu-00] is an on-the-fly model checker for regular alternation-free mu-calculus formulas on LTSs. This temporal logic is an extension of the alternation-free mu-calculus with ACTL-like action formulas and PDL-like regular formulas, making a good compromise between expressiveness, user-friendliness, and efficiency of model checking algorithms. The model checker works by translating the verification problem in terms of the on-the-fly resolution of a BES. It is also able to generate diagnostics (portions of the LTS) illustrating the truth value of temporal formulas [Mateescu-00].

  EVALUATOR 3.0 was developed jointly with Mihaela Sighireanu using the OPEN/CAESAR environment, and consists of about 10,000 lines of code (SYNTAX/FNC-2 and C). The new version EVALUATOR 3.6 uses the BES resolution algorithms provided by the CAESAR_SOLVE library. Several libraries of derived temporal operators were also developed, which encode the operators of ACTL and a set of generic property patterns described in ACTL and in regular alternation-free mu-calculus. Moreover, the model checker is used in a tool environment for verification and performance evaluation of multimedia systems.

  EVALUATOR 3.x was used for verifying several industrial critical applications:

  Air traffic control system General Packet Radio Service (GPRS) SPLICE coordination architecture Steam-boiler system Distributed locker system Truck lifting system Dynamic reconfiguration protocol for mobile agents Checkpointing Algorithms in Distributed Systems AIDA (Automatic In-Flight Data Acquisition) system JavaSpaces shared data space architecture Needham-Schroeder public key authentication protocol Replication features of the Splice architecture Positive Acknowledgement Retransmission (PAR) protocol Jackal distributed shared memory implementation of Java Parallel programs developed using JavaSpacesTM Agent-based dynamic online auction protocol Pragmatic General Multicast (PGM) protocol Asynchronous circuit for Data Encryption Standard (DES) Chilean Electronic Invoices System

  Fair Payment Protocol Negotiation among Web Services Turntable System for Drilling Products Fair Non-Repudiation Protocol Fractal Components Fault-Tolerant Erlang Programs Software Components Automatic Document Feeder Digital Rights Management (DRM) Protocol Observational Determinism for Security Protocols Asynchronous Network-on-Chip .Net On-Line Sale Application Dining Cryptographers and Electronic Voting Scheme Erlang's Open Telecom Platform Library IEEE 1394 Tree Identify Protocol Dutch Rijnland Internet Election System Adaptors between Evolving Components Verification and adaptation of WF/.NET components Specification and analysis of a Web service for GPS navigation

• BISIMULATOR [MO-08-a, MO-08-b, Mateescu-06-a, BDJM-05, Mateescu-03-a] is an on-the-fly equivalence checker comparing two LTSs modulo a given equivalence or preorder relation. The tool currently provides seven equivalence relations and their associated preorders: strong, branching, observational, tau*.a, safety, trace, and weak trace. BISIMULATOR works by translating the verification problem in terms of the on-the-fly resolution of a BES. It is also able to generate counterexamples (acyclic graphs containing distinguishing sequences) illustrating the non equivalence of two LTSs.

  BISIMULATOR was developed using the OPEN/CAESAR environment, and consists of about 23,000 lines of C code. The tool uses the BES resolution algorithms provided by the CAESAR_SOLVE library.

  BISIMULATOR was used for verifying several industrial critical applications:

  • Asynchronous Network-on-Chip
  • Registrar Entity for the Session Initiation Protocol
  • Dutch Rijnland Internet Election System

Committees

• TACAS'2005, TACAS'2009 (11th, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

• FMICS'2001, FMICS'2003, FMICS'2004, FMICS'2005, FMICS'2006, FMICS'2007, FMICS'2008 (6th, 8th-13th International Workshop on Formal Methods for Industrial Critical Systems)

• PDMC'2007, PDMC'2008, PDMC'2009 (6th-8th International Workshop on Parallel and Distributed Methods in verifiCation)

• EWSA'2004, EWSA'2005, EWSA'2006 (1st-3rd European Workshop on Software Architectures)

• VVEIS'2003, VVEIS'2004, VVEIS'2005, MSVVEIS'2006 (1st-4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems)

• ICSEA'2006, ICSEA'2007, ICSEA'2008 (1st-3rd International Conference on Software Engineering Advances)

• MSR'2007 (6ème Colloque Francophone sur la modélisation des systèmes réactifs). Member of the organisation committee.

• CAL'2006 (1ère Conférence Francophone sur les Architectures Logicielles)

• ICCGI'2006 (International Conference on Computing in the Global Information Technology)

• ETR'2005 (Ecole d'Eté Temps Réel 2005)

• SoftMC'2003 (2nd International Workshop on Software Model Checking)

Awards

• Information Technology Award attributed by Fondation Rhône-Alpes Futur for the EVALUATOR 3.0 model checker and its industrial applications (Lyon, France, November 21, 2002).

Publications

Journals:

• A Service-Oriented Architecture for Integrating the Modeling and Formal Verification of Genetic Regulatory Networks.
  P. T. Monteiro, E. Dumas, B. Besson, R. Mateescu, M. Page, A. T. Freitas, and H. de Jong, BMC Bioinformatics 10(450), 2009.


• Formal Modeling and Discrete-Time Analysis of BPEL Web Services.
  R. Mateescu and S. Rampacek, International Journal of Simulation and Process Modelling 4(3-4):183-194, 2008.


• Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks.
  P.T. Monteiro, D. Ropers, R. Mateescu, A.T. Freitas, and H. de Jong, Bioinformatics 24(16):i227-i233, 2008.


• CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems.
  R. Mateescu Springer International Journal on Software Tools for Technology Transfer (STTT) 8(1):37-56, February 2006.


• Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli.
  G. Batt, D. Ropers, H. de Jong, J. Geiselmann, R. Mateescu, M. Page, and D. Schneider, Bioinformatics 21(Suppl-1):i19-i28, 2005.


• Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones.
  R. Mateescu, Technique et science informatiques 22(4):461-495, 2003.


• Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus.
  R. Mateescu and M. Sighireanu, Science of Computer Programming 46(3):255-281, March 2003.


• Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS.
  M. Sighireanu and R. Mateescu, Springer International Journal on Software Tools for Technology Transfer (STTT) 2(1):68-88, December 1998.


• Vérification de systèmes répartis : l'exemple du protocole BRP.
  R. Mateescu, Technique et science informatiques 16(6):725-751, June 1997.

Book chapters:

• Specification and Analysis of Asynchronous Systems using CADP.
  R. Mateescu, Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, chapter 5, pages 141-170. ISTE publishing / John Wiley, January 2008.


• Modélisation et analyse de systèmes asynchrones avec CADP.
  R. Mateescu, Systèmes temps réel 1 - techniques de description et de vérification, IC2 treatise, chapter 5, pages 151-180. Lavoisier, June 2006.

Conferences and workshops:

• Partial Order Reductions using Compositional Confluence Detection.
  F. Lang and R. Mateescu, Proceedings of the 16th International Symposium on Formal Methods FM'2009 (Eindhoven, The Netherlands), Lecture Notes in Computer Science vol. 5850, pages 157-172. Springer Verlag, November 2009.


• Modeling Multiprocessor Cache Protocol Impact on MPI Performance.
  G. Chehaibar, M. Zidouni, and R. Mateescu, Proceedings of the 2009 IEEE International Workshop on Quantitative Evaluation of Large-Scale Systems and Technologies QuEST'09 (Bradford, UK). IEEE Computer Society Press, May 2009.


• Hierarchical Adaptive State Space Caching based on Level Sampling.
  R. Mateescu and A. Wijs, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'09 (York, UK), Lecture Notes in Computer Science vol. 5505, pages 215-229. Springer Verlag, March 2009.


• Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques.
  R. Mateescu, P. Poizat, and G. Salaün, Proceedings of the 6th International Conference on Service Oriented Computing ICSOC'08 (Sydney, Australia), Lecture Notes in Computer Science vol. 5364, pages 84-99. Springer Verlag, December 2008.


• Computation Tree Regular Logic for Genetic Regulatory Networks.
  R. Mateescu, P. T. Monteiro, E. Dumas, and H. de Jong, Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis ATVA'08 (Seoul, South Korea), Lecture Notes in Computer Science vol. 5311, pages 48-63. Springer Verlag, October 2008.


• Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks
  P. T. Monteiro, D. Ropers, R. Mateescu, A. T. Freitas, and H. de Jong, Proceedings of the 7th European Conference on Computational Biology ECCB'08 (Cagliari, Sardinia-Italy), pages 227-233. September 2008.


• Improved On-the-Fly Equivalence Checking using Boolean Equation Systems.
  R. Mateescu and E. Oudot, Proceedings of the 15th International SPIN Workshop on Model Checking of Software SPIN'2008 (Los Angeles, USA), Lecture Notes in Computer Science vol. 5156, pages 196-213. Springer Verlag, August 2008.


• Temporal Logic Patterns for Querying Qualitative Models of Genetic Regulatory Networks
  P. T. Monteiro, D. Ropers, R. Mateescu, A. T. Freitas, and H. de Jong, Proceedings of the 18th European Conference on Artificial Intelligence ECAI'08 (Patras, Greece), pages 229-233. IOS Press, July 2008.


• Formal Modeling and Discrete-Time Analysis of BPEL Web Services.
  R. Mateescu and S. Rampacek, Proceedings of the 4th International Workshop on Enterprise and Organizational Modeling and Simulation EOMAS'08 (Montpellier, France), Lecture Notes in Business Information Processing vol. 10, pages 179-193. Springer Verlag, June 2008. SIGMAS best paper award.


• Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems.
  R. Mateescu and E. Oudot, Proceedings of the 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2008 (Anaheim, CA, USA), pages 73-74. IEEE Computer Society Press, June 2008. Short paper.


• A Model Checking Language for Concurrent Value-Passing Systems.
  R. Mateescu and D. Thivolle, Proceedings of the 15th International Symposium on Formal Methods FM'2008 (Turku, Finland), Lecture Notes in Computer Science vol. 5014, pages 148-164. Springer Verlag, May 2008.


• Behavioral Adaptation of Component Compositions based on Process Algebra Encodings.
  R. Mateescu, P. Poizat, and G. Salaün, Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering ASE'2007 (Atlanta, Georgia, USA), pages 385-388. ACM Press, November 2007.


• CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes.
  H. Garavel, F. Lang, R. Mateescu, and W. Serwe, Proceedings of the 19th International Conference on Computer Aided Verification CAV'2007 (Berlin, Germany), volume 4590 of Lecture Notes in Computer Science, pages 158-163. Springer Verlag, July 2007.


• DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation.
  H. Garavel, R. Mateescu, D. Bergamini, A. Curic, N. Descoubes, C. Joubert, I. Smarandache-Sturm, and G. Stragier, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006 (Vienna, Austria), volume 3920 of Lecture Notes in Computer Science, pages 445-449. Springer Verlag, March-April 2006.


• Distributed On-the-Fly Model Checking and Test Case Generation.
  C. Joubert and R. Mateescu, Proceedings of the 13th International Workshop on Model Checking of Software SPIN'2006 (Vienna, Austria), volume 3925 of Lecture Notes in Computer Science, pages 126-145. Springer Verlag, March-April 2006.


• On-the-Fly State Space Reductions for Weak Equivalences.
  R. Mateescu, Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems FMICS'05 (Lisbon, Portugal), pages 80-89. ACM Press, September 2005.


• Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach.
  G. Batt, D. Ropers, H. de Jong, J. Geiselmann, R. Mateescu, M. Page, and D. Schneider, Proceedings of the Proceedings of the 19th International Joint Conference on Artificial Intelligence IJCAI'05 (Edinburgh, Scotland), July-August 2005.


• BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking.
  D. Bergamini, N. Descoubes, C. Joubert and R. Mateescu, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland), volume 3440 of Lecture Notes in Computer Science, pages 581-585. Springer Verlag, April 2005.


• Distributed Local Resolution of Boolean Equation Systems.
  C. Joubert and R. Mateescu, Proceedings of the 13th Euromicro Conference on Parallel, Distributed and Network-Based Processing PDP'2005 (Lugano, Switzerland), IEEE Computer Society Press, February 2005.


• Distributed On-the-Fly Equivalence Checking.
  C. Joubert and R. Mateescu, Proceedings of the 3rd Workshop on Parallel and Distributed Methods for Verification PDMC'2004 (London, UK), Electronic Notes in Theoretical Computer Science (ENTCS) 28(3), September 2004.


• Model Checking for Software Architectures.
  R. Mateescu, Proceedings of the 1st European Workshop on Software Architecture EWSA'2004 (St Andrews, Scotland), volume 3047 of Lecture Notes in Computer Science, pages 219-224. Springer Verlag, May 2004. Position paper.


• SEQ.OPEN: A Tool for Efficient Trace-Based Verification.
  H. Garavel and R. Mateescu, Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN'2004 (Barcelona, Spain), volume 2989 of Lecture Notes in Computer Science, pages 150-155. Springer Verlag, April 2004.


• Model Checking Genetic Regulatory Networks using GNA and CADP.
  G. Batt, D. Bergamini, H. de Jong, H. Garavel, and R. Mateescu, Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN'2004 (Barcelona, Spain), volume 2989 of Lecture Notes in Computer Science, pages 156-161. Springer Verlag, April 2004.


• Calculating Tau-Confluence Compositionally.
  G. Pace, F. Lang, and R. Mateescu, Proceedings of the 15th International Conference on Computer Aided Verification CAV'2003 (Boulder, Colorado, USA), volume 2725 of Lecture Notes in Computer Science, pages 446-459. Springer Verlag, July 2003.


• On-the-Fly Verification using CADP.
  R. Mateescu, Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2003 (Trondheim, Norway), volume 80 of Electronic Notes in Theoretical Computer Science (ENTCS), June 2003. Invited paper.


• A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems.
  R. Mateescu, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland), volume 2619 of Lecture Notes in Computer Science, pages 81-96. Springer Verlag, April 2003.


• Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems.
  R. Mateescu, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2002 (Grenoble, France), volume 2280 of Lecture Notes in Computer Science, pages 281-295. Springer Verlag, April 2002.


• Compiler Construction using LOTOS NT.
  H. Garavel, F. Lang, and R. Mateescu, Proceedings of the International Conference on Compiler Construction CC'2002 (Grenoble, France), volume 2304 of Lecture Notes in Computer Science, pages 9-13. Springer Verlag, April 2002.


• An Overview of CADP 2001.
  H. Garavel, F. Lang, and R. Mateescu, European Association for Software Science and Technology (EASST) Newsletter volume 4, pages 13-24, August 2002.


• Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications.
  M. Aguilar Cornejo, H. Garavel, R. Mateescu, and N. de Palma, Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems DAIS'2001 (Krakow, Poland), pages 229-242. Kluwer Academic Publishers, September 2001.


• Parallel State Space Construction for Model-Checking.
  H. Garavel, R. Mateescu, and I. Smarandache, Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), volume 2057 of Lecture Notes in Computer Science, pages 217-234. Springer Verlag, May 2001.


• Formal Specification of Checkpointing Algorithms.
  G. Godza, V. Cristea, and R. Mateescu, Proceedings of the 13th International Conference on Control Systems and Computer Science CSCS 13 (Bucharest, Romania). Polytechnic University of Bucharest, May 2001.


• Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus.
  R. Mateescu and M. Sighireanu, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), pages 65-86. GMD/FOKUS, April 2000.


• Efficient Diagnostic Generation for Boolean Equation Systems.
  R. Mateescu, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2000 (Berlin, Germany), volume 1785 of Lecture Notes in Computer Science, pages 251-265. Springer Verlag, March 2000.


• Model Checking for Managers.
  W. Janssen, R. Mateescu, S. Mauw, P. Fennema, and P. van der Stappen, Proceedings of the 6th International SPIN Workshop on Practical Aspects of Model Checking (Toulouse, France), volume 1680 of Lecture Notes in Computer Science, pages 92-107. Springer Verlag, September 1999.


• Verification of Temporal Properties of Processes in a Setting with Data.
  J.F. Groote and R. Mateescu, Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology AMAST'98 (Amazonia, Brazil), volume 1548 of Lecture Notes in Computer Science, pages 74-90. Springer Verlag, January 1999.


• Verifying Business Processes using SPIN.
  W. Janssen, R. Mateescu, S. Mauw, and J. Springintveld, Proceedings of the SPIN'98 International Workshop (Paris, France), pages 21-36. ENST Paris, November 1998.


• Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus.
  R. Mateescu, Proceedings of the 2nd International Workshop on Verification, Model Checking and Abstract Interpretation VMCAI'98 (Pisa, Italy), September 1998.


• XTL: A Meta-Language and Tool for Temporal Logic Model-Checking.
  R. Mateescu and H. Garavel, Proceedings of the International Workshop on Software Tools for Technology Transfer STTT'98 (Aalborg, Denmark), July 1998.


• Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS.
  M. Sighireanu and R. Mateescu, Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997.


• CADP'97 - Status, Applications and Perspectives.
  H. Garavel, M. Jorgensen, R. Mateescu, C. Pecheur, M. Sighireanu and B. Vivien, Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997.


• CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox.
  J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, Proceedings of the 8th International Conference on Computer-Aided Verification CAV'96 (New Brunswick, NJ, USA), volume 1102 of Lecture Notes in Computer Science, pages 437-440. Springer Verlag, August 1996.


• Formal Description and Analysis of a Bounded Retransmission Protocol.
  R. Mateescu, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), June 1996.


• Another Way Towards a Concurrent Programming Environment.
  M. Dobre and R. Mateescu, Proceedings of the 10th International Conference on Control Systems and Computer Science CSCS 10 (Bucharest, Romania), volume 2, pages 302-309. Polytechnic University of Bucharest, May 1995.

Reports:

• Extending SPARQL with Temporal Logic.
  R. Mateescu, S. Meriot, and S. Rampacek, INRIA Research Report RR-7056, October 2009.


• Verification of Temporal Properties of Processes in a Setting with Data.
  J.F. Groote and R. Mateescu, CWI Technical Report SEN-R9804, Amsterdam, The Netherlands, May 1998.


• From AMBER to Promela: A Translation and its Application to Business Processes.
  W. Janssen, R. Mateescu, S. Mauw, and J. Springintveld, Testbed Report, Telematics Institute, Enschede, The Netherlands, May 1998.


• French-Romanian Proposal for Capture of Requirements and Expression of Properties in E-LOTOS Modules. H. Garavel and R. Mateescu, Rapport SPECTRE 96-04, VERIMAG, Grenoble, May 1996. Input document [KC4] to the ISO/IEC JTC1/SC21/WG7 Meeting on Enhancements to LOTOS (1.21.20.2.3), Kansas City, Missouri, USA, May 1996.

Thesis:

• Composants génériques pour l'analyse des systèmes de transitions.
  R. Mateescu, Habilitation à Diriger les Recherches, Institut National Polytechnique de Grenoble, septembre 2007.


• Vérification des propriétés temporelles des programmes parallèles.
  R. Mateescu, Thèse de Doctorat, Institut National Polytechnique de Grenoble, avril 1998.


• Définition et compilation d'un méta-langage pour l'implémentation des logiques temporelles.
  R. Mateescu, Mémoire de DEA, Institut National Polytechnique de Grenoble, juin 1994.

Back to the VASY Home Page