A Caltech Library Service

SCALE: Source Code Analyzer for Locating Errors


Florian, Mihai (2010) SCALE: Source Code Analyzer for Locating Errors. Master's thesis, California Institute of Technology. doi:10.7907/KXWA-7Y81.


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:
  • None, None
Defense Date:14 April 2010
Record Number:CaltechTHESIS:04142010-122136677
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:5718
Deposited By: Mihai Florian
Deposited On:16 Apr 2010 22:18
Last Modified:08 Nov 2019 18:08

Thesis Files

PDF - Final Version
See Usage Policy.


Repository Staff Only: item control page