OpenLLM-France/wikimedia huggingface dataset:
# Gôndola

A gôndola é uma embarcação típica da Lagoa de Veneza, na Itália. Pelas suas características de manobrabilidade e velocidade, foi, até a chegada dos meios motorizados, a embarcação veneziana mais adaptada ao transporte de pessoas. Em uma cidade como Veneza, os canais foram sempre mais utilizados como via de transporte. Atualmente é usada sobretudo para passeios turísticos.
A gôndola é considerada uma das formas de encontro mais românticos de Veneza.
Em 2010 existiam 426 gondoleiros, dos quais um era mulher As gôndolas de Veneza são conhecidas mundialmente como um símbolo emblemático da cidade. Sua história remonta ao século XI, quando eram utilizadas para transporte e comércio ao longo dos canais venezianos. Com o passar dos séculos, as gôndolas passaram a ser associadas à elegância e ao charme da cidade, tornando-se uma parte integrante da cultura veneziana.
No século XVI, as gôndolas evoluíram para a forma alongada que conhecemos hoje, com uma proa ornamentada e um casco assimétrico que facilita a navegação nos canais estreitos. Essa forma distintiva permitiu que as gôndolas se movessem com agilidade pelos canais sinuosos, tornando-se uma forma eficiente de transporte para os habitantes de Veneza.
Além disso, as gôndolas possuem detalhes decorativos, como o ferro da proa, conhecido como "fèrro," que serve tanto para equilíbrio quanto para simbolismo. O fèrro geralmente tem seis dentes, representando os seis distritos de Veneza, e um dente voltado para cima, simbolizando a Ilha de Giudecca.
Os gondoleiros, responsáveis por pilotar as gôndolas, também desempenham um papel importante na tradição. Eles são conhecidos por seus trajes típicos, compostos por camisetas listradas, chapéus de palha e faixas vermelhas.
# Atomkraft

Atomkraft é banda inglesa de speed metal que existiu de 1979 a 1988 e se reiniciou em 2005.

## Discografia

* 1981 - Atomkraft (demo)
* 1981 - Demon (demo)
* 1983 - Total Metal (demo)
* 1985 - Future Warriors
* 1985 - Heat and Pain (demo)
* 1985 - Pour the Metal In (demo)
* 1986 - Your Mentor (demo)
* 1986 - Queen of Death (EP)
* 1987 - Conductors of Noize (EP)
* 1987 - Conductors of Noize (vídeo)
* 2011 - Cold Sweat (EP)

## Compilação

* 1987 - Atomkraft (compilação)
* 2004 - Total Metal: The Neat Anthology (compilação)
* 2014 - Looking Back to the Future (compilação)
# Vista da Janela em Le Gras

Vista da Janela em Le Gras (em francês intitulado Point de vue du Gras) é uma imagem heliográfica considerada a primeira fotografia permanente do mundo. Foi criada por Joseph Nicéphore Niépce em 1826 ou 1827 em Saint-Loup-de-Varennes, na França, e mostra partes dos edifícios e paisagem vizinhos de sua propriedade, Le Gras. Em 2003, a revista Life a incluiu na lista das "100 Fotografias que Mudaram o Mundo".
# Campeonato Mundial de Ginástica Artística de 2009 - Cavalo com alças masculino

Londres 2009 :
Competições
Individual geral
masc
fem
Salto sobre a mesa
masc
fem
Solo
masc
fem
Cavalo com alças
masc
Argolas
masc
Barras paralelas
masc
Barra fixa
masc
Barras assimétricas
fem
Trave
fem :
Esta caixa: verdiscutireditar :
A competição do cavalo com alças masculino do Campeonato Mundial de Ginástica Artística de 2009 teve sua final disputada no dia 17 de outubro. A qualificatória que definiu os ginastas finalistas foi disputada em 13 de outubro

## Medalhistas

| Ouro | CHN Zhang Hongtao |
| Prata | HUN Krisztián Berki |
| Bronze | AUS Prashanth Sellathurai |

## Resultados
### Qualificatória

Esses são os resultados da qualificatória.
| Pos. | Ginasta | Total | Nota |
| 1 | CHN Zhang Hongtao | 16,275 | Q |
| 2 | HUN Krisztián Berki | 16,100 | Q |
| 3 | GBR Louis Smith | 15,900 | Q |
| 4 | ROU Flavius Koczi | 15,625 | Q |
| 5 | AUS Prashanth Sellathurai | 15,575 | Q |
| 6 | FRA Cyril Tommasone | 15,450 | Q |
| 7 | CRO Robert Seligman | 15,350 | Q |
| 8 | USA Timothy McNeill | 15,350 | Q |
| 9 | ROU Cosmin Popescu | 15,075 | R |
| 10 | HUN Vid Hidvegi | 14,925 | R |
| 11 | BLR Aliaksandr Tsarevich | 14,875 | R |
* Q - qualificado para a final
* R - reserva

### Final

Esses são os resultados da final.
| Pos. | Ginasta | Nota D | Nota E | Total |
| | CHN Zhang Hongtao | 6,600 | 9,600 | 16,200 |
| | HUN Krisztián Berki | 6,900 | 9,175 | 16,075 |
| | AUS Prashanth Sellathurai | 6,600 | 8,800 | 15,400 |
| 4 | FRA Cyril Tommasone | 6,500 | 8,725 | 15,225 |
| 5 | USA Timothy McNeill | 6,400 | 8,750 | 15,150 |
| 6 | ROU Flavius Koczi | 6,600 | 8,375 | 14,975 |
| 7 | CRO Robert Seligman | 6,100 | 8,650 | 14,750 |
| 8 | GBR Louis Smith | 6,600 | 7,850 | 14,450 |
# São Pedro (Cabo Verde)

Coordenadas: 16º 44' 14" 0″ N 25º 0' 20" W
São Pedro é uma aldeia piscatória na ilha de São Vicente, Cabo Verde, pertencendo ao concelho homónimo e à freguesia de Nossa Senhora da Luz. Fica a 7 km a sudoeste da cidade do Mindelo, capital da ilha. A nordeste da aldeia localiza-se o aeroporto que serve a ilha.

## Lugares próximos

* Lazareto, nordeste
* Mindelo, nordeste
* Praia de Flamengos, leste
* «Aeroporto Cesária Évora (Aeroporto Internacional de São Pedro)»

## Turismo

São Pedro tem uma enorme praia com águas turquesas, na baía homónima. A paisagem é árida e majestosa e os ventos constantes tornam-na numa praia internacionalmente reputada para a prática do windsurf. A aldeia é pequena e pitoresca, com casas coloridas. Praticamente apenas pescadores a habitam.
A oeste, no lugar de Santo André, está uma moderna unidade hoteleira, com pequenos apartamentos, chamada Foya Branca. Outro aldeamento turístico, São Pedro Village, vai também ser criado na zona. A 2 km, mais para oeste, fica o farol de D. Amélia.
Na zona de São Pedro está incluída parte do complexo montanhoso do qual o Monte Cara faz parte, incluindo o ponto mais alto desse conjunto (o pico de Fateixa, com 571 m).

## Património

* Farol de D. Amélia

## Aeroporto Cesária Évora

O Aeroporto Cesária Évora (VXE) localiza-se junto à aldeia homónima, no vale da ribeira de São Pedro, cerca de 5 km a sudoeste do centro da cidade do Mindelo, capital da ilha de São Vicente.

## Desporto

Um clube de futebol da aldeia, Clube de Futebol de São Pedro, participa nas competições de Liga Insular de São Vicente, hoje na Segunda Divisão.
# (34731) 2001 QU47

2001 QU47 (asteroide 34731) é um asteroide da cintura principal. Possui uma excentricidade de 0.08711350 e uma inclinação de 7.69640º.
Este asteroide foi descoberto no dia 16 de agosto de 2001 por LINEAR em Socorro.
# Leis de Ranganathan

As leis de Ranganathan são cinco leis fundamentais instituídas para a biblioteconomia pelo pensador indiano Shiyali Ramamrita Ranganathan, e vigoram até os dias atuais. Ranganathan era um professor de matemática indiano interessado em biblioteconomia que cursou na Inglaterra. Seu livro "The Five Laws of Library Science" (1931) aborda importantes pontos para as práticas da biblioteconomia. Os enunciados do autor são, em sua essência, os precursores dos movimentos liderados por profissionais bibliotecários de hoje.

## As cinco leis

As leis de Ranganathan podem ser resumidas da seguinte forma:
* Os livros são escritos para serem lidos - o livro é um meio que impulsiona o conhecimento. E podemos observar a importância de uma biblioteca na seguinte frase: "quem tem informação, tem poder". Aponta para o livro como um meio e não como tendo um fim em si. Em relação às bibliotecas, de nada adianta tê-las cheias de livros senão se dá o acesso à informação. Por isso, esta afirmativa de Ranganathan se perpetua até hoje.
* Todo leitor tem seu livro - o bibliotecário deve fazer o estudo dos usuários, observando a clientela para preparar o acervo. Aponta para a seleção conforme o perfil do usuário.
* Todo livro tem seu leitor - refere-se a disseminação da informação, em que se deve divulgar os livros existentes em cada biblioteca. Aponta para a importância da divulgação do livro, sua disseminação, antecipando a estética da recepção.
* Poupe o tempo do leitor - a arrumação e catalogação dos documentos diminui o tempo necessário para encontrar a informação desejada. Aponta para o livre acesso às estantes, o serviço de referência e a simplificação dos processos técnicos.
* Uma biblioteca é um organismo em crescimento - o bibliotecário deve controlar esse crescimento, verificando qual a informação que está sendo usada, através de estatísticas da consulta e empréstimo. Decorre da explosão bibliográfica que exige atualização das coleções e previsão do crescimento da área ocupada pela biblioteca.
# Gödeken

Gödeken :
| Província: | Santa Fé |
| Departamento: | Caseros |
| Código postal: | S2639 |
| Código telefônico: | 03465 |
| Localização: | 33° 23' S 61° 50' O |
| Área: | 227 km² |
| Altitude: | 94 m. |
| Fundação: | 1888 |
| Fundador: | Juan Gödeken |
| População: | 1 707 (2001 - INDEC) |
| Densidade: | 7,51 hab./km² |
| Variação intercensial: | -7,15% (1991-2001) |
| Fuso horário: | GMT-3 |
| Presidente Comunal | Jorge ALberto Rosell, PJ |
| Gentílico: | godekense |
| Código IFAM: | SFE140 |
Gödeken é uma comuna da Província de Santa Fé, no departamento Caseros, a 170 km de Rosário e a 299 km de Santa Fé, sendo a Ruta provincial 93 sua principal via de comunicação.

## História

Domingo Funes vendeu a Juan Gödeken uma fração de campo sem existência de caminhos ou algum tipo de assentamento, levando a supor que Juan Gödeken se encarregaria do primeiro loteamento, e que os colonos que chegavam depois limparam o campo e o cultivou, trazendo depois a maioria dos caminhos rurais.

## Toponímia

O nome do povoado é em homenagem a Juan Gödeken.

## Santo Padroeiro

* São José, festividades: 19 de março.

## Criação da Comuna

* 30 de junho de 1891.

## Biblioteca Popular

* Sarmiento

## Escolas de Educação Comum e Adultos

* Esc. Juan Gödeken, 82
* Esc. Malvinas Argentinas, 228
* Centro Alfab. 289, 12
* Esc. Baldomero F. Moreno, 104

## Televisão

* Gödeken Cable Visión

## Entidades Esportivas

* Club 25 de Mayo
* Club Soc. Dep. M. Gödeken
# Atomistix Virtual NanoLab

Atomistix Virtual NanoLab (VNL) é um software comercial do tipo aponte e clique, desenvolvido para simulação e análise de propriedades físicas e químicas de nanodispositivos. O "Virtual NanoLab" foi criado e é comercializado pela empresa Atomistix A/S.

## Recursos

