Robert Clarisó Viladrosa Ph.D. Student Department of Software Technical University of Catalonia Campus Nord, Edifici Omega, Office S108 c/ Jordi Girona Salgado 1-3 08034 Barcelona, Spain E-mail:  rclariso at lsi dot upc dot edu Phone:  +34-93-4137861 Fax:      +34-93-4137833

Affiliation

Research interests

• Program static analysis
  • Abstract interpretation
  • Code optimization
• Analysis and verification of concurrent systems
  • Quasi-Static Scheduling
  • False paths problem in Quasi-Static Scheduling
  • Parametric timing analysis of concurrent systems
• Numerical properties and abstract domains
  • Convex polyhedra
  • The octahedron abstract domain

Publications

1. R. Clarisó and J. Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. To appear in the 5th International Conference on Application of Concurrency to System Design (ACSD'05). June 2005.
2. R. Clarisó, E. Rodríguez-Carbonell and J. Cortadella. Derivation of Non-structural Invariants of Petri Nets Using Abstract Interpretation. To appear in the 26th International Conference On Application and Theory of Petri Nets and Other Models of Concurrency (ATPN'05). June 2005.
3. 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
4. R. Clarisó and J. Cortadella. Verification of parametric timed circuits using octahedra. In Proc. International Workshop on Designing Correct Circuits (DCC'05). March 2004.
5. 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 ]
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.

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