A verifier for functional properties of sequence-manipulating programs. Many programs operate on data structures whose models are sequences, such as arrays, lists, and queues. When specifying and verifying functional properties of such programs, it is convenient to use an assertion language and a reasoning engine that incorporate sequences natively. This paper presents `qfis’, a program verifier geared to sequence-manipulating programs. `qfis’ is a command-line tool that inputs annotated programs, generates the verification conditions that establish their correctness, tries to discharge them by calls to the SMT-solver CVC3, and reports the outcome back to the user. `qfis’ can be used directly or as a back-end of more complex programming languages.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.