BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20100314T020000 RDATE:20100314T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100422T155706Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100427T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100427T103000 DTSTAMP;VALUE=DATE-TIME:20100422T155706Z LAST-MODIFIED;VALUE=DATE-TIME:20100422T155706Z UID:http://calagator.org/events/1250458589 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\nThe talk will be held at \;\n \;\nGalois Inc. \;\n421 SW 6th Ave. S uite 300\, Portland\, OR\, USA \;\n(3rd floor of the Commonwealth bui lding) \;\n \;\nVisualizing Information Flow through C Programs 3\;\n \;\nDetails: \;\n \;\n * Presenter: Joe Hurd \;\n * Date: Tuesday April 27\, 2010 \;\n * Time: 10:30am \;\n \;\nAbstract: The aim of the Automated Security Analysis project is to d etermine whether the information flows in a realistically-sized C codeba se can be automatically deduced and communicated in an understandable wa y to someone unfamiliar with the code. To test this\, a new information flow static analysis and visualization technique were developed\, and im plemented in a research prototype tool. This talk will present the novel features of the static analysis and demonstrate how the results are sho wn in the visualization tool: information flow between program storage l ocations is decomposed into two compositional properties\, which can be computed using sound abstract interpretation techniques. For each deduce d information flow\, the static analysis keeps track of a set of source code locations which demonstrate the information flow\, and this is used by the visualization component to communicate the information flow to a user browsing the source code. \;\n \;\nBio: Joe Hurd\, Ph.D. is a Formal Methods Engineer at Galois\, Inc. For the past ten years Dr. Hu rd has been applying theorem proving techniques to formally verify the c orrectness of complex software\, including probabilistic programs\, elli ptic curve cryptography and game tree analysis algorithms. He is also th e developer of Metis\, an automatic theorem prover for first order logic \, and coordinates the OpenTheory project\, a package management system for higher order logic theories. Dr. Hurd is an active member of the the orem proving research community\, having organized conferences in 2005 a nd 2008\, given invited talks\, and regularly appears on program committ ees and reviews papers for conferences and journals. Prior to joining Ga lois in 2007\, Dr. Hurd was a research fellow at Magdalen College\, Univ ersity of Oxford. He studied at the University of Cambridge\, receiving a Masters level degree in Mathematics in 1997\, and a Ph.D. in Computer Science in 2002.\n\nImported from: http://calagator.org/events/125045858 9 URL:http://www.galois.com/blog/2010/04/22/tech-talk-visualizing-informati on-flow-through-c-programs/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR