<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><b>Software Testing and Verification with Grammatical Inference</b>
<br>
<b><a href="http://www.domagoj-babic.com/">Domagoj Babic</a></b>, <a href="http://www.berkeley.edu/">University of California, Berkeley</a>
<br>
<br>
Recent progress in automated deductive reasoning techniques has
triggered a small scientific revolution in automated software testing,
verification, and security. Indeed, it is becoming increasingly
difficult to find new automated software analysis papers that do not use
or assume existence of propositional satisfiability and
satisfiability-modulo theories solvers.
<p><br>
</p><p>In this talk, I will discuss the first results of my efforts to answer a
simple question: What kind of automated reasoning will trigger the next
scientific revolution in automated software analysis? As a potential
candidate, I will present grammatical inference (GI), a class of
techniques for learning formal languages. By inductively generalizing
from examples, GI techniques nicely complement the capabilities of
existing (deductive) approaches. Furthermore, the inferred grammars (or
automata) are themselves analyzable objects, which can be used as
approximations or abstractions of the behavior of the analyzed program.
</p><p><br>
</p><p>In this talk, I'll analyze several open problems, namely (1) test
generation for programs whose inputs have to adhere to complex
grammars, and (2) automated verification of web sanitizers, and offer
some solutions. The common trait of the above mentioned problems is
that they require exact or approximate understanding of the relation
between program's input and output. I'll explain how GI techniques can
infer such relations and serve as a basis for inventing new powerful
software analyses. In particular, I'll show that GI-based automated
testing can find six times more vulnerabilities than the
state-of-the-art methods, increasing code coverage by up to 58%. The
novel symbolic learning technique that I'll present learns input-output
relations of web sanitizers (for subsequent verification) in seconds,
while construction of the same relations used to take several hours of a
human expert's time in the past.
</p><p><br>
</p><p>Domagoj Babic received his Dipl.Ing. in Electrical Engineering and M.Sc.
in Computer Science from the Zagreb University (Faculty of Electrical
Engineering and Computing) in 2001 and 2003. He received his Ph.D. in
Computer Science in 2008 from the University of British Columbia. After
spending a bit more than a year in industry, he joined UC Berkeley, as a
research scientist.
</p><p><br>
</p><p>Domagoj's research focuses on various aspects of software analysis
(software verification, testing, and security), decision procedures,
grammatical inference, and applied formal methods in general.
</p><p><br>
</p><p>He is a recipient of the Canada's NSERC PDF Research Fellowship
(2010-2012), Microsoft Graduate Research Fellowship (2005-2007),
Fulbright Fellowship (declined to attend UBC), and several awards at
international programming competitions (1st place at the 2007
Satisfiability Modulo Theories competition in the bit-vector arithmetic
category and 3rd place at the 2005 Satisfiability Testing competition in
the satisfiable-crafted instances category).
</p>
<br>For more, see:<a href="http://www.domagoj.info/">http://www.domagoj.info/</a>
<div><span name="x"></span><br></div><br></div></body></html>