Campus Event Calendar
Event Entry
What and Who
Structural Abstraction of Software Verification Conditions--
Domagoj Babic, UBC.
U of British Columbia
SWS Colloquium
Domagoj Babic is a Ph.D. candidate at the University of British Columbia.
His research interests include software verification and analysis,
as well as automated theorem proving and SAT solving. Domagoj is
currently working on a scalable and precise static checker Calysto, and
a bit-vector decision procedure Spear for software verification. He is
planning to graduate in early spring 2008.
Domagoj holds a M.Sc. degree in computer science and a Dipl.Ing. degree
in industrial electronics from the Faculty of Electrical Engineering and
Computing at Zagreb University.
For more information, see http://www.domagoj.info/
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 27 September 2007
15:00
60 Minutes
E1 5
rotunda 6th floor
Saarbrücken
Abstract
Precise software analysis and verification require tracking the exact path
along which a statement is executed (path-sensitivity), the different
contexts from which a function is called (context-sensitivity), and the
bit-accurate operations performed. Previously, verification with such
precision has been considered too inefficient to scale to large software.
In this talk, Domagoj presents a novel approach to solving such verification
conditions, based on an automatic abstraction-checking-refinement framework
that exploits natural abstraction boundaries present in software.
Experimental results show that our approach scales to over 200,000 lines of
real C code.
Contact
Brigitta Hansen
0681 9325200
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 09/25/2007 15:14 -- Created document.