Software and Computational Systems Lab

k-induction is a verification technique for reachability analysis. Ranking function analysis can prove the termination of a loop and map states reachable inside the loop into numbers satisfying multiple conditions. Plain k-induction sometimes assumes unreachable states when trying to infer k-inductive invariant. These states are often pruned by using auxiliary invariants either provided by different reachability analyses or written by human. The goal of the thesis is to use termination analysis to compute ranking function and then use these ranking functions to boost k-induction.

C program satisfies termination specification if all the possible executions of the program eventually terminate. It is usually very challenging to automatically prove that a given program satisfies this property. T2R is an algorithm that transforms the program so that the transformed program can be verified using well-performing fine-tuned reachability algorithms. It is implemented in our modular framework for program transformations. Current transformation is inefficient for some reachability techniques like symbolic execution. The goal of this thesis is to implement another transformation that would make the symbolic tree easier to explore for symbolic execution.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. After having solved the transformed task, we want to transform the witness i.e. the information the verifier provided for the verdict of the program to a witness for the original program. The goal of the thesis is to implement such a transformation of witnesses.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. No-Datarace and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the No-Datarace property to the Reach-Safety property, which opens new options for No-Datarace analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves No-Datarace, implement the transformation in a tool and observe whether it is more efficient to solve No-Overflow using Reach-Safety analysis.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves Memory-Safety, implement the transformation in a tool and observe whether it is more efficient to solve Memory-Safety using Reach-Safety analysis.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Thread-Liveness property is a liveness property, whereas Reach-Safety is a safety property. It is well-known that liveness can be transformed to safety. By instrumenting C programs, we can convert the Thread-Liveness property to the Reach-Safety property, which opens new options for Thread-Liveness analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to implement the transformation in a tool and observe whether it is more efficient to solve Thread-Liveness using Reach-Safety analysis.