-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathprogram.html
194 lines (171 loc) · 9.35 KB
/
program.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
<head>
<title>Program | TAPAS 2013: Workshop on Tools for Automatic Program Analysis</title>
<meta name="description" content="Submit Analyzer Pearls by 13 April 2013. The Fourth Workshop on Tools for Automatic Program Analysis will be held on 19 June 2013, is an SAS 2013 affiliated event, and is co-located with PLDI 2013." />
<meta name="keywords" content="tools, program analysis, static analysis" />
<meta http-equiv="content-type" content="text/html; charset=utf-8" />
<meta http-equiv="X-UA-Compatible" content="IE=9" />
<link rel="stylesheet" type="text/css" href="css/style.css" />
<script type="text/javascript" src="js/jquery.min.js"></script>
<script type="text/javascript" src="js/image_slide.js"></script>
<script type="text/javascript">
var _gaq = _gaq || [];
_gaq.push(['_setAccount', 'UA-25127606-1']);
_gaq.push(['_trackPageview']);
(function() {
var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
})();
</script>
</head>
<body>
<div id="main">
<div id="header">
<div id="banner">
<div id="welcome">
<h1>TAPAS 2013</h1>
</div><!--close welcome-->
<div id="welcome_slogan">
<h1>The Fourth Workshop on <u>T</u>ools for
<u>A</u>utomatic <u>P</u>rogram <u>A</u>nalysi<u>s</u></h1>
</div><!--close welcome_slogan-->
</div><!--close banner-->
</div><!--close header-->
<div id="menubar">
<ul id="menu">
<li><a href="index.html">Home</a></li>
<li class="current"><a href="program.html">Program</a></li>
</ul>
</div><!--close menubar-->
<div id="site_content">
<div class="sidebar_container">
<div class="sidebar">
<div class="sidebar_item">
<p>affiliated with
<a
href="http://research.microsoft.com/en-us/events/sas2013/">SAS
2013</a></p>
<p>co-located with
<a href="http://pldi2013.ucombinator.org/">PLDI 2013</a></p>
</div>
</div>
</div><!--close sidebar_container-->
<div id="content">
<div class="content_item">
<h2>Program</h2>
<table>
<tr>
<td>08:00-09:00am</td>
<td>Breakfast</td>
</tr>
<tr>
<td>09:00-09:10am</td>
<td>Welcome (Belltown)</td>
</tr>
<tr>
<td>09:10-10:00am</td>
<td>
<b>Invited Talk</b><br>
Chair: Bor-Yuh Evan Chang<br>
<a href="http://research.microsoft.com/en-us/people/sriram/">Sriram
Rajamani</a> (Microsoft Research India)
<p><i><a href="#rajamani">Probabilistic Programming: A Program Analysis Perspective</a></i></p>
</td>
</tr>
<tr>
<td>10:30-11:20am</td>
<td>
<b>Invited Talk</b><br>
Chair: Ranjit Jhala<br>
<a href="http://www7.in.tum.de/~rybal/">Andrey
Rybalchenko</a> (Microsoft Research Cambridge and Technische Universität München)
<p><i><a href="#rybalchenko">Solving Quantified Horn Clauses</a></i></p>
</td>
</tr>
<tr>
<td>11:20-11:45am</td>
<td>
<p><a href="http://www.cs.utah.edu/~liangsy/">Shuying Liang</a>,
<a href="http://matt.might.net">Matthew Might</a>,
and <a href="http://www.ccs.neu.edu/home/dvanhorn/">David
Van Horn</a>. <i>AnaDroid: Malware Analysis of
Android with User-supplied Predicates</i>.</p>
</td>
</tr>
<tr>
<td>12:00-01:30pm</td>
<td>Lunch</td>
</tr>
<tr>
<td>01:30-02:20pm</td>
<td>
<b>Invited Talk</b><br>
Chair: Werner Dietl<br>
<a href="http://theory.stanford.edu/~aiken/">Alex Aiken</a>
(Stanford University)
<p><i><a href="#aiken">Using Learning Techniques in Invariant Inference</a></i></p>
</td>
</tr>
<tr>
<td>02:20-02:45pm</td>
<td>
<p>
<a href="http://cs.wisc.edu/~adi">Aditya Thakur</a>,
<a href="http://research.microsoft.com/en-us/people/akashl/">Akash
Lal</a>,
<a href="http://cs.wisc.edu/~junghee">Junghee Lim</a>,
and <a href="http://www.cs.wisc.edu/~reps/">Thomas
Reps</a>. <i>PostHat and All That: Automating
Abstract Interpretation</i>.</p>
</td>
</tr>
<tr>
<td>03:15-04:05pm</td>
<td>
<b>Invited Talk</b><br>
Chair: Ben Hardekopf<br>
<a href="http://researcher.watson.ibm.com/researcher/view.php?person=us-dolby">Julian
Dolby</a> (IBM T.J. Watson Research Center)
<p><i><a href="#dolby">The End of Pointer Analysis?</a></i></p>
</td>
</tr>
<tr>
<td>04:05-04:20pm</td>
<td>Conclusion</td>
</tr>
</table>
<h2>Abstracts</h2>
<h3 id="rajamani">Sriram Rajamani</h3>
<p>Probabilistic Programming: A Program Analysis Perspective</p>
<p>Probabilistic models, particularly those with causal dependencies, can be succinctly written as probabilistic programs. Recent years have seen a proliferation of languages for writing such probabilistic programs, as well as tools and techniques for performing inference over these programs. In this talk, we show that static and dynamic program analysis techniques can be used to infer quantities of interest to the machine learning community, thereby providing a new and interesting domain of application for program analysis. In particular, we show that static analysis techniques inspired by dataflow analysis and iterative refinement techniques can be used for Bayesian inference. We also show that dynamic analysis techniques inspired by directed testing and symbolic execution can be used for sampling probabilistic programs.</p>
<p>Joint work with Aditya Nori, Andy Gordon, Arun Chaganty, Akash Lal, Johannes Borgstorm and Guillaume Claret.</p>
<h3 id="rybalchenko">Andrey Rybalchenko</h3>
<p>Solving Quantified Horn Clauses</p>
<p>
Quantified Horn clauses can be used to represent proof obligations for a variety of verification and synthesis tasks, e.g., proving existential temporal properties, solving games, and dealing with container data structures.
We discuss application scenarios for quantified Horn clauses and briefly overview solving approaches, as well as experience with extending our solver ARMC to support quantification.
</p>
<p>
Joint work with Tewodros Beyene, Nikolaj Bjorner, Swarat Chaudhuri, Ken McMillan, and Corneliu Popeea.
</p>
<h3 id="aiken">Alex Aiken</h3>
<p>Using Learning Techniques in Invariant Inference</p>
<p>Arguably the hardest problem in automatic program analysis is designing appropriate techniques for discovering loop invariants (or, more generally, for recursive procedures). Certainly, if invariants are known, the rest of the analysis problem becomes easier. This talk presents a family of invariant inference techniques based on using test cases to generate an underapproximation of program behavior and then using machine learning algorithms to generalize the underapproximation to an invariant. These techniques are simpler, much more efficient, and appear to be more robust than previous approaches to the problem. If time permits, some open problems will also be discussed.</p>
<h3 id="dolby">Julian Dolby</h3>
<p>The End of Pointer Analysis?</p>
<p>
Pointer analysis means computing an approximation of the possible objects to which any program variable may refer; it has traditionally been done by conservatively approximating all possible data flow in the program, resulting in a conservative approximation of the objects held by any variable. This has always been a bit fake---no tools soundly approximates all possible reflective and JNI behavior in Java, for instance---but even the comforting illusion of soundness has become unsustainable in the world of framework- and browser-based Web applications. The frameworks are built on ubiquitous complex reflective behavior, and the browser appears as a large, complex, poorly-specified native API; the frameworks and the applications themselves are written in JavaScript, the lingua franca of the Web, the dynamic nature of which give pointer analysis no help. Whether this world can be analyzed soundly is perhaps technically still an open problem, but the prognosis seems grim at best.
</p>
<p>
We have been exploring deliberately unsound analyses which make no attempt to approximate all possible data flow in a program; certain constructs are ignored not because they are unimportant, but simply because they are too hard. The tradeoff is now between how much can we ignore and still provide useful information versus how little can we ignore and still be tractable in practice. The good news so far is that there appear to be good tradeoffs, at least for a range of applications supporting IDE services. I will discuss recent and ongoing work in providing key information for IDE services: callgraphs and smart completions.
</p>
</div><!--close content_item-->
</div><!--close content-->
</div><!--close site_content-->
</div><!--close main-->
<div id="footer">
</div><!--close footer-->
</body>
</html>