Tata Institute of Fundamental Research
Automated Test Generation Using Concolic Testing
Seminar
Speaker:
Koushik Sen (University of California, Berkeley
Department of Electrical Engineering and
Computer Sciences
581 Soda Hall # 1776
United States of America)
Organiser:
R K Shyamasundar
Date:
Tuesday, 3 Jun 2014, 11:30 to 12:30
Venue:
AG-66 (Lecture Theatre)
(Scan to add to calendar)
Abstract:
Abstract: In this talk, I will describe concolic testing, also known as directed automated random testing (DART) or dynamic symbolic execution, an efficient way to automatically and systematically generate test inputs for programs. Concolic testing uses a combination of runtime symbolic execution and automated theorem proving techniques to automatically generate non-redundant and exhaustive test inputs. Specifically, concolic testing performs symbolic execution along a concrete execution path, generates a logical formula denoting a constraint on the input values, and solves a constraint to generate new test inputs that would execute the program along previously unexplored paths. Concolic testing has inspired the development of several industrial and academic automated testing and security tools such as PEX, SAGE, and YOGI at Microsoft, Apollo at IBM, Conbol at Samsung, and CUTE, jCUTE, CATG, Jalangi, SPLAT, BitBlaze, jFuzz, Oasis, and SmartFuzz in academia. A central reason behind the wide adoption of concolic testing is that, while concolic testing uses program analysis and automated theorem proving techniques internally, it exposes a testing usage model that is familiar to most software developers.
| Speaker: | Koushik Sen (University of California, Berkeley Department of Electrical Engineering and Computer Sciences 581 Soda Hall # 1776 United States of America) |
| Organiser: | R K Shyamasundar |
| Date: | Tuesday, 3 Jun 2014, 11:30 to 12:30 |
| Venue: | AG-66 (Lecture Theatre) |
(Scan to add to calendar)
Abstract:
Abstract: In this talk, I will describe concolic testing, also known as directed automated random testing (DART) or dynamic symbolic execution, an efficient way to automatically and systematically generate test inputs for programs. Concolic testing uses a combination of runtime symbolic execution and automated theorem proving techniques to automatically generate non-redundant and exhaustive test inputs. Specifically, concolic testing performs symbolic execution along a concrete execution path, generates a logical formula denoting a constraint on the input values, and solves a constraint to generate new test inputs that would execute the program along previously unexplored paths. Concolic testing has inspired the development of several industrial and academic automated testing and security tools such as PEX, SAGE, and YOGI at Microsoft, Apollo at IBM, Conbol at Samsung, and CUTE, jCUTE, CATG, Jalangi, SPLAT, BitBlaze, jFuzz, Oasis, and SmartFuzz in academia. A central reason behind the wide adoption of concolic testing is that, while concolic testing uses program analysis and automated theorem proving techniques internally, it exposes a testing usage model that is familiar to most software developers.