Verifying Properties on a Program Using Static Analysis and Model Checking

Authors

Aymeric Fages

Type

techreport

Year

2020

Number

2020

Abstract

In this paper, we present different solutions to transform a program into a finite state system. Then we present our functional pipeline that allows us the say whether a program verifies a LTL formula. We describe all the aspect of this pipeline from LLVM tools and a C++ algorithm for model abstraction to the Spot library. On a first part of this paper, we explain the type of finite graph that we want to obtain in order to apply model checking in. On a second part, we define important models such as pushdown systems or Buchi automaton. On a third part, we explain how to find an under-approximation and over-approximation of a pushdown system as a finite system. Then finally, we show how those theoretical solutions were implemented into an actual functional pipeline.