Marcio Teixeira Oliveira
3251 Woodcrest Dr
San Jose, CA, 95118
M.Sc. Computer Science, University of British Columbia, fall 2003
B.Sc. Computer Science, Federal University of Minas Gerais, Brazil, 1999
M. Sc. Thesis Research
Title: High-Level Specification and Automatic Generation of IP Interface Monitors
Abstract: A central problem in functional verification is to check that a
circuit block is producing correct outputs while enforcing that the environment
is providing legal inputs. To attack this problem, several researchers have
proposed monitor-based methodologies, which offer many benefits. We have
developed a novel, high-level specification style for these monitors, along
with a linear-size, linear-time translation algorithm into monitor circuits.
To demonstrate the advantage of our specification style, we have specified
monitors for various versions of the Sonics OCP protocol as well as the
AMBA AHB protocol, and have developed a prototype tool that automatically
translates specifications into Verilog or VHDL monitor circuits.
Advisor: Alan J. Hu
Completion Date: August, 2003
Research and Industry Experience
Formal Verification/CAD Engineer, NVIDIA Corporation (Santa Clara, USA), in 12/2002 - present
Responsible for defining and applying the formal verification methodology in all NVIDIA projects. Developed CAD tools and libraries in C++, Perl, TCL, including parsers and design efficiency analyzers.
Research in symbolic model checking and formal verification techniques with
Prof. Sergio Campos, Federal University of Minas Gerais, in 1998-1999
As a B.Sc. thesis, we introduced a new model of time (semi-continuous time),
in which the passage of time is dissociated from the occurrence of events.
This model was later implemented in the Verus tool, a symbolic model checker
for real time systems. I migrated the tool from David Long's BDD package to
CUDD and together with Prof. Sergio Campos, we implemented counter-examples
and witnesses in Verus.
Research in adaptable exhibition of MPEG video for mobile environments with
Prof. Antonio Loureiro, Federal University of Minas Gerais, in 1999
Together with 2 other students, we developed a prototype tool to remove MPEG 1
B-frames, according to network available bandwidth, and encrypt the result to
be transmitted over a wireless network. The tool performs both operations in
Web Robot project with Prof. Sergio Campos, Federal University of Minas Gerais, in 2000
Together with 1 other student, we developed and implemented new algorithms for
a web crawler robot based on multi threads and without a central "URL to fetch"
Telemar and Federal University of Minas Gerais Joint Project, in 01/1999 - 08/2000
Telemar is one of the biggest Brazilian telecommunication companies.
C/Java developer in a project for telecommunication network management.
Reference Center for Applied Informatics, Federal University of Minas Gerais, in 06/1997 - 12/1998
C, Java and WEB developer for telecommunication engineering applications.
Internship at Start Software Brasil, in 01/1997 - 05/1997
Visual Basic developer in a multimedia digital photo album system.
Teaching Assistant for CPSC252 (Program Design and Data Structures for Engineers), UBC, 2000
I was the teaching assistant for three labs of about 35 students each.
Teaching Assistant for CPSC315 (Introduction to Operating Systems), UBC, 2001
I was the marking coordinator and I was responsible for answering student questions about assignments and projects.
Teaching Assistant for CPSC252 (Program Design and Data Structures for Engineers), UBC, 2001
I was the teaching assistant for a lab of about 30 students.
Marcio T. Oliveira, Alan J. Hu. "High-Level Specification and Automatic
Generation of IP Interface Monitors", 39th ACM/IEEE Design Automation
Conference , 2002, to appear.
Daniela A. S. dos Santos, Marcio T. Oliveira, Reuber G. Duarte, Antonio Alfredo
F. Loureiro, Geraldo Robson Mateus and Berthier Ribeiro-Neto. "Adaptable
Exhibition of MPEG Video for Mobile Environments" (original work in Portuguese),
in the Proceedings of the III Brazilian Workshop on Wireless Communication and
Mobile Computing. Recife, PE, Brazil. August 2001
S. Campos, M. Teixeira, M. Minea, A. Kuehlmann, E. Clarke. "Model Checking
Semi-Continuous Time Models Using BDDs", in the Proceedings of the
International Workshop on Symbolic Model Checking. Trento, Italy. July 1999.
Available on request.