Formal Specification, Verification and Implementation of Concurrent Real-Time Embedded Systems


INFINIS is a French-Argentinean Laboratory (Laboratoire Internationale Associé) between Centre National de la Recherche Scientifique (CNRS) and Université Paris Diderot, on the one hand, and Consejo Nacional de Investigaciones Cientéficas y Técnicas (CONICET) and the Universidad de Buenos Aires, on the other. It is devoted to research in Computer Science. Specific focus is placed on formal methods, for modeling, verification and development of complex software artifacts.



  • Formal specification and algorithmic verification techniques of infinite-state systems.
  • Design and implementation of concurrent real-time embedded systems.
  • Static analysis aimed at resource usage analysis of Java-like programs.
  • Automated program understanding and validation.


Team members