Esta segunda edição de Lógica em Ciência da Computação atende às necessidades mais atuais no estudo e na prática da verificação de hardwares e softwares, continuando a fornecer uma introdução a argumentos formais que são, ao mesmo tempo, relevantes para as necessidades da ciência da computação moderna e suficientemente rigorosas para aplicações práticas. A apresentação é clara e simples, com material principal descrito no início do livro e técnicas mais aprimoradas introduzidas quando necessárias pelas aplicações. Esta nova edição inclui as versões mais atuais das ferramentas NuSMV e Alloy; foram feitas melhorias em todo o texto em relação à primeira edição, com seções extras e expandidas sobre a verificação de modelos na lógica temporal de tempo linear, programas de resolução SAT, lógica de segunda ordem, a ferramenta de especificação Alloy e programação por contrato. A cobertura sobre verificação de modelos também foi substancialmente atualizada, e mais exercícios foram adicionados.