Re: [pl-seminar] No PL seminar tomorrow - TALK Today instead

[Alisa Maas <ajmaas@xxxxxxxxxxx>]

PS: Cookies starting at 3:45, if the talk wasnât incentive enough to go.

On Apr 18, 2016, at 2:01 PM, Loris D'Antoni <loris@xxxxxxxxxxx> wrote:

If you don't have class, you should definitely attend Akash's talk today.

-----

Inferring Annotations from Verification Histories [2]
Monday, April 18, 2016 - 4:00pm to 5:00pm
1240 CS
Akash Lal
Microsoft Research India
Finding invariants is an important step in automated program analysis.
Discovery of precise invariants, however, can be very difficult in practice.
The problem can be simplified if one has access to a candidate set of
predicates (or annotations) and the search for invariants is limited over the
space defined by these annotations.

We present an approach that infers program annotations automatically by
leveraging the history of verifying related programs. Our algorithm extracts
high-quality annotations from previous verification attempts, and then
applies them for verifying new programs.  We present a case study where we
applied our techniques to Microsoft's Static Driver Verifier (SDV).

SDV currently uses manually-tuned heuristics for obtaining a set of
annotations. Our techniques not only can replace the need for this manual
effort, they even outperform these heuristics and improve the performance of
SDV overall.

Speaker's Bio: Akash Lal is a Researcher at Microsoft Research India, which
he joined in 2009 after receiving his Ph.D. from the Computer Sciences
Department of the University of Wisconsin-Madison. For his thesis, he was a
co-recipient of both the UW CS Outstanding Graduate Student Research Award
and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. In 2011, Akash
was named to MIT Technology Review's 2011 India TR-35 list (top innovators
under 35).

_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar