Finding bugs in software with a constraint solver

Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004.

Bibliographic Details
Main Author: Vaziri-Farahani, Mandana
Other Authors: Daniel N. Jackson.
Format: Thesis
Language:eng
Published: Massachusetts Institute of Technology 2006
Subjects:
Online Access:http://hdl.handle.net/1721.1/30090
_version_ 1826216088351801344
author Vaziri-Farahani, Mandana
author2 Daniel N. Jackson.
author_facet Daniel N. Jackson.
Vaziri-Farahani, Mandana
author_sort Vaziri-Farahani, Mandana
collection MIT
description Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004.
first_indexed 2024-09-23T16:42:09Z
format Thesis
id mit-1721.1/30090
institution Massachusetts Institute of Technology
language eng
last_indexed 2024-09-23T16:42:09Z
publishDate 2006
publisher Massachusetts Institute of Technology
record_format dspace
spelling mit-1721.1/300902019-04-12T09:06:38Z Finding bugs in software with a constraint solver Vaziri-Farahani, Mandana Daniel N. Jackson. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. Includes bibliographical references (p. 99-101). We present a static technique for finding bugs in object-oriented procedures. It is capable of checking complex user-defined structural properties - that is, of the configuration of objects on the heap - and generates counterexample traces with no false alarms. It is modular, requires no user-provided abstractions, and is fully automatic. It is based on the Alloy modelling language and analyzer. The method relies on a three-step translation: from code to a formula in Alloy, which is a first-order relational logic, then to a propositional formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to find a solution that constitutes a counterexample. Modularity comes at the price of intermediate specifications. To minimize such annotations, the analysis contains a suite of optimizations that allow checking larger procedures with fewer annotations. The optimizations are based on a special treatment of relations that are known to be functional, and target all steps of the translation to CNF. Their effect is demonstrated with a prototype tool that can handle a subset of Java, by analyzing real code. by Mandana Vaziri-Farahani. Ph.D. 2006-03-24T18:18:33Z 2006-03-24T18:18:33Z 2004 2004 Thesis http://hdl.handle.net/1721.1/30090 55673127 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 101 p. 6085880 bytes 6085686 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology
spellingShingle Electrical Engineering and Computer Science.
Vaziri-Farahani, Mandana
Finding bugs in software with a constraint solver
title Finding bugs in software with a constraint solver
title_full Finding bugs in software with a constraint solver
title_fullStr Finding bugs in software with a constraint solver
title_full_unstemmed Finding bugs in software with a constraint solver
title_short Finding bugs in software with a constraint solver
title_sort finding bugs in software with a constraint solver
topic Electrical Engineering and Computer Science.
url http://hdl.handle.net/1721.1/30090
work_keys_str_mv AT vazirifarahanimandana findingbugsinsoftwarewithaconstraintsolver