Bárbara Vieira

Research

Ongoing

CACE's Minho Team is currently developing a deductive verification tool for CAO (programming language under the development in the CACE European Project) which is built on the top of Jessie plug-in part of the Why framework and also included in the Frama-C framework. The CAO language is tuned to the implementation of low-level cryptographic primitives in a way which is close to the notation used in scientific papers and standards.

In the past

- During 3 months, between March 2009 and May 2009, I did an internship at INRIA Saclay,Île-de-France, to work with Proval team. In particular, I started the development of a deductive verification tool for a domain specific languange called CAO, together with Jean-Christophe Filliâtre and Claude Marché.

- Researcher at "Pervasive Retail" Project, from October 2007 to June 2008. This project addressed cryptography and security areas, and was resultant of a cooperation between CCTC and Enabler/Wipro company.

- Internship at Multivector S.A. Company, Braga, Portugal, from March 2007 to September 2007.

Workshops and scientific activities

• - Work packages WP1 and WP2 meeting (CACE project), April 2008,Bristol, UK.
• - WP5 workshop (CACE project), Partner and End user Meeting for Security Policy Specification, July 2008, Porto, Portugal.
• - Summer School on Verification Technology Systems & Applications, Max Planck Institute for Informatics, September 2008, Saarbrucken, Germany.
• - NASA Formal Methods Symposium (NFM 2009), April 2009, Moffett Field, California, USA.
• - Summer School Marktoberdorf 2009 , August 4 to August 16, 2009, Marktoberdorf, Germany.
• - 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2009), November 2-3, 2009, Eindhoven, The Netherlands.
• - 10th International School on Foundations of Security Analysis and Design (FOSAD 2010), September 2010, Bertinory, Italy.
• - 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), September 2010, Pisa, Italy.

Publications

• - Security Policies for Cryptographic Software, CACE Project, Work Package WP5 -- Formal Verification and Validation, Deliverable D5.1. Editor Manuel Barbosa, 2008.
• - Deductive verification of Cryptographic Software, NASA Formal Methods Symposium 2009, from J. Bacelar Almeida, M. Barbosa, J. Sousa Pinto and B. Vieira, 2009.
• - Formal specification language definitions and security policy extensions, CACE Project, Work Package WP5 -- Formal Verification and Validation, Deliverable D5.2. Editor Manuel Barbosa, 2009.
• - Verifying Cryptographic Software Correctness with Respect to Reference Implementations, FMICS 2009, from J. Bacelar Almeida, M. Barbosa, J. Sousa Pinto and B. Vieira, 2009.
  - Machine assisted verification and certification tools, CACE Project, Work Package WP5 -- Formal Verification and Validation, Deliverable D5.3. Editor Manuel Barbosa, 2010.
  - Deductive verification of cryptographic software, NASA Journal of Innovations in Systems and Software Engineering 2010, from J. Bacelar Almeida, M. Barbosa, J. Sousa Pinto and B. Vieira, 2010.
• - A Deductive Verification Platform for Cryptographic Software, 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), from M. Barbosa, J.-C. Filliâtre, J. Sousa Pinto and B. Vieira, 2010.