Event Start

About

In 2020, the 23rd edition of Brazilian Symposium on Formal Methods (SBMF) will be held, for the first time, in a virtual format.

The 23rd SBMF is the 2020 edition of a series of events devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event, with an international reputation.

Previous editions

Speakers

Rohit Gheyi

UFCG, Brazil

Talk: Testing Refactoring Implementations

Abstract: Refactoring is a widely used development practice, available in mainstream IDEs. However, testing refactoring implementations is not an easy task since it requires complex input objects, and it is not simple to test all refactoring conditions. In this talk, I will present techniques to test refactoring implementations with respect to overly weak and overly strong conditions. I will also explain our latest approach to evaluate the refactoring mechanics implemented by Eclipse, NetBeans, and JRRT. We detect and report more than 100 compilation errors and behavioral changes in popular IDEs. We also find differences in the refactoring mechanics considered by Eclipse, NetBeans, and JRRT.

Short bio: Rohit Gheyi is an Associate Professor at Federal University of Campina Grande. He received his DSc. in Computer Science in 2007 from Federal University of Pernambuco. He was a visiting scholar at Massachusetts Institute of Technology during his PhD. Gheyi has co-authored more than 80 refereed papers in international conferences and journals. He also participates in research and development projects with partners in industry since 2010. His research interests include software evolution, software testing, formal methods, software product lines, and machine learning.

Nikolaj Bjørner

Microsoft Research, United States

Talk: Navigating the Universe of Z3 Theory Solvers

Abstract: Modular combination of theory solvers is an integral theme in engineering modern SMT solvers. The CDCL(T) architecture provides an overall setting for how theory solvers may cooperate around a SAT solver based on confl􏰂ict driven clause learning. The Nelson-Oppen framework provides the interface contracts between theory solvers for disjoint signatures. In this talk, we provide an update on theories integrated in Z3. We brie􏰂fly review principles of theory integration in CDCL(T) and then examine the theory solvers available in Z3, with special emphasis on two recent solvers: a new solver for arithmetic and a pluggable user solver that allows callbacks to invoke propagations and detect conflicts.

Short Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Network Verification. His current main line of work with Leonardo de Moura and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award, most influential tool paper in the first 20 years of TACAS in 2014, the 2017 Skolem award for the 2007 paper on Efficient E-matching for SMT solvers. Another main line of activities are focused on Network Verification with colleagues in Azure, Karthick Jayaraman, and academia, George Varghese. Previously, he developed the DFSR, Distributed File System - Replication, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.

Martin Leucker

University of Lübeck, Germany

Talk: Formal Verification of Neural Networks may be questionable

Abstract: Machine learning is a popular tool for building state of the art software systems. It is more and more used also in safety critical areas. This demands for verification techniques ensuring the safety and security of machine learning based solutions. However, in this presentation, we argue that the popularity of machine learning comes from the fact that no formal specification exists which renders traditional verification in appropriate. Instead, validation is typically demanded and we present a recent technique that validates certain correctness properties for an underlying recurrent neural network.

Short bio: Martin Leucker is currently a professor at the University of Lübeck, Germany heading the Institute of Software Engineering and Programming Languages. He obtained his Ph. D. at the RWTH Aachen, Germany and afterwards, he worked as a Postdoc at the University of Philadelphia, USA and at the Uppsala University, Sweden. He pursued his habilitation at the TU München, Germany. He is the author of more than 100 peer reviewed conference and journal papers ranging over software engineering, formal methods and theoretical computer science.

Important Dates

31 July, 2020 (extended) Abstract submission deadline.
31 July, 2020 (extended) Full paper submission deadline.
O8 September, 2020 (extended) Authors notification deadline.
02 October, 2020 (extended) Camera-ready copy deadline.
25 November, 2020 to 27 November, 2020 SBMF 2020

Call for papers



