Contacts

Probabilistic software analysis (PSA) aims at computing the probability for a target event to occur during a program execution, given a probabilistic usage profile. The profile assigns to each input variable a probability distribution over its valid domain. A recent technique for PSA exploits symbolic execution to extract the constraints on the input variables leading to the occurrence of the target event; a second analysis step quantifies then the probability for these constraint to be satisfy, assuming the given usage profile. The technique has been implemented on top of Symbolic PathFinder for Java. The goal of this seminar is to create a PSA tool for C programs, composing the symbolic execution of C programs performed in KLEE