english only
EPFL > I&C > Tresor > Seminars
RESOURCES
Home
People
Seminars
Courses
Research Topics
Events
Useful Links

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
seminars:2010 [2010/06/29 15:31]
psuter
seminars:2010 [2010/08/27 10:50]
hojjat
Line 192: Line 192:
  
 We have implemented our type system as an extension to Scala. Practical experience suggests that our system allows type checking real-world actor-based concurrent programs with only a small number of additional type annotations. We have implemented our type system as an extension to Scala. Practical experience suggests that our system allows type checking real-world actor-based concurrent programs with only a small number of additional type annotations.
 +
 +\\
 +\\
 +===== Model Checking using Bounded Languages =====
 +
 +  * 2010-07-07 - 16:15, [[http://​plan.epfl.ch/?​lang=en&​room=INR113|INR 113]], [[http://​www.cs.ucla.edu/​~rupak/​|Prof. Rupak Majumdar]]
 +
 +Abstract:
 +
 +Bounded languages, introduced by Ginsburg and Spanier, are subsets of
 +regular languages of the form w1*w2*... wk* for some words
 +w1,...,wk. Bounded languages have nice structural and decidability ​
 +properties.
 +
 +We show two applications of bounded languages in model checking:
 +first, to underapproximate the reachable state space of multithreaded ​
 +procedural programs and
 +second, to underapproximate the reachable state space of counter machines.
 +In particular, we show that verification with bounded languages
 +generalizes context-bounded reachability for multithreaded programs.
 +
 +We also show a new and constructive proof of the following ​
 +language-theoretic
 +result: for every context-free language L, there is a bounded ​
 +context-free language
 +L' which is a subset of L and has the same Parikh image as L.
 +
 +(Joint work with Pierre Ganty and Benjamin Monmege)
 +
 +\\
 +\\
 +===== Automatically Identifying Critical Input Regions and Code in Applications =====
 +
 +  * 2010-07-09 - 15:15, [[http://​plan.epfl.ch/?​lang=en&​room=BC229|BC229]],​ [[http://​people.csail.mit.edu/​mcarbin|Michael Carbin]], MIT CSAIL
 +
 +Abstract:
 +
 +Applications that process complex inputs often react in different ways to changes in different regions of the input. Small changes to forgiving regions induce correspondingly small changes in the behavior and output. Small changes to critical regions, on the other hand, can induce disproportionally large changes in the behavior or output. Identifying the critical and forgiving regions in the input and the corresponding critical and forgiving regions of code is directly relevant to many software engineering tasks.
 +
 +In this talk, I will present a system, Snap, for automatically grouping related input bytes into fields and classifying each field and corresponding regions of code as critical or forgiving. Given an application and one or more inputs, Snap uses targeted input fuzzing in combination with dynamic execution and influence tracing to classify regions of input fields and code as critical or forgiving. Our experimental evaluation shows that Snap makes classifications with close to perfect precision (99%) and very good recall (between 99% and 73%, depending on the application).
 +\\
 +\\
 +===== Solvers for Software Reliability and Security =====
 +
 +  * 2010-07-23 - 15:15, [[http://​plan.epfl.ch/?​lang=en&​room=BC229|BC 229]], [[http://​people.csail.mit.edu/​vganesh|Dr. Vijay Ganesh]], MIT CSAIL
 +
 +Abstract:
 +
 +Constraint solvers play a central role in the construction of reliable and secure software, regardless of whether such software is based on formal methods, program analysis, testing or synthesis. In this talk, I will present two solvers namely, STP and HAMPI. STP extends SAT solvers with the theory of bit-vectors and arrays, and has enabled a new testing technique known as Concolic Testing. STP-enabled Concolic testers have been used to find hundreds of previously unknown bugs in Unix utilities, OS kernels, media players, and commercial software, some with approximately a million lines of code. HAMPI is designed for the analysis of string-manipulating programs and incorporates a rich theory of equality over bounded string variables, bounded regular expressions,​ and context-free grammars. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis. I will discuss techniques that make these solvers scale to large formulas obtained from real-world applications,​ and some related theoretical results.
 +
 +Bio:
 +
 +Dr. Vijay Ganesh is a Research Scientist at MIT since 2007. He completed his PhD in computer science from Stanford University in 2007, and Bachelor of Technology from College of Engineering,​ Trivandrum, India. His primary research interests are constraint solvers and their applications to software reliability,​ computer security and biology. His STP solver was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006, and his paper on HAMPI won the ACM Distinguished Paper Award in 2009.