Com sua interface gráfica, o Virtual NanoLab disponibiliza uma forma amigável de modelagem em escala atômica. O software contém um conjunto de instrumentos interativos que permitem ao usuário desenvolver nanosistemas, executar cálculos numéricos, e visualizar os resultados.
Exemplos como moléculas, nanotubos, sistemas cristalinos e sistemas two-probe(por exemplo, a nanoestrutura ligada a dois eletrodos), são criados com poucos cliques do mouse.
O Virtual NanoLab contém uma ferramenta de visualização 3D chamada Nanoscope, onde a geometria atômica e os resultados computados podem ser vistos e analisados. É possível, por exemplo, visualizar as funções de Bloch de nanotubos e cristais, orbitais moleculares, densidades de elétrons, e potenciais efetivos.
# Campeonato Europeu de Hóquei em Patins Masculino de 1973

O Campeonato Europeu de 1973 foi a 31.ª edição do Campeonato Europeu de Hóquei em Patins.

## Participantes

| País | Participação | Melhor Resultado |
| Portugal | 26.ª | Campeão (1947, 1948, 1949, 1950, 1952, 1956, 1959, 1961, 1963, 1965, 1967 e 1971) |
| Espanha | 19.ª | Campeão (1951, 1954, 1955, 1957 e 1969) |
| Itália | 30.ª | Campeão (1953) |
| Alemanha Ocidental | 27.ª | 2.º Lugar (1932 e 1934) |
| Holanda | 17.ª | 3.º Lugar (1963, 1967 e 1969) |
| Bélgica | 30.ª | 2.º Lugar (1947) |
| França | 30.ª | 2.º Lugar (1926, 1927, 1928, 1930 e 1931) |
| Suíça | 31.ª | 2.º Lugar (1937) |
| Inglaterra | 31.ª | Campeão (1926, 1927, 1928, 1929, 1930, 1931, 1932, 1934, 1936, 1937, 1938 e 1939) |

## Resultados

| Portugal | 5-0 | 3-1 | 2-1 | 17-1 | 17-2 | 11-3 | 16-0 |
| Espanha | 4-0 | 2-2 | 5-1 | 8-2 | 12-1 | 11-0 | 11-3 |
| Alemanha Ocidental | | 4-2 | 6-1 | 13-1 | 10-1 | 8-3 | 8-1 |
| Itália | | | 2-3 | 4-1 | 6-1 | 6-1 | 7-3 |
| Holanda | | | | 4-3 | 3-4 | 3-4 | 9-2 |
| Suíça | | | | | 12-4 | 3-2 | 2-0 |
| Bélgica | | | | | | 9-6 | 7-1 |
| França | | | | | | | 4-2 |
| Inglaterra | | | | | | | |

## Classificação final

| Lugar | Seleção | J | V | E | D | P | GM | GS | Dif. |
| | Portugal | 8 | 8 | 0 | 0 | 16 | 73 | 9 | +64 |
| | Espanha | 8 | 6 | 1 | 1 | 13 | 54 | 11 | +43 |
| | Alemanha Ocidental | 8 | 6 | 0 | 2 | 12 | 49 | 18 | +31 |
| 4 | Itália | 8 | 4 | 1 | 3 | 9 | 30 | 18 | +12 |
| 5 | Holanda | 8 | 3 | 0 | 5 | 6 | 25 | 29 | -4 |
| 6 | Suíça | 8 | 3 | 0 | 5 | 6 | 25 | 51 | -26 |
| 7 | Bélgica | 8 | 3 | 0 | 5 | 6 | 29 | 67 | -38 |
| 8 | França | 8 | 2 | 0 | 6 | 4 | 23 | 53 | -30 |
| 9 | Inglaterra | 8 | 0 | 0 | 8 | 0 | 12 | 64 | -52 |
* Campeões Europeus 1973
* PORTUGAL 13.º Título
# Lugano

