Workshop

LfSA 2012 - Logics for System Analysis

Berkeley, July 7, 2012

Program

9:00-10:00  Invited Talk
  • Radu Grosu (Vienna University of Technology)
    Time-Frequency Logic For Signal Processing
  • 10:00-10:30  Coffee Break
    10:30-12:00  Morning Session
  • Kazunori Ueda, Shota Matsumoto, Akira Takeguchi, Hiroshi Hosobe and Daisuke Ishii
    HydLa: A High-Level Language for Hybrid Systems
  • Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina.
    Interpolation-based Function Summaries in Bounded Model Checking (Presentation)
  • Vijay D'Silva, Leopold Haller, and Daniel Kroening.
    Abstract Conflict Driven Clause Learning (Discussion)
  • 12:00-14:00  Lunch Break
    14:00-15:00  Invited Talk
  • Ashish Tiwari (SRI)
    Verifying Safety of Hybrid Systems
  • 15:00-15:30  Coffee Break
    15:30-16:30  Afternoon Session
  • Olivier Bouissou, Samuel Mimram and Alexandre Chapoutot
    HySon: Precise Simulation of Hybrid Systems with Imprecise Inputs (Presentation)
  • Xinxin Liu and Bingtian Xue
    Decidability and Completeness of PDL through Canonical Model
  • Invited Talks

  • Radu Grosu (Vienna University of Technology)
    Time-Frequency Logic For Signal Processing (Invited Talk)
    In this talk I will first introduce Time-Frequency Logic (TFL), a new speci cation formalism for real-valued signals that combines temporal logic properties in the time domain with frequency-domain properties. I will then present a property checking framework for this formalism and demonstrate its expressive power to the recognition of musical pieces. Like hybrid automata and their analysis techniques, the TFL formalism is a contribution to a uni ed systems theory for hybrid systems
    This is joint work with Alexandre Donze, Oded Maler, Dejan Nickovic, Ezio Bartocci and Scott Smolka.
  • Ashish Tiwari (SRI)
    Verifying Safety of Hybrid Systems (Invited Talk)
    The safety verification problem for hybrid systems asks if a hybrid system can ever reach an undesirable state. There are at least three different approaches that have been studied for solving this problem: (a) reach set computation by applying abstract interpretation on the hybrid dynamics (b) abstraction of the hybrid system and model checking the abstract system (c) direct proof of safety by demonstrating existence of an inductive invariant
    In this talk, we argue that ideas from each of the three approaches can be used to improve the other approaches. We present three concrete safety verification techniques: qualitative abstraction, inductive invariants, and relational abstraction, and show how ideas from one influence the other techniques.
  • Proceedings

    Here is hand-out of the Proceedings of LfSA'12 for the workshop.