Navigation:

Recent activities:

23 Oct 2009: Release of ZB2SMT, a Z and B verification engine, available at http://www.consiste.dimap.ufrn.br/projetos/zb2smt/.

Affiliated to:

Instituto Nacional de Ciência e Tecnologia para Engenharia de Software

Formal Methods and Languages Research Laboratory

The Formal Methods and Research Laboratory (ForAll) is a research group of the Department of Informatics and Applied Mathematics (DIMAp) from Federal University of Rio Grande do Norte (UFRN). It was created in October 2008 and is being formally registered to Brazilian's National Center for Research and Development (CNPq). 


ForAll develops research on formal languages and techniques for the specification, design and verification of software and hardware. Specific lines of research include:
  • rigorous model-based design;
  • refinement strategies and tactics;
  • satisfiability modulo theory solvers;
  • verification of web service compositions;
  • automatic code generation.
The members of the ForAll group are associated to INES, the Brazilian National Institute of Science and Technology for Software Engineering.

The laboratory provides internships and grants to students from UFRN's Doctoral Course in Computer Science and Master Course in Systems and Computing delivered within the Graduate Program in Systems and Computing (PPgSC), and undergraduate courses in Computer Science (CCC), Computer Engineering (EngComp) and Software Engineering.

Key technologies: UML, the B method, CSP, Circus, SMT solver.