Lugano é uma comuna da Suíça, no Cantão Tessino, do qual é a maior cidade, com cerca de 65 015 habitantes, embora a capital do cantão seja Bellinzona. Estende-se por uma área de 75,81 km², de densidade populacional de 857,6 hab/km². Confina com as seguintes comunas: Arogno, Bioggio, Campione d'Italia (IT-CO), Canobbio, Collina d'Oro, Grancia, Lanzo d'Intelvi (IT-CO), Massagno, Melide, Muzzano, Paradiso, Porza, Savosa, Sorengo, Valsolda (IT-CO), Vezia.
A língua oficial nesta comuna é o italiano. A cidade é banhada pelo Lago de Lugano (ou Ceresio).

## Educação

Lugano acolhe numerosas escolas e universidades:
* Universidade de Lugano (USI)
* Istituto Dalle Molle di Studi sull'Intelligenza Artificiale (IDSIA)
* Franklin University Switzerland
* The American School In Switzerland
* Scuola universitaria professionale della Svizzera italiana (SUPSI)
* Centro Svizzero di Calcolo Scientifico
* Lugano Monte Brè

## Outros projetos

O Wikimedia Commons possui multimédia sobre: Lugano.
# Telureto de manganês(II)

Telureto de manganês(II) é um composto inorgânico de fórmula química MnTe. Pode ser utilizado como detector potenciométrico.
# (34728) 2001 QM30

2001 QM30 (asteroide 34728) é um asteroide da cintura principal. Possui uma excentricidade de 0.05707310 e uma inclinação de 4.72266º.
Este asteroide foi descoberto no dia 16 de agosto de 2001 por LINEAR em Socorro.
# Leptogenys iridipennis

Leptogenys iridipennis é uma espécie de formiga do gênero Leptogenys, pertencente à subfamília Ponerinae.
# Guinga

Carlos Althier de Sousa Lemos Escobar (Rio de Janeiro, 10 de junho de 1950), mais conhecido como Guinga, é um compositor e violonista brasileiro. Profissionalmente, atuou como violonista com vários artistas renomados como Clara Nunes, Beth Carvalho, Alaíde Costa, João Nogueira e Cartola. Para além de compositor, Guinga formou-se em odontologia em 1975.
Teve várias de suas músicas gravadas por Elis Regina, Cauby Peixoto, Michel Legrand, Sérgio Mendes, Chico Buarque, Ivan Lins, Leila Pinheiro e Ronnie Von. No álbum Catavento e Girassol, gravado pela cantora Leila Pinheiro, as quatorze músicas são de sua autoria. Como parceiros estão Paulo César Pinheiro, Aldir Blanc e Chico Buarque.
Guinga tem dez discos solos gravados, todos bem recebidos pela crítica especializada, além de muitas parcerias com grandes nomes da música brasileira. O seu disco ”Cheios de Dedos”, recebeu prêmio Sharp como melhor disco instrumental de 1996. Em 2002, sua biografia, "Guinga, os mais belos acordes do subúrbio", escrita pelo jornalista Mário Marques foi publicado pela Editora Gryphus. Em 2003, a mesma editora lançou o songbook "A Música de Guinga", com partituras de grande parte da obra do autor.

## Discografia
### Como Compositor e Intérprete

* Simples e Absurdo (1991)
* Delírio Carioca (1993)
* Cheio de Dedos (1996)
* Suíte Leopoldina (1999)
* Cine Baronesa (2001)
* Noturno Copacabana (2003)
* Graffiando Vento (2004)
* Casa da Villa (2007)
* Dialetto Carioca (2007)
* Saudade do Cordão (2009), com Paulo Sérgio Santos
* Rasgando Seda (2012), com o Quinteto Villa-Lobos
* Francis e Guinga (2013), com Francis Hime
* Roendopinho (2014)
* Mar Afora (2015), com Maria João
* Porto da Madama (2015), com Maria João, Esperanza Spalding, Maria Pia de Vito e Mônica Salmaso
* Canção da Impermanência (2017)
* Avenida Atlântica (2017), com Quarteto Carlos Gomes

### Como compositor

