Organized by Mani Chandy, Richard Murray, Paulo Tabuada, and Ufuk Topcu.
Findings of the workshop will be summarized in a report that will be available here following the workshop.
Description
Formal verification and validation (V&V) have been subject to research in controls, computer science, and networking but often in isolation from each other. With recent convergence of controls, computation, and communication, there is a need for unified theories and algorithms. Despite advances in V&V tools in respective areas, such unification is in its infancy. Moreover, rigorous V&V for systems of current interest is a complicated task due to common difficulties including the interaction the software and the physical world, untraditional information flow, modeling/environmental uncertainties, and unavoidable explosion of computational complexity of the currently available tools (in both domains).
We believe that the success of formal methods and V&V in the intersection of controls, computer science, and networking is stringent on the development truly hybrid methods that blend ideas from all these areas and possibly others. The main purpose of the proposed workshop is to bring experts from academia, industry, and governmental agencies together and promote exchange of ideas and establishment of interdisciplinary collaborations. We will emphasize the integration of the tools and ideas from these fields to lead to a unified toolset. Moreover, we are expecting to highlight current trends and future directions in V&V research as well as industrial needs and requirements for V&V through outlook sessions and talks by experts from the industry and government agencies.
Speakers and titles of their presentations
NOTE: The “pdf version” following a title links to the copies written to pdf from either ppt or pptx. They may not properly display certain figures, animations, and/or equations. In that case, please try to download and open the original copies in ppt or pptx (clicking directly on the title).
Karl-Erik Arzen “On verification and validation of real-time control systems: Formal Approaches vs Simulation” pdf version
Gerard Holzmann “The practice of formal methods” pdf version
Brian Williams “Managing risk and uncertainty in model-based programs” pdf version
Mani Chandy “New models and theory for game theory with message passing” pdf version
Nancy Leveson “A new control theoretic foundation for safety engineering” pdf version
Rupak Majumdar “Symbolic robustness analysis” pdf version
Koushik Sen “Testing concurrent programs”
Sayan Mitra “Replication-based fault-tolerance of wireless distributed control systems” pdf version
Stavros Tripakis “Implementation of synchronous programs on asynchronous execution platforms: correctness, modularity, and performance analysis”
Edmund Clarke “Model checking: making it scale” pdf version
Eric Feron “Control systems software assurance”
Rajeev Alur “Interfaces for control components” pdf version
Allessandro Pinto “Formal verification and analytical methods for complex systems: The UTRC experience”
Andrew Packard “Quantitative local analysis for continuous nonlinear systems” pdf version
Ashish Tiwari “Verification using constraint solving”
Domitilla Del Vecchio “Dynamic feedback for hybrid systems on a partial order” pdf version
Calin Belta “Formal approaches to robot motion planning and control”
Paulo Tabuada “From formal verification to formal synthesis”
Andre Platzer “Hybrid logical verification for hybrid systems”
Slides presented by the panelists
The Caltech Verification and Validation Workshop, 2009 is sponsored by Caltech’s Center for the Mathematics of Information and the Air Force Office of Scientific Research (through the MURI “Specification, Design and Verification of Distributed Embedded Systems”).
The workshop will be held in Annenberg Building room 105. The location of this building in Caltech campus is marked in the map.
Slides presented by Yaniv Saar on Sept 25 (at Caltech) “Solving reactive games - a case study for JTLV”