Important dates
  • Abstract submission deadline: 31 July, 2020 (extended)
  • Full paper submission deadline: 31 July, 2020 (extended)
  • Authors notification deadline: 08 September, 2020
  • Camera-ready copy deadline: 02 October, 2020


IMPORTANT ANNOUNCEMENT REGARDING COVID-19
In light of the COVID-19 pandemic, the Organising Committee has decided that SBMF 2020 will not take place physically. It will be replaced by a virtual event only. The exact format is still to be decided. Nevertheless, the paper selection process will proceed as planned, and an LNCS proceedings will be prepared as usual.

Publication
Accepted papers will be published, after the conference, in a volume of LNCS. The authors will be requested to complete and sign a consent-to-publish form. Every accepted paper MUST have at least one author registered in the symposium by the time the camera-ready copy is submitted. The registered author is also expected to attend the symposium and present the paper.

A special issue of the Science of Computer Programming Journal (Elsevier) is going to be organised with selected and extended papers from the 23rd Brazilian Symposium on Formal Methods (SBMF 2020).

All questions about submissions should be sent to: sbmf2020@easychair.org
Scope and topics
The aim of SBMF is to provide a venue for the presentation and discussion of high-quality work in formal methods. The topics include, but are not limited to, the following:
  • Applications of formal methods to
    • Software or/and hardware design
    • Software or/and hardware development
    • Software or/and hardware code generation
    • Software or/and hardware testing
    • Software maintenance, evolution or/and reuse
    • Intelligent systems
  • Specification and modelling languages
    • Logic and semantics for specification or/and programming languages
    • Formal methods for timed, real-time, hybrid, or/and safety-critical systems
    • Formal methods for service-oriented, cloud-based, or/and cyber-physical systems
  • Theoretical foundations
    • Domain theory
    • Term rewriting
    • Computational models
    • Type systems and category systems
    • Computation complexity of methods and models
    • Models of time, concurrency, security or/and mobility
  • Verification and validation
    • Abstraction, modularization or/and refinement techniques
    • Static analysis
    • Model checking
    • Theorem proving
    • Software certification
    • Correctness by construction
  • Experience reports
    • Reports on teaching formal methods
    • Reports on industrial application of formal methods

Registration

SBMF and ETMF are sponsored by the Brazilian Computer Society (SBC). SBC is a civil, non-profit association that brings together students, professors, professionals, researchers, and enthusiasts in Computer Science from all over Brazil, being the largest scientific society of this field in South America. With 42 years of existence, SBC stimulates the scientific and technological development of Brazil by promoting digital inclusion, encouraging teaching, research, and development activities in Computer Science in Brazil, and contributing to the formation of Computer Science professionals with social responsibility.

The registration fees for SBMF 2020 and ETMF 2020 are listed below. Students and professionals who are not members of SBC can associate or renew their association with a discount during the registration process. Registering for the conference and becoming a member of SBC (combo) is the most advantageous option for the participant who is not yet a member of SBC since he/she will pay less than the option for non-members and will enjoy the benefits of being a member of SBC.

Registration will be handled by the SBC's ECOS system:

Click here to register!

However, it is recommended to carefully read the information below to know the conditions and deadlines related to the registration. All registration fees are in Brazilian reais (R$/BRL).

Registration Fees

Undergraduate students

Graduate students

Professionals

Additional Fees

Additional Information

Registration + SBC membership (or membership renewal). These categories refer to a discounted value applied when registering for SBMF/ETMF 2020 and joining SBC. This modality was created to make the sum of those benefits cheaper than acquiring each of them separately, thus being the most advantageous option for whom is not yet a member of SBC or is with his/her membership expired or about to expire.