(Discos de outros intérpretes em que todas as faixas são de composição de Guinga)
* Leila Pinheiro - Catavento e Girassol (1996) (Guinga participa também como violonista)
* Marcus Tardelli - Unha e Carne (2005)
* Mônica Salmaso - Corpo de Baile (2014)
# Atomotricha

Atomotricha é um gênero de traça pertencente à família Agonoxenidae.
# Língua cauixana

O Kauixana (Cawishana, Kawishana, Kaiʃana) é uma língua aruaque tida como extinta do Brasil. Poucos falantes foram registrados nos anos 50.
Aikhenvald (1999) a classificou como uma língua Manao Alto Amazonas junto com a língua shiriana. Kaufman (1994) a colocou no ramo das Leste Nawiki Alto Amazonas junto com línguas há muito extintas como a Jumana (Yumana) e Pasé, as quais Aikhenvald considerou sem classificação, isoladas. Sua sintaxe é ativa-estativa.

## Fonologia

O kauixana tinha 21 fonemas:
* consoantes (15): p, t, k, ʔ, ts, tʃ, x, h, m, n, ɲ, l, ɾ, w, j
* vogais (6): i, e, a, o, i, V́
# Tarcisio Cleto Chiavegato

Tarcisio Cleto Chiavegato nasceu em Jaguariúna no dia 13 de fevereiro de 1940. Filho de Alfredo Chiavegato e Clotilde Frachetta Chiavegato, mais conhecida como Dona Zenaide. Foi bancário e, desde a década de 1970, atua na área empresarial, como proprietário de indústria de produtos químicos. Sua experiência nesta área contribuiu para que fundasse a Associação Comercial e Industrial de Jaguariúna.
Ingressou na política como vice-prefeito; na ocasião acumulou os cargos de diretor municipal de Finanças e, interinamente, foi diretor do Departamento de Administração. Participou ativamente do governo do prefeito Laércio Gothardo, realizando ampla modernização dos serviços municipais e modificações na área do planejamento urbano. Como vice-prefeito, diretor de finanças e administrador, equilibrou as finanças municipais, seguindo a regra de que “não se pode gastar mais do que se arrecada”.
Suas maiores realizações foram: aumento da captação de água do rio Jaguari; ampliação da Estação de Tratamento de Água e sua distribuição; implantação da Rádio Educativa Estrela FM; restauração da antiga estação FEPASA, transformando-a no Centro Cultural de Jaguariúna; construção do pontilhão para transposição do rio Jaguari que permitiu o retorno da Maria Fumaça; construção de novas áreas do Hospital Municipal “Walter Ferrari”; construção de uma série de obras importantes nas áreas da habitação, saúde, educação, esporte, saneamento e industrialização. Em 2008, construiu e equipou o Teatro Dona Zenaide e a Casa da Memória Padre Gomes.
Em 2004 Tarcisio concluiu a recuperação da área do antigo lixão que existia na cidade há mais de vinte anos. Tarcisio construiu mais de vinte escolas e creches, sete Unidades Básicas de Saúde. Em sua gestão a cidade ficou por três anos consecutivos (2006, 2007 e 2008) entre as dez melhores do Brasil e em 2008 foi considerado o 3ª melhor município brasileiro em qualidade de vida, alcançando níveis de primeiro mundo.
# (34727) 2001 QV28

2001 QV28 (asteroide 34727) é um asteroide da cintura principal. Possui uma excentricidade de 0.17011640 e uma inclinação de 1.12502º.
Este asteroide foi descoberto no dia 16 de agosto de 2001 por LINEAR em Socorro.
# Leptogenys jeanneli

Leptogenys jeanneli é uma espécie de formiga do gênero Leptogenys, pertencente à subfamília Ponerinae.
# Guingamp

Guingamp (pronúncia AFI: /gɛ̃.gɑ̃/) é uma comuna francesa na região administrativa da Bretanha, no departamento Côtes-d'Armor. Estende-se por uma área de 3,41 km². Em 2010 a comuna tinha 7 561 habitantes (densidade: 2 217,3 hab./km²).318 hab/km².
A região é também a terra natal de Théodule-Armand Ribot, considerado o fundador da psicologia experimental francesa.
# Arras (direito)

