BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Scalable Software Model Checking for Finding Bugs in the Large 
DTSTART:20110621T141500
DTSTAMP:20260408T171857Z
UID:677bcf8338fb2452fb4df0a693b97f948c8290bad2320ca66968e751
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr Aarti Gupta\, NEC Laboratories America\nSoftware model chec
 king has become popular due to the success of predicate abstraction and re
 finement techniques in finding API usage bugs in programs.  In this talk\,
  I will describe an alternate approach we have taken for finding memory sa
 fety bugs (such as null pointer dereferences\, array buffer overflows\, st
 ring errors\, memory leaks)\, and\nviolations of API usage and user-specif
 ied assertions in C programs.\n\nThe highlights of our approach are:\n\n  
 - accurate memory modeling\, including an analysis-friendly\n    represent
 ation\n\n  - powerful static analyses based on abstract\n    interpretatio
 n\, to simplify models and find relatively\n    easy proofs of correctness
 \n\n  - efficient symbolic model checking\, to verify the\n    unresolved 
 properties and generate concrete error\n    traces.\n\nTo improve scalabil
 ity on large software projects\, we utilize a DC2 (Depth Cutoff with Desig
 n Constraints) framework. DC2 creates manageable partitions based on scope
  bounding\, and uses automated specification inference techniques to deriv
 e environment constraints for partitions and stubs for missing code. Furth
 ermore\, it can automatically suggest refinements of the environment contr
 aints based on counterexamples generated by a model checker\, if a user de
 ems a reported witness to be a false positive. We have implemented these\n
 ideas in the F-Soft verification platform\, which has been used successful
 ly to find bugs in many large open source as well as  industry software pr
 ojects. Dr Gupta's homepage
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR