Robert Clarisó Viladrosa Estudis d'Informàtica, Multimèdia i Telecomunicació Universitat Oberta de Catalunya Rambla del Poblenou 156, Office 212 08018 Barcelona, Spain E-mail:  rclariso (a) uoc dot edu Phone:  +34-93-3263410 Fax:      +34-93-3568822

Affiliation

• Lecturer at the Universitat Oberta de Catalunya (UOC).
  
• Member of the GRES-UOC and GMC research groups.

Teaching

• Compilers: UPC - Spring 2006, UOC - fall 2005 until now
• Automata theory: UOC - fall 2005 until now, UAB - fall 2006 until spring 2011
• Data structures: UOC - fall 2006 until spring 2008

Research interests

• Formal methods in Software Engineering
  • Verification of UML models [The UMLtoCSP tool].
• Formal verification
  • Program static analysis
  • Abstract interpretation
  • Timing analysis of concurrent systems
• Numerical properties and abstract domains [image]
  • Convex polyhedra
  • The octahedron abstract domain

Scientific events

• TAP 2012: 6th International Conference on Tests and Proofs. Prague, Czech Republic, May 31-July 1 (co-located with TOOLS Europe 2012 and ICMT'2012).

• OCL'2011: International Workshop on OCL and Textual Modelling. Zurich, Switzerland, June 29 2011. Co-chair with Jordi Cabot, Martin Gogolla and Burkhart Wolff.
• TAP'2011: 5th International Conference on Tests and Proofs. Zurich, Switzerland, June 27-July 1 2011 (co-located with TOOLS Europe 2011 and ICMT'2011).
• ACSD'2011: 11th International Conference on the Application of Concurrency to System Design. Kanazawa, Japan, June 20-24 2011 (co-located with PETRI NETS'2011).
• MELO'2011: Model-Driven Engineering, Logic and Optimization: friends or foes? Birmingham, UK, June 6 2011 (co-located with ECMFA'2011).
• JISBD'2011: XVI Jornadas de Ingeniería del Software y Bases de Datos. A Coruña, Spain, 5-8 September 2011 (co-located with PROLE'2011 and JCIS'2011).
• OCL'2010: Workshop on OCL and Textual Modelling. Oslo, Norway, October 3-8 2010 (part of MODELS'2010).
• MDI'2010: 1st Workshop on Model-Driven Interoperability. Oslo, Norway, October 3-8 2010 (part of MODELS'2010).
• DSDM'2010: VII Taller sobre Desarrollo de Software Dirigido por Modelos. Valencia, Spain, September 7 2010 (part of JISBD'2010).

Publications

   DBLP - ResearcherID - ACM Portal - Google Scholar - MSN Academic Search

1. R. Clarisó. Abstract Interpretation Techniques for the Verification of Timed Systems. PhD Thesis, Department of Software (LSI), Technical University of Catalonia (UPC). September 2005. [ PDF ]
   PhD. advisor: Jordi Cortadella

1. J. Cabot, R. Clarisó, E. Guerra and J. de Lara. Verification and Validation of Declarative Model-to-Model Transformations Through Invariants. Journal of Systems and Software, 83(2): 283-302, 2010. [ PDF preprint, Publisher site ]
2. J. Cabot, R. Clarisó, E. Guerra and J. de Lara. A UML/OCL Framework for the Analysis of Graph Transformation Rules. Software and Systems Modeling. 9(3): 335-357, 2010. [ PDF preprint, Publisher site ]
3. R. Clarisó and J. Cortadella.The octahedron abstract domain. Science of Computer Programming, 64(1):115-139, January 2007. [ PDF preprint, Publisher site ]
4. R. Clarisó and J. Cortadella.Verification of Concurrent Systems with Parametric Delays using Octahedra. Fundamenta Informaticae,78(1):1-33, July 2007. [ PDF preprint, Publisher site ]