Student registration. Registration fees for students are only available to those who are currently enrolled in undergraduate or graduate courses at Higher Education Institutions and do not apply to post-doc researchers. When registering through the ECOS system, an electronic proof of the student status with affiliation, participant's name, course which he/she is enrolled at, and current date will be required. Only after SBC verifies the document (which can take up to 1 business day to be analyzed) it will be possible to proceed with the payment of registration. To avoid any inconvenience, it is recommended not registering for SBMF/ETMF 2020 in the last day of the registration range. Payment options will be available only after the SBC's validation. Registrants will receive informative e-mails in all stages of their registration for SBMF/ETMF 2020.

Registration for SBMF authors. Papers accepted to SBMF will be published in a volume of LNCS. At least one author (professional or student) of each accepted paper must be registered for SBMF 2020 and pay the author fee. Authors can not use the registration benefits (exemption or 50% discount) granted by SBC to affiliated institutions. The author fee must be paid until October 30, 2020.

Printed proceedings. All registered papers will receive a printed copy of the SBMF 2020 proceedings. Non-author participants interested in printed copies of the conference proceedings must pay the Printed Proceedings additional fee.

Payment options. Registrations can be paid by bank ticket, credit card, debit to a Bank of Brazil account, note of commitment or billing through the ECOS system. Registrations can be made until the last day of SBMF 2020, but payments by debit account and bank ticket will be closed on November 20, 2020. After that date, registration can be paid only by credit card, note of commitment, and billing.

Registrations to be paid by note of commitment or billing. Registrants must access the ECOS system and make their registration by selecting either "Note of commitment" or "Billing" as payment option. Once the payment has been requested, the system will provide the required information that must be in the note of commitment or billing request.

Cancellation policy. Registration cancellation requests made until November 13, 2020 may have a refund of 70% of the amount paid for registration in SBMF / ETMF 2020, the remaining 30% being used to cover administrative costs. After that date, there will be no refund of any paid amount. This policy applies to cancellation of both registration and author fee. To request cancellation, registrants must send an e-mail to faturamento@sbc.org.br.

Benefits of the SBC Membership

Becoming a member of SBC is a way of strengthening it to represent the Computer Science field in several parties. Other reasons to become a member of SBC are:

The specific benefits of each membership category can be found at the SBC website.

Committees

Organizing Committee:

General Chair:
  • Rodrigo Ribeiro (Universidade Federal de Ouro Preto, Brazil)

PC Chairs:
  • Gustavo Carvalho (Universidade Federal de Pernambuco, Brazil)
  • Volker Stolz (Western Norway University of Applied Sciences, Norway)

Steering Comittee:

  • Simone Cavalheiro (Universidade Federal de Pelotas, Brazil)
  • José Fiadeiro (Royal Holloway, University of London, United Kingdom)
  • Tiago Massoni (Universidade Federal de Campina Grande, Brazil)
  • Mohammad Mousavi (University of Leicester, United Kingdom)
  • Adolfo Duran (Universidade Federal da Bahia, Brazil)
  • Phillip Wadler (University of Edinburgh, United Kingdom)

