O uso de multiprocessamento em chip sob a crescente demanda por desempenho leva a um aumento do número de núcleos de processamento, que interagem através de uma complexa hierarquia de memória compartilhada, a qual deve obedecer a requisitos de coerência e consistência capturados na interface hardware-software na forma de um modelo de memória. dada uma execução de um programa paralelo, verificar se a hierarquia obedece aqueles requisitos é um problema intratável quando a observabilidade do sistema restringe-se a um trace de memória para cada processador, tal como ocorre em um checker dinâmico pós-silício. esses checkers (baseados em inferências sobre traces) requerem o uso de backtracking para excluir falsos negativos. por outro lado, checkers pré-silício podem se beneficiar da observabilidade ilimitada de representações executáveis do multiprocessador para induzir um problema de verificação que pode ser resolvido em tempo polinomial (sem o uso de backtr acking) com plenas garantias de verificação (sem falsos negativos nem falsos positivos). esta dissertação faz uma avaliação experimental comparativa de checkers dinâmicos reportados na literatura e baseados em diferentes mecanismos (inferências, emparelhamento em grafo bipartido, scoreboard único e múltiplos scoreboards). os checkers são comparados para exatamente o mesmo conjunto de casos de teste: 100 programas paralelos não sincronizados, gerados de forma pseudo-aleatória, obtidos variando a frequência de ocorrência de instruções (3 mixes), o número de endereços compartilhados (entre 2 e 32) e o número de operações (entre 1k e 64k). a partir de uma mesma representação pré-validada do sistema, foram construídas dez representações derivadas, cada uma contendo um erro de projeto distinto. para reproduzir condições compatíveis com as tendências arquiteturais, os checkers foram comparados ao verificar um modelo com máxima relaxação de ordem de programa (bastante similar ao usado, por exemplo, nas arquiteturas alpha e armv7) para sistemas contendo de 2 a 32 núcleos de processamento. não é do conhecimento do autor a existência na literatura de uma avaliação experimental tão ampla. os resultados mostram a inviabilidade do uso de checkers baseados em inferências em tempo de projeto: têm o mais alto esforço computacional (pelo menos uma ordem de magnitude superior aos demais) e com a maior taxa de crescimento com o aumento do número de processadores. a avaliação indica que a forma mais eficiente de construir um checker pré-silício corresponde a uma observabilidade de três pontos de monitoramento por processador, ao uso de verificação on-the-fly (ao invés de análise postmortem) e à utilização de múltiplos artefatos para verificar separadamente e em paralelo os subespaços de verificação definidos pelo escopo individual de cada processador, antes de verificar globalmente os subespaços entre processadores. como um desdobramento da avaliação experimental, a dissertação identifica uma deficiência comum a todos os checkers analisados: sua inadequação para verificar modelos de memória com fraca atomicidade de escrita, exatamente aqueles apontados como tendência e já presentes em arquiteturas recentes (e.g. armv8). diante disso, a dissertação propõe algoritmos generalizados capazes de verificar tais modelos com plenas garantias de verificação com uma observabilidade de quatro pontos (bem definidos) por processador.