CaltechTHESIS
  A Caltech Library Service

SCALE: source code analyzer for locating errors

Citation

Florian, Mihai (2010) SCALE: source code analyzer for locating errors. Master's thesis, California Institute of Technology. http://resolver.caltech.edu/CaltechTHESIS:04142010-122136677

Abstract

This thesis presents the design and implementation of SCALE, a tool for systematic software testing multi-threaded C applications that use the pthread library. SCALE exhaustively explores the non determinism introduced by thread schedulings and tries to find violations of safety properties. We have designed SCALE to be flexible so that it is easy to add and combine different exploration and state space reduction algorithms. In this thesis we describe the currently implemented reduction algorithms, of which the most important ones are local execution cycle detection and super step partial order reduction. To exemplify how SCALE can be used, we have applied it to a few multi-threaded applications, measured its performance and compared the results to those obtained by other tools. While checking the implementation of a non-blocking queuing algorithm, we were able to find a previously unknown bug that appears only in some unexpected thread inter-leavings.

Item Type:Thesis (Master's thesis)
Subject Keywords:software verification, systematic software testing, model checking, partial order reduction, super step partial order reduction, local cycle detection
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Holzmann, Gerard J. (advisor)
  • Chandy, K. Mani (co-advisor)
Thesis Committee:
  • Unknown, Unknown
Defense Date:14 April 2010
Author Email:mflorian (AT) cs.caltech.edu
Record Number:CaltechTHESIS:04142010-122136677
Persistent URL:http://resolver.caltech.edu/CaltechTHESIS:04142010-122136677
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:5718
Collection:CaltechTHESIS
Deposited By: Mihai Florian
Deposited On:16 Apr 2010 22:18
Last Modified:26 Dec 2012 03:24

Thesis Files

[img]
Preview
PDF - Final Version
See Usage Policy.

982Kb

Repository Staff Only: item control page