Program Comittee:

  • Adenilso Simão (Universidade de São Paulo, Brazil)
  • Alexandre Mota (Universidade Federal de Pernambuco, Brazil)
  • Aline Andrade (Universidade Federal da Bahia, Brazil)
  • Álvaro Moreira (Universidade Federal do Rio Grande do Sul, Brazil)
  • Ana Cavalcanti (University of York, United Kingdom)
  • Ana Melo (Universidade de São Paulo, Brazil)
  • Anamaria Moreira (Universidade Federal do Rio de Janeiro, Brazil)
  • Andrea Corradini (Università di Pisa, Italy)
  • Arnd Hartmanns (University of Twente, The Netherlands)
  • Augusto Sampaio (Universidade Federal de Pernambuco, Brazil)
  • Christiano Braga (Universidade Federal Fluminense, Brazil)
  • Clare Dixon (University of Liverpool, United Kingdom)
  • Colin Snook (University of Southampton, United Kingdom)
  • David Déharbe (CLEARSY Systems Engineering, France)
  • David Naumann (Stevens Institute of Technology, United States of America)
  • Giovanny Lucero (Universidade Federal de Sergipe, Brazil)
  • Gustavo Carvalho (Universidade Federal de Pernambuco, Brazil)
  • Jim Davies (University of Oxford, United Kingdom)
  • Jim Woodcock (University of York, United Kingdom)
  • Jose Fiadeiro (University of Dundee, United Kingdom)
  • José Oliveira (Universidade do Minho, Portugal)
  • Juliano Iyoda (Universidade Federal de Pernambuco, Brazil)
  • Leila Ribeiro (Universidade Federal do Rio Grande do Sul, Brazil)
  • Leonardo de Moura (Microsoft Research, United States of America)
  • Leopoldo Teixeira (Universidade Federal de Pernambuco, Brazil)
  • Luis Barbosa (Universidade do Minho, Portugal)
  • Manfred Broy (Technische Universität München, Germany)
  • Marcel Oliveira (Universidade Federal do Rio Grande do Norte, Brazil)
  • Márcio Cornélio (Universidade Federal de Pernambuco, Brazil)
  • Maurice ter Beek (Istituto di Scienza e Tecnologie dell’Informazione, Italy)
  • Michael Leuschel (Universität Düsseldorf, Germany)
  • Mohammad Mousavi (University of Leicester, United Kingdom)
  • Nils Timm (University of Pretoria, South Africa)
  • Patrícia Machado (Universidade Federal de Campina Grande, Brazil)
  • Philip Wadler (University of Edinburgh, United Kingdom)
  • Robert Hierons (Brunel University London, United Kingdom)
  • Rohit Gheyi (Universidade Federal de Campina Grande, Brazil)
  • Sidney Nogueira (Universidade Federal Rural de Pernambuco, Brazil)
  • Simone Cavalheiro (Universidade Federal de Pelotas, Brazil)
  • Sofiène Tahar (Concordia University, Canada)
  • Thierry Lecomte (CLEARSY Systems Engineering, France)
  • Tiago Massoni (Universidade Federal de Campina Grande, Brazil)
  • Volker Stolz (Western Norway University of Applied Sciences, Norway)

Submission instructions

We invite submissions of papers with a strong emphasis on formal methods, whether practical or theoretical, in the following categories:
  • 1 - Regular papers (limit of 16 pages);
  • 2 - Journal-first papers (limit of 4 pages).
Page limits include references and any appendices. When submitting the paper, the authors should select the appropriate submission category. Contributions should not be simultaneously submitted for publication elsewhere. They should be written in English and prepared using Springer’s Lecture Notes in Computer Science (LNCS) format.
More information available in the following link:

Papers submitted to Category (1) should present unpublished and original work that has a clear contribution to the state-of-the-art on the theory and practice of formal methods. Papers will be judged by at least three reviewers on the basis of originality, relevance, technical soundness and presentation quality and should contain sound theoretical or practical results. Industry papers should emphasize practical application of formal methods or report on open challenges.

Papers submitted to Category (2) should provide a concise summary of an outstanding journal paper published by the same authors, besides considering an updated reflection about the achieved results: what has been done since the original publication, and what are the current challenges. The submission must explicitly include full bibliographic details (including a DOI) of the journal publication it is based on. The published journal paper must adhere to the following criteria:

  • It is clearly within the scope of the conference.
  • It has been made available in a journal (online or in print) not before 1 January 2018.
  • It is not an extended version of a selected conference paper.
  • It has not been presented at, and is not under consideration for, other journal-first tracks.
Our goal with Category (2) is to further enrich the SBMF program, bringing about results that have been published but not presented in any conference yet. In this way, we want to foster interesting discussions that might be relevant to attendees and authors. Papers submitted to this category will be judged based on the aforementioned recommendations and criteria.

Submissions for all categories should be made via the following link:

Accepted Papers

  • Graphical Calculational proofs in Relational Linear Algebra. Joao Paixao and Pawel Sobocinski.
  • Merging cloned Alloy models with colorful refactorings. Chong Liu, Nuno Macedo and Alcino Cunha.
  • Modeling Big Data Processing Programs. João Batista de Souza Neto, Anamaria Martins Moreira, Genoveva Vargas-Solar and Martin Alejandro Musicante.
  • Optimization of Timed Scenarios. Neda Saeedloei and Feliks Kluzniak.
  • Porting the Software Product Line Refinement Theory to the Coq proof assistant. Thayonara Alves, Leopoldo Teixeira, Vander Alves and Thiago Castro.
  • Reversal Fuzzy Switch Graphs. Suene Duarte, Regivan Santiago, Manuel Martins and Daniel Figueredo.
  • Safe Evolution of Product Lines using Configuration Knowledge Laws. Leopoldo Teixeira, Rohit Gheyi and Paulo Borba.
  • Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Yvonne Murray, David A. Anisi, Martin Sirevåg, Rabah Saleh Hagag, Pedro Ribeiro and Geir Hovland.
  • Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model. Mihir Mehta and William R Cook.
  • Statistical Model Checking in Drug Repurposing for Alzheimer's Disease. Herbert Fernandes, Antonio Carlos Oliveira and Sérgio Campos.

Proceedings

IMPORTANT ANNOUNCEMENT REGARDING COVID-19

In light of the COVID-19 pandemic, SBMF 2020 will not take place physically. It will be replaced by a virtual event only using Zoom. Registration is now open.

Important dates

  • 17 November, 2020: SBMF warm-up sessions
  • 24 to 27 November, 2020: ETMF lectures and tutorials
  • 25 to 27 November, 2020: SBMF keynote speeches and technical sessions

Introduction

SBMF 2020 is the twenty-third of a series of events devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event, with an international reputation. In SBMF 2020, we are going to have three keynote speeches and four technical sessions.

ETMF is a School of Theoretical Computer Science and Formal Methods that aims to bring together students and researchers to disseminate and promote theoretical aspects of computing. In ETMF 2020, we are going to have two lectures and three introductory tutorials on formal methods aimed at people unfamiliar with the subject.

Awards

Sponsored by Springer, a physical book (see the list below) is going to be given to the recipients of the following awards: (I) Best SBMF paper, (II) Best SBMF reviewer, (III) Best SBMF technical presentation, (IV) Best ETMF lecture/tutorial, and (V) Most engaged attendee.

Code of Conduct

The open exchange of ideas and the freedom of thought and expression are central to SBMF/ETMF goals. This requires an environment that acknowledges the inherent worth of every person and group, fosters dignity, understanding, and mutual respect, and embraces diversity. For these reasons, SBMF/ETMF are committed to provide a harassment-free experience to participants and in its official communication channels, including social media. The aim is every and any participant to feel welcome, included, respected, and safe. There is no any tolerance for hostile or unwelcome behavior or for speech that intimidates, creates discomfort or interferes with a person’s participation at the conference.

Unacceptable behavior include: abusive or degrading language, sustained disruption of a talk, discussion or other activity, discrimination, deliberate intimidation, stalking, harassing photography or recording, inappropriate physical contact, sexual imagery, and undesired sexual attention.

Harassment includes: harmful comments, writings or actions related to race, color, sex, gender, sexual orientation, gender identity or expression, age, marital status, religion, national origin, disability, pregnancy, medical conditions, veteran status or any other status protected by Brazilian laws.

Anyone witnessing or subject to unacceptable behavior should notify a member of the SBMF/ETMF 2020 Organizing Committee or security staff. A response that the participant was "joking" or that the behavior was "playful" will not be accepted. Individuals violating these standards may be punished or excluded from the conference without any reimbursement or refund at the discretion of the SBMF/ETMF 2020 Organizing Committee.

