BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Reasoning Challenges for Guard Applications
DTSTART:20120604T140000
DTEND:20120604T150000
DTSTAMP:20260407T210755Z
UID:f03e72cfbb9e2677fbc7e7542c82388edf7a9da9210d308d725a444d
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr. Mike Whalen\, University of Minnesota Software Engineering
  Center\, USA\nAbstract :\nGuardol is a domain-specific language designed 
 to facilitate the construction of correct network guards operating over tr
 ee-shaped data. The Guardol system generates Ada code from Guardol program
 s and also provides speci cation and automated veri cation support.\nGuard
  programs and specications are translated to higher order logic\, then ded
 uctively transformed to a form suitable for a SMT-style decision procedure
  for recursive functions over tree-structured data.\nThe result is that ce
 rtain complex properties of Guardol programs can be proved fully automatic
 ally.  Reasoning challenges for guards involve several aspects:\n   - R
 easoning about tree structured data\n   - Reasoning about strings\n   
 - Reasoning about arrays\nas well as language design to easily support suc
 h reasoning.  In this talk we describe how some of these challenges have 
 been addressed\, and how several are yet to be addressed.\n\nBio :\nSoftwa
 re plays an increasing role in the operation of critical systems. As these
  systems become more complex\, ensuring software correctness becomes much 
 more difficult. I am interested in automated formal techniques for precise
 ly specifying\, implementing\, and verifying software. To support these ac
 tivities\, I have developed several translation and analysis tools to supp
 ort formal reasoning and test case generation. I have significant experien
 ce in applying formal verification and auto-test generation techniques to 
 production DO178B Level A and B avionics software development efforts.\nI 
 have 15 years experience in software development and analysis\, including 
 10 years experience in Model-Based Development & safety-critical systems. 
 Most of that time has been spent developing simulation\, translation\, tes
 ting\, and formal analysis tools for Model-Based Development languages inc
 luding Simulink\, Stateflow\, Lustre\, and RSML-e. I have led successful f
 ormal verification projects on large industrial avionics models\, includin
 g displays (Rockwell-Collins ADGS-2100 Window Manager)\, redundancy manage
 ment and control allocation (AFRL CerTA FCS program) and autoland (AFRL Ce
 rTA CPD program). I was the lead developer of the Rockwell-Collins Gryphon
  tool suite\, which can be used for compilation\, test-case generation\, a
 nd formal analysis of Simulink/Stateflow models. This tool suite has been 
 used both for academic research and industrial verification projects.\nI c
 ompleted my PhD at the University of Minnesota in January\, 2005.  As a g
 raduate student\, I worked in the Critical Systems Research Group ( CriSys
  )\, where I helped design a synchronous language called Requirements Stat
 e Machine Language without Events (RSML-e).  My Masters thesis provided t
 he first complete formalization of RSML-e\, written in the Z formalism. Th
 is formalization has formed the backbone of the RSML-e NIMBUS Simulator an
 d translation tools from RSML-e to model checking and theorem proving tool
 s.  My PhD dissertation re-formalized RSML-e using higher-order abstract 
 syntax and structural operational semantics to create a provably-correct t
 ranslator from RSML-e to a subset of C.
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR