• Welcoming
Session 1 (CPS Design)
[Chair: Jim Kapinski]
  • Invited talk (45mn): Zhi Han
    Title: Accelerating Model-Based Development with Integrated Formal Verification using Simulink Design Verifier
  • Contributed paper (25mn): Fribourg Laurent and Romain Soulat
    Title: Stable Limit Cycles for Sampled Switched Systems
Coffee Break 10-10:30
Session 2 (Abstract Interpretation)
[Chair: Sylvie Putot]
  • Invited talk (50mn): Arnaud J. Venet
    Title: Putting Numerical Abstract Domains to Work: A Study ofArray-Bound Checking for C Programs
  • Contributed paper (25mn): Pierre Roux and Pierre-Loic Garoche
    Title: A Polynomial Template Abstract Domain based on Bernstein Polynomials
Lunch break 12-1:30
Session 3 (Program Synthesis)
[Chair: Swarat Chaudhuri]
  • Invited talk (50mn): Ashish Tiwari
    Title: Automated Safety Analysis for Hybrid Systems
  • Contributed paper (25mn): Susmit Jha and Sanjit A. Seshia
    Title: From Verification to Synthesis of Fixedpoint Implementation of Numerical Software Routines
Coffee Break 3-3:30
Session 4 (Formal Specification)
[Chair: Alwyn E. Goodloe]
Plenary discussion
  • Workshop future
  • Closing comments