Programme

Overview

Please notice that all times are GMT-3:00

.

All Zoom links are available in the description of the respective session's Slack channel.

Detailed programme

Please notice that the program may be subject to change

Warm-up sessions

SBMF 2020 Warm-up #1 --- The formal methods community in Brazil
  • Speaker: Tiago Massoni - Universidade Federal de Campina Grande (BR)
  • Format: Zoom Webinar
SBMF 2020 Warm-up #2 --- A practical introduction to formal methods using Coq
  • Speaker: Gustavo Carvalho - Universidade Federal de Pernambuco (BR)
  • Format : Zoom Meeting

ETMF programme

Opening of ETMF 2020
  • Speaker: SBMF organization committee.
  • Format : Zoom Webinar
ETMF 2020 Lecture #1 --- Improving GUI programming and usability by formal thinking.
  • Speaker: Jaakko Järvi - University of Bergen (NO)
  • Format : Zoom Webinar
ETMF 2020 Lecture #2 --- Applications of formal methods in industry.
  • Speaker: Sérgio Campos - Universidade Federal de Minas Gerais (BR)
  • Format : Zoom Webinar
ETMF 2020 Tutorial #1 --- An introduction to formal models and languages.
  • Speaker: Gustavo Carvalho - Universidade Federal de Pernambuco (BR)
  • Format : Zoom Meeting
ETMF 2020 Tutorial #2 --- An introduction to model checking.
  • Speaker: Marcel Oliveira - Universidade Federal do Rio Grande do Norte (BR)
  • Format : Zoom Meeting
ETMF 2020 Tutorial #3 --- An introduction to theorem proving.
  • Speaker: Leopoldo Teixeira - Universidade Federal de Pernambuco (BR)
  • Format : Zoom Meeting

SBMF programme

Opening of SBMF 2020
  • Speaker: SBMF organization committee.
  • Format : Zoom Webinar
SBMF Keynote 1: Testing Refactoring Implementations
  • Speaker: Rohit Gheyi - Universidade Federal de Campina Grande (BR)
  • Format : Zoom Webinar
SBMF Keynote 2: Navigating the Universe of Z3 Theory Solvers
  • Speaker: Nikolaj Bjørner - Microsoft Research (US)
  • Format : Zoom Webinar
SBMF Keynote 3: Formal Verification of Neural Networks?
  • Speaker: Martin Leucker - Universtity of Lübeck (DE)
  • Format : Zoom Webinar
SBMF Technical Session 1 (Zoom Meeting): Topic: Models, Languages and Semantics (part 1)
  • Modeling Big Data Processing Programs: João de Souza Neto - Universidade Federal do Rio Grande do Norte (BR)
  • Reversal Fuzzy Switch Graphs: Suene Campos - Universidade Federal do Rio Grande do Norte (BR)
  • Calculational proofs in Relational Graphical Linear Algebra: João Paixão - Universidade Federal do Rio de Janeiro (BR)
SBMF Technical Session 2 (Zoom Meeting): Topic: Models, Languages and Semantics (part 2)
  • Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model: Mihir Mehta - University of Texas at Austin (US)
  • Optimization of Timed Scenarios: Neda Saeedloei - Towson University (US)
SBMF Technical Session 3 (Zoom Meeting): Topic: Experience Reports
  • Statistical Model Checking in Drug Repurposing for Alzheimer’s Disease: Herbert Fernandes - Universidade Federal de Minas Gerais (BR)
  • Safety Assurance of a High Voltage Controller for an Industrial Robotic System: Yvonne Murray (NO) - University of Agder (NO)
SBMF Technical Session 4 (Zoom Meeting): Topic: Software Product Lines
  • Merging Cloned Alloy Models with Colorful Refactorings: Chong Liu - INESC TEC (PT)
  • Porting the Software Product Line Refinement Theory to the Coq proof assistant: Thayonara Alves - Universidade Federal de Pernambuco (BR)
  • Safe Evolution of Product Lines using Configuration Knowledge Laws: Leopoldo Teixeira - Universidade Federal de Pernambuco (BR)
