Português English

Research Groups | Computer Fundamentals and Formal Methods

The research group in Fundamentals of Computing and Formal Methods has been working in research and development of techniques to ensure correction in software development for several areas of Computer Science. To ensure that the development of software is in fact a solution to the problem proposed, one should: build a solution model (specification) using a formal language; perform mathematical tests to ensure that this model has the required properties (checking), analyze whether the proposed solution is acceptable in terms of performance, and indicate  the best strategies to be implemented; validate the model through simulations, perform software development that ensures that the implementation is correct (correct code generation).


Research Themes

  • Algorithms and optimization: external-memory algorithm design and data stream based algorithms required for processing large volumes of data. Mathematical modeling of combinatorial optimization problems and development of efficient algorithms (optimal and heuristic) for the resolution of those problems.
  • Software Verification and Testing: Study of techniques for verifying correctness and functional properties of software validation techniques.
  • Specification and Software Design Languages: Investigation of languages for the various phases of software development and applications (e.g. mobile code applications, databases, reactive systems). Approaches for modifying programs and specifications preserving their original behavior.
  • Specification and Management of Process oriented Software Design: Study, development and evaluation of tehcniques and methods for specifying, planning and managing process oriented software design.
  • Analytical and Complex System Simulation Methods:  quantitative analysis of stochastic and deterministic complex systems in biological, physical and social contexts.
  • Webgraph Analysis and Modelling:  Development of computational and analytical models for the temporal evolution of the Web. These models can be used as basis for testing correctness and efficiency of new algorithms for the Webgraph.
  • Logics applied to Computing: the use of logics for specification, verification and the study of properties of computational systems.
  • Cognitive Computing: definition of computational models that incorporate reasoning and machine learning.
  • Natural Computing: development of computational models inspired in nature and modeling of complex systems.
  • Specification and verification of Embedded Systems: use of formal methods in the design of embedded software.
  • Computational complexity: classify computational problems according to their inherent difficulty, and relating those classes to each other

Recent Research Projects

  • AC-RS – Development of a Center for Digital Certification in Rio Grande do Sul. Participants: UFRGS / Procergs / Banrisul / ACRS. Funded by: ITI. From 2006.
  • PLATUS – Formal development of and simulation of reactive systems. Funded by: CNPq. From 2004 to 2007
  • IQ-Mobile – Improving the Quality of Open Systems with Code Mobility through Rigorous Development. Co-Participants:PUCRS/CNR(Italy)/University of Pisa (Italy). Funded by: CNPq/CNR (Italy). From 2001 to 2004
  • DACHIA – Modeling, Analysis and Development of an Approach for the Construction of High-Quality Internet Applications based on Visual Languages and Formal Methods. Co-Participants: PUCRS/TU Berlin (Germany)/MSB (Germany). Funded by: CNPq/DLR (Germany). From 2003 to 2004
  • Form-X – Data integration – Foundations of query languages in the context of data integration. Funded by: CNPq/FAPERGS. From 2005-2007
  • Characterization of Control Strategies for Heterogeneous Multiagent Systems – Funded by: CAPES-GRICES. From  2005-2007


Recent Research Results

  • Techniques and tools for verification of object-based systems, including real-time systems
  • Specification Techniques for object oriented concurrent and distributed systems
  • Large scale graph generation from the structure of Wikipedia.
  • Prosoft-APSEE  Environment for supporting management and development of process oriented software design. Prosfot-APSEE is currently being developed as an open source version, the WebApsee.
  • Techniques and tools for the specification and verification of mobile code systems.
  • Computational Approach to modeling the evolution of the Webgraph.
  • Three algorithm patents:
  1. Method and Apparatus for Providing a Survivable Network Design;
  2. Method and Apparatus for Updating Dynamic Shortest Path Graphs;
  3. Method and Apparatus for Providing Composite Link Assignment in Network Design.