1. A. Shaikh, R. Clarisó, U.K. Wiil, N. Memon. Verification-driven slicing of UML/OCL Models. In Proc. 25th IEEE/ACM International Conference on Automated Software Engineering, pages 185-194, ACM, 2010. [ PDF ]
2. J. Cabot, R. Clarisó, E. Guerra and J. de Lara. Synthesis of OCL Pre-conditions for Graph Transformation Rules. In Proc. 3rd International Conference on Model Transformation (ICMT'2010), volume 6142 of Lecture Notes in Computer Science, pages 45-60, Springer-Verlag, 2010. [ PDF ]   © Springer-Verlag LNCS
3. J. Cabot, R. Clarisó and D. Riera. Verifying UML/OCL Operation Contracts. In Proc. 7th International Conference on Integrated Formal methods (iFM'2009), volume 5423 of Lecture Notes in Computer Science, pages 40-55, Springer-Verlag, Februrary 2009. [ PDF ]   © Springer-Verlag LNCS
4. J. Cabot, R. Clarisó, E. Guerra and J. de Lara. An Invariant-Based Method for the Analysis of Declarative Model-to-Model Transformations. In Proc. 11th International Conference on Model-Driven Engineering Languages and Systems (MODELS'2008), volume 5301 of Lecture Notes in Computer Science, pages 37-52, Springer-Verlag, September 2008. [ PDF ]   © Springer-Verlag LNCS
5. J. Cabot, R. Clarisó, E. Guerra and J. de Lara. Analysing Graph Transformation Rules Through OCL. In Proc. International Conference on Model Transformation (ICMT'2008), volume 5063 of Lecture Notes in Computer Science, pages 225-239, Springer-Verlag, July 2008. [ PDF ]   © Springer-Verlag LNCS
6. R. Clarisó and J. Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In Proc. 5th International Conference on Application of Concurrency to System Design (ACSD'05), pages 122-131, IEEE Computer Society Press. June 2005. [ PDF ] [ BibTeX ] © IEEE
7. R. Clarisó, E. Rodríguez-Carbonell and J. Cortadella. Derivation of Non-structural Invariants of Petri Nets Using Abstract Interpretation. In Proc. 26th International Conference On Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN'05), volume 3536 of Lecture Notes in Computer Science, pages 188-207, Springer-Verlag, June 2005. [ PDF ] [ BibTeX ] © Springer-Verlag LNCS
8. R. Clarisó and J. Cortadella. The octahedron abstract domain. In 11th Static Analysis Symposium (SAS'04), volume 3148 of Lecture Notes in Computer Science, pages 312-327. Springer-Verlag, August 2004. [ PS ] [ PDF ] [ BibTeX ]   © Springer-Verlag LNCS
9. R. Clarisó and J. Cortadella. Verification of timed circuits with symbolic delays. In Proc. Asia and South Pacific Design Automation Conference, pages 628-633. January 2004. [ PS ] [ PDF ] [ BibTeX ]

1. S. Sánchez-Alonso, D. Rodríguez-García, and R. Clarisó. Comparing a fully online course to a blended one: the case of compilers In. Proc. 2nd Workshop on Methods and Cases in Computing Education (MCCE'09), April 2009. [ PDF ]
2. J. Cabot and R. Clarisó. UML/OCL Verification in Practice. In Proc. 1st International Workshop on Challenges in Model-Driven Software Engineering (ChaMDE'2008), September 2008. [ PDF ]
3. J. Cabot, R. Clarisó and D. Riera. Verification of UML/OCL Class Diagrams Using Constraint Programming. In Proc. ICST Workshop on Model Driven Engineering, Verification and Validation: Integrating Verification and Validation in MDE (MoDeVVa'2008), April 2008. [ PDF ]
4. J. Cabot, R. Clarisó and D. Riera. UMLtoCSP: A Tool For the Formal Verification of UML/OCL Models Using Constraint Programming. Tool demo in 22nd ACM/IEEE International Conference on Automated Software Engineering (ASE'07), pages 547-548. November 2007. [ PDF ]
5. R. Clarisó and J. Cortadella. Verification of parametric timed circuits using octahedra. In Proc. International Workshop on Designing Correct Circuits (DCC'05). March 2004.
6. R. Clarisó and J. Cortadella. Verification of timed circuits with symbolic delays. In Proc. of the 12th International Workshop on Logic and Synthesis (IWLS'03), pages 310-317. May 2003.
7. R. Clarisó and J. Cortadella. Symbolic timing analysis for the verification of asynchronous circuits. In 3rd Workshop of the Working Group on Asynchronous Circuit Design (ACiD-WG'03). January 2003.
8. R. Clarisó, J. Cortadella, A. Kondratyev, L. Lavagno, C. Passerone and Y. Watanabe. Synthesis of embedded software for reactive systems. Proc. 2nd International Workshop on Integration of Specification Techniques for Applications in Engineering (INT'02), pages 2-20. April 2002.

1. R. Clarisó. Formal Proof: Understanding, writing and evaluating proofs. January 2010. [ PDF ]
2. R. Clarisó. Entorn per optimització i generació de codi (Catalan, "Code optimization and generation environment"). April 2000. [ PDF ]
   Description of an optimizing compiler designed for academic use in Compiler courses. Project to achieve the degree of Enginyer en Informàtica.

Links

• Abstract interpretation
  • Patrick Cousot - ENS Paris, France
  • Radhia Cousot - CNRS, France
  • Nicolas Halbwachs - Verimag, France
  • Bertrand Jeannet - IRISA, France
  • Roberto Bagnara - Univ. Parma, Italy
  • Antoine Miné - ENS Paris, France
  • Enric Rodríguez Carbonell - UPC
• Convex polyhedra resources
  • Frequently asked questions in polynomial computation
  • PPL - The Parma Polyhedra Library
  • New Polka convex polyhedra library
  • Polylib and its successor PolyLib
  • polymake
• Tools for the analysis of timed systems
  • Kronos - Verification of timed automata
  • RED - Verification of timed automata and hybrid automata
  • HyTech - Verification of hybrid automata
  • TReX - Verification of parametric timed automata with several extensions (e.g. counters)
  • CMC - Compositional model-checking of timed automata
  • Difference Decision Diagrams (DDD) - Verification of timed guarded commands
  • UPPAAL - Verification of timed automata with several extensions (e.g. counters, arrays)
• Scientific references
  • IEEExplore
  • CiteSeer Research Index
  • Bibliotecnica - UPC library catalog
  • Google Scholar
  • DBLP Bibliography
  • ISI Web of Knowledge