Closing of SBMF 2020, announcement of awards and SBMF 2021
  • Speaker: SBMF organization committee.
  • Format : Zoom Webinar

Ouro Preto

Ouro Preto is located about 100/km from the capital of Minas Gerais state, Belo Horizonte, in a region which is a cultural center with various well-known poets, musicians, and Brazilian visual artists. Due to its architecture, composed by the biggest group of Baroque works in Brazil, Ouro Preto was the first Brazilian town entitled as World Cultural Heritage by UNESCO in 1980.
Born from explorer Antônio Dias’s discovery of “ouro preto” (black gold) in the Tripuí riverbed in the 17 th century, the history of the city could be conflated with Brazil’s. Ouro Preto enjoyed its gilded age during the Ciclo do Ouro , when it was the stage for the Inconfidência Mineira, a separatist movement led by Tiradentes and motivated by the Portuguese crown’s high taxation of gold.
The decline of Ouro Preto’s mines, at the end of the 18 th Century, led much of the population to abandon the city. This migration, on the other hand, led to the preservation of its historical center, the largest example of Baroque architecture in the world. Especially noteworthy are the works of Aleijadinho and Master Ataíde.
Rich in history, culture, education, and entertainment, the town has an intense cultural agenda, organized in partnership with UFOP and some of the most important artistic and cultural events of the country.
Inspiration for poets and artists, for mysterious legends and stories that have persisted generation after generation among its inhabitants, Ouro Preto is an icon survived in Tomás Antônio Gonzaga’s poetry, in Guignard’s canvases and in the imagination of all who have the chance to visit.


Church Nossa Senhora do Pilar

This building was completed in 1731 as a replacement for the original main church, constructed between 1700 and 1707 of mud and wood reinforcements. It is considered the pinnacle of baroque opulence and dramatic quality. Its austere facade is a sharp contrast to the lavish interior, decorated with 434 kg (956 lb) of gold and 400 kg (880 lb) of silver. Francisco Xavier de Brito, one of Aleijadinho's mentors, is believed to have designed the main altar. Don't miss the Museu de Arte Sacra in the basement of this church.
Informations of other curches can be seen here.


Museum of the Inconfidência

The Museum of the Inconfidência is the second most visited museum in Brazil. It is dedicated to those who died in a failed rebellion movement Inconfidência Mineira (1789) for Brazilian independence from Portugal. It offers a rich portrait of the local society at the time. It is located at Tiradentes square, right in front of a monument dedicated to Joaquim Jose da Silva Xavier the most famous activist of the Inconfidência movement.


Santa Rita Gold Mine

Opened in 1704, this is oldest mine in town. This mine was dug by slaves and shows the contrast between hand dug mines and industrially dug mines. It's digging produced a maze of tunnels. Guided visits allow tourists to explore some parts of the ancient mine.


Mina do Chico Rei

The legend says this mine was property of "Chico Rei" (fictional name), a former slave who won his freedom and become rich. He was the only black who owned a gold mine in colonial times . It is located in the backyard a particular property . The mine is well conserved. In the mine walls are cavities where the deposited gold was collected during the day. The total area of 8 square kilometers with 175 open galleries , excavated in three levels deep.


Train ride from Ouro Preto to Mariana

The train ride allows to know history and beautiful scenery of the cities of Ouro Preto and also the historic town of Mariana, through the old railway built in 1883, with 18 kilometers long. The carriages and the locomotive were handmade renovated, preserving its original features - keeping the same design of the old trains , with wooden interiors. Panoramic windows allow a full view of the beautiful countryside, including waterfalls. The Ouro Preto and Mariana stations complete in 2016, respectively, 128 and 102 years.

Sponsorship

Realization