Return to search

Expressive and efficient bounded model checking of concurrent software

To improve automated verification techniques for ANSI-C software, I examine temporal logics for describing program properties, and techniques for increasing the speed of program verification,for both single threaded and concurrent programs, based on the model checker ESBMC. A technique for evaluating LTL formulae over finite program traces is proposed and evaluated over a piece of industrial software and a suite of benchmarks, with favourable results. Efficient formulations of the model checking problem for SMT solvers are evaluated, and the performance of different solvers compared. Finally a number of optimisations for concurrent program verification not previously applied to symbolic software model checking are evaluated, resulting in an order of magnitude performance improvement over ESBMCs prior and already internationally competitive performance.
Date January 2015
CreatorsMorse, Jeremy
ContributorsNicole, Denis
PublisherUniversity of Southampton
Source SetsEthos UK
Detected LanguageEnglish
TypeElectronic Thesis or Dissertation

Page generated in 0.0156 seconds