Arras ou sinal é a entrega, por parte de um dos contratantes, de coisa ou quantia que significa a firmeza da obrigação contraída ou garantia da obrigação pactuada. Quando a coisa entregue é do mesmo gênero do restante da obrigação, as arras são consideradas como princípio de pagamento.
Existem dois tipos de arras:

## Confirmatórias

Confirmatórias ou arras propriamente ditas, quando representam uma prestação efetiva, realizada em garantia da conclusão de um contrato; Ver arts. 417 a 419 do Código Civil brasileiro de 2002.

## Penitenciais

Penitenciais, se há cláusula de arrependimento, caso em que a perda da prestação constitui a pena, tem o caráter de cláusula penal compensatória.
Nos tempos antigos, o Arras foi chamado diversas vezes de "Um centavo sério", ou "Arles centavo", ou o Deus de prata (em latim Argentum Dei). Era uma valiosa moeda ou sinal dado para vincular um negócio, nomeadamente para a compra ou locação de um servo.
Quando a operação é liquidada em seguida, o depósito é aplicado a parte do comprador dos custos restantes. Se a oferta for rejeitada, o dinheiro é normalmente devolvido, uma vez que nenhum contrato obrigatório foi celebrado. As leis variam quanto ao que acontece com o depósito caso o comprador não cumpra o contrato.
# Verificação de modelos

No campo da ciência da computação, verificação de modelos (do inglês, Model Checking) refere-se ao problema de testar automaticamente se um modelo que representa um sistema atende a uma dada especificação.
Tipicamente estes são sistemas de hardware, software e protocolos de comunicação e suas especificações contém requisitos de segurança como a ausência de deadlocks e comportamentos similares que podem levar o sistema a travar. Esse deadlock é uma situação onde duas ou mais ações simultaneamente esperam a finalização da outra para sua continuação, e assim nenhuma delas pode ser concluída.
Para resolver tal problema de maneira algorítmica, tanto o modelo do sistema quanto a especificação são formulados em alguma linguagem matematicamente precisa. Para esta finalidade, ela deve ser formulada como uma tarefa de lógica, de forma a verificar se uma dada estrutura satisfaz uma dada fórmula lógica. O conceito é geral e se aplica a todos os tipos de lógicas e estruturas apropriadas. Um problema simples de verificação de modelo é verificar se uma dada fórmula na lógica proposicional é satisfeita por uma dada estrutura.

## Visão geral

Uma importante classe de métodos de verificação de modelos tem sido desenvolvida para verificação de modelos de projetos de hardware e software onde a especificação é dada por uma fórmula de lógica temporal. Trabalhos pioneiros em verificação de modelos de fórmula de lógica temporal foram realizados por Edmund Clarke e Ernest Allen Emerson e por J. P. Queille e Joseph Sifakis. Clarke, Emerson e Sifakis receberam juntos o Prêmio Turing de 2007 por seu trabalho em verificação de modelos.
Verificação de modelos é mais freqüentemente aplicada em projetos de hardware. Para software, devido à indecidabilidade, a abordagem não pode ser totalmente algorítmica; tipicamente ela pode provar ou não provar uma dada propriedade.
A estrutura é usualmente dada como descrição de código fonte numa linguagem descritiva industrial de hardware ou uma linguagem de propósito especial. Tal programa corresponde a uma máquina de estados finitos, ou seja, um dígrafo (ou quiver) consistindo de nós (ou vértices) e bordas. Um conjunto de proposições atomizadas está associada a cada nó, tipicamente estabelecendo quais elementos de memória são um nó. Os nós representam estados do sistema, as bordas representam possíveis transições que podem alterar o estado, enquanto que as proposições atomizadas representam as propriedades básicas que se mantém num ponto de execução.
Formalmente, o problema pode ser estabelecido da seguinte maneira: dada uma propriedade desejada, expressa como uma lógica temporal p, e uma estrutura M com estado inicial s, decida se $M,s\models p$ . Se M é finito, como é em hardware, a verificação de modelos se reduz a uma busca gráfica.