Under-constrained execution

Published 9 July 2007

Dawson Engler, Daniel Dunbar

Citations65

TL;DR

Software testing is well-recognized as a crucial part of the modern software development process, however, manual testing is labor intensive and often fails to produce impressive coverage results.

Abstract

Article Share on Under-constrained execution: making automatic code destruction easy and scalable Authors: Dawson Engler Stanford University Stanford UniversityView Profile , Daniel Dunbar Stanford University Stanford UniversityView Profile Authors Info & Claims ISSTA '07: Proceedings of the 2007 international symposium on Software testing and analysisJuly 2007 Pages 1–4https://doi.org/10.1145/1273463.1273464Online:09 July 2007Publication History 43citation404DownloadsMetricsTotal Citations43Total Downloads404Last 12 Months27Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Keywords

Computer Science

ACM SIGPLAN NoticesDART

2,073 Citations2005Patrice Godefroid, Nils Klarlund +1 more

CUTE

1,653 Citations2005Koushik Sen, Darko Marinov +1 more

A method to represent and track constraints that capture the behavior of a symbolic execution of a unit with memory graphs as inputs is developed and an efficient constraint solver is proposed to facilitate incremental generation of such test inputs.

DART

1,501 Citations2005Patrice Godefroid, Nils Klarlund +1 more

DART is a new tool for automatically testing software that combines three main techniques, automated extraction of the interface of a program with its external environment using static source-code parsing, and dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths.

EXE

789 Citations2006Cristian Cadar, Vijay Ganesh +3 more

This paper presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code instead of running code on manually or randomly constructed input, and solves the current path constraints to find concrete values using its own co-designed constraint solver, STP.

ACM SIGSOFT Software Engineering NotesKorat

598 Citations2002Chandrasekhar Boyapati, Sarfraz Khurshid +1 more

Lecture notes in computer scienceGeneralized Symbolic Execution for Model Checking and Testing

561 Citations2003Sarfraz Khurshid, Corina S. Păsăreanu +1 more

A source to source translation to instrument a program is defined, which enables standard model checkers to perform symbolic execution of the program, and a novel symbolic execution algorithm is given that handles dynamically allocated structures, method preconditions and concurrency.

ACM SIGPLAN NoticesCompositional dynamic test generation

411 Citations2007Patrice Godefroid

Thorough static analysis of device drivers

376 Citations2006Thomas Ball, Ella Bounimova +7 more

The Static Driver Verifier tool (SDV) uses this engine to find kernel API usage errors in a driver, and discusses the techniques used in SDV to meet these requirements, and empirical results from running SDV on over one hundred Windows device drivers.

Compositional dynamic test generation

308 Citations2007Patrice Godefroid

This paper introduces a new algorithm, dubbed SMART for Systematic Modular Automated Random Testing, that extends DART by testing functions in isolation, encoding test results as function summaries expressed using input preconditions and output postconditions, and then re-using those summaries when testing higher-level functions.

Korat

291 Citations2002Chandrasekhar Boyapati, Sarfraz Khurshid +1 more

Korat is a novel framework for automated testing of Java programs that uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size and generates test cases much faster than the declarative framework.