Symbolic and quantitative methods in software model learning, model assessment, and model checking
File(s)
Author(s)
Clun, Donato
Type
Thesis
Abstract
Formal models are central in various methods for verifying, testing, reasoning about, and documenting software. However, there are circumstances in which their applicability is limited. Models are seldom available; creating and maintaining them is time-consuming and error-prone, and they often become outdated quickly. Moreover, for specific problems, commonly used quantitative techniques require annotating system models with probabilities. Defining probabilistic models can be more challenging than non-probabilistic ones, and in some cases this may not be possible, because the aspect being modelled has no intrinsic probabilistic behaviour. This thesis investigates methods aimed at addressing these challenges.
First, it introduces an active learning method to automatically learn a model of the language of syntactically correct inputs of a program from its implementation. The method leverages symbolic values to reason about multiple input symbols at once, and uses concolic execution to obtain a symbolic path condition containing the constraints that determined each execution path. This results in improved query efficiency and correctness guarantees for inputs up to a prescribed length, compared to existing active learning methods that process only concrete program inputs and require usually intractable equivalence oracles for correctness.
Next, it presents a method to rigorously measure the accuracy of an inferred model against a ground truth reference model --- a crucial step in the development of model inference algorithms. The proposed method addresses longstanding limitations of widely used statistical assessment methods, which generally overlook the evaluation bias introduced by the random sampling, generating potentially misleading results.
Finally, it provides a deterministic quantitative model checking method to verify non-regular properties of terminating recursive programs. Unlike currently available methods, which are limited to the analysis of probabilistic models and where the quantitative result is the probability that the given property is satisfied, the proposed method allows quantitative model checking of non-probabilistic models.
First, it introduces an active learning method to automatically learn a model of the language of syntactically correct inputs of a program from its implementation. The method leverages symbolic values to reason about multiple input symbols at once, and uses concolic execution to obtain a symbolic path condition containing the constraints that determined each execution path. This results in improved query efficiency and correctness guarantees for inputs up to a prescribed length, compared to existing active learning methods that process only concrete program inputs and require usually intractable equivalence oracles for correctness.
Next, it presents a method to rigorously measure the accuracy of an inferred model against a ground truth reference model --- a crucial step in the development of model inference algorithms. The proposed method addresses longstanding limitations of widely used statistical assessment methods, which generally overlook the evaluation bias introduced by the random sampling, generating potentially misleading results.
Finally, it provides a deterministic quantitative model checking method to verify non-regular properties of terminating recursive programs. Unlike currently available methods, which are limited to the analysis of probabilistic models and where the quantitative result is the probability that the given property is satisfied, the proposed method allows quantitative model checking of non-probabilistic models.
Version
Open Access
Date Issued
2023-09-30
Date Awarded
01/03/2024
License URL
Advisor
Filieri, Antonio
Sponsor
Engineering and Physical Sciences Research Council
Grant Number
EP/L016796/1
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)