Aplicando técnicas de programacão por restricões com raciocínio automático para verificação formal de software

Nesta pesquisa está sendo utilizada uma estratégia envolvendo técnicas de programação por restrições e aritmética intervalar para redução do domínio de variáveis no pré-processamento de programas para verificação formal via sistema BMC (Bounded Model Checking). A verificação formal de software envolve métodos que fazem uso de modelos matemáticos para checar a especificação de um determinado sistema. A verificação de modelo limitado BMC é um método formal que visa lidar com problemas com um número exponencial de estados, muitas vezes da classe EXP-time de complexidade computacional. O BMC consiste na modelagem em um sistema de transição de estados e procura por contra-exemplos das propriedades em cada estado até um limite k. Basicamente, o BMC reduz o problema de verificação de programa ao clássico da Satisfabilidade Booleana (SAT), NP-Completo em tempo de execução.Na estratégia elaborada, o programa é modelado como um CSP (Constraint Satisfaction Problem) usando as variáveis de entrada, seus domínios e as propriedades do programa, que são as restrições. Experimentos computacionais foram realizados usando benchmarks de programas em linguagem de programação Kotlin e Java, com a estratégia de CSP/CP para redução de domínio de variáveis do programa a ser verificado segundo uma propriedade desejada, no verificador automático de modelo limitado ESBMC-Jimple, desenvolvido pelo grupo de pesquisa. Com isto, obteve-se a redução do espaço de busca, o que pode ser verificado empiricamente nos resultados preliminares obtidos que, no geral, há redução do domínio com consequente diminuição do tempo de verificação dos programas Kotlin via ESBMC-Jimple.