go to the list of abstracts

go to the list of previous talks
previous talks

go to the list of other SCS seminars
scs seminars

go to the SCS home page

go to the CMU home page


The Next Talk Fa'14 Talks General Info Speaking Req't

Formal Verification of Distributed Aircraft Controllers

Tuesday, November 4th, 2014 from 12-1 pm in GHC 6501.

Sarah Loos, CSD

Formal verification and theorem proving have been used successfully in many discrete applications, such as chip design and verification. However, computation is not confined to the discrete world of desktop computing. Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems (for example, adaptive cruise control in cars and collision avoidance in aircraft). It is vital that these hybrid (discrete and continuous) systems behave as designed, or they will cause more damage than they intend to fix. In this talk, I will present several challenges associated with verifying hybrid systems and how we can use differential dynamic logic and its proof calculus to ensure safety for hybrid systems under a continuously infinite range of circumstances.

In addition to covering the theoretical foundations for deductive verification of hybrid systems, I will discuss some of the practical uses of our verification tools:KeYmaera and KeYmaeraD. These tools have been used to verify a class of distributed collision avoidance controllers designed to work in environments with arbitrarily many aircraft. We prove that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver that the new plane may not be aware of. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior, which simulation and testing may miss.

This is joint work with André Platzer and David Renshaw.

In Partial Fulfillment of the Speaking Requirement.

Fall 2014 Schedule
Tue, Sep 2 GHC 6501 AVAILABLE
Fri, Sep 5 GHC 4303 AVAILABLE
Tue, Sep 9 GHC 6501 AVAILABLE
Fri, Sep 12 GHC 4303 AVAILABLE
Tue, Sep 16 GHC 6501 AVAILABLE
Fri, Sep 19 GHC 4303 AVAILABLE
Tue, Sep 23 GHC 6501 AVAILABLE
Fri, Sep 26 GHC 4303 AVAILABLE
Tue, Sep 30 GHC 6501 AVAILABLE
Fri, Oct 3 GHC 4303 Arbob Ahmad Declassification and Authorization in Epistemic Logic
Tue, Oct 7 GHC 6501 AVAILABLE
Fri, Oct 10 GHC 4303 AVAILABLE
Tue, Oct 14 GHC 6501 AVAILABLE
Fri, Oct 17 GHC 4303 AVAILABLE
Tue, Oct 21 GHC 6501 AVAILABLE
Fri, Oct 24 GHC 4303 AVAILABLE
Mon, Oct 27 GHC 7101 Flavio Cruz Forward-Chaining Linear Logic Programming for Parallel Programming Over Graph Structures
Fri, Oct 31 GHC 4303 AVAILABLE
Tue, Nov 4 GHC 6501 Sarah Loos Formal Verification of Distributed Aircraft Controllers
Fri, Nov 7 GHC 4303 AVAILABLE
Tue, Nov 11 GHC 6501 Akshay Krishnamurthy Adaptive Sampling with Matrices
Fri, Nov 14 GHC 4303 Timothy Zhu PriorityMeister: Tail Latency QoS for Shared Networked Storage
Tue, Nov 18 GHC 6501 AVAILABLE
Fri, Nov 21 GHC 4303 Lin Xiao TBA
Tue, Nov 25 GHC 6501 Yong He Extending the Graphics Pipeline with Adaptive, Multi-rate Shading
Fri, Nov 28 GHC 4303 Thanksgiving Break UNAVAILABLE
Tue, Dec 2 GHC 6501 Kuen-Bang Hou (Favonia) TBA
Fri, Dec 5 GHC 4303 AVAILABLE
Tue, Dec 9 GHC 6501 AVAILABLE
Fri, Dec 12 GHC 4303 AVAILABLE
Tue, Dec 16 GHC 6501 AVAILABLE

General Info

The Student Seminar Series is an informal research seminar by and for SCS graduate students from noon to 1 pm on Tuesdays and Fridays. Lunch is provided by the Computer Science Department (personal thanks to Sharon Burks and Debbie Cavlovich!). At each meeting, a different student speaker will give an informal, 40-minute talk about his/her research, followed by questions/suggestions/brainstorming. We try to attract people with a diverse set of interests, and encourage speakers to present at a very general, accessible level.

So why are we doing this and why take part? In the best case scenario, this will lead to some interesting cross-disciplinary work among people in different fields and people may get some new ideas about their research. In the worst case scenario, a few people will practice their public speaking and the rest get together for a free lunch.

Guideline & Speaking Requirement Need-to-Know

Note: Step #1 below are applicable to all SSS speakers. You can schedule AT MOST THREE talks per semester.

SSS is an ideal forum for SCS students to give presentations that count toward fulfilling their speaking requirements. The specifics, though, vary with each department. For instance, students in CSD will need to be familiar with the notes in Section 8 of the Ph.D. document and follow the instructions outlined on the Speakers Club homepage. Roughly speaking, these are the steps:

  1. Schedule a talk with SSS by sending your talk title, abstract, additional info (like "Joint work with..." or "In Partial Fulfillment of the Speaking Requirement"), and a picture of yourself (preferably jpeg) to sss@cs at least TWO WEEKS before your scheduled talk.
  2. After you are confirmed with your SSS slot, go to the Speakers Club Calendar and schedule your talk at least THREE WEEKS in advance of the talk date.
  3. On the day of your talk, make sure you print Speakers Club evaluation forms for your evaluators to use.
Students outside of CSD will need to check with their respective departments regarding the procedure. As another example, ISRI students fulfill their speaking requirements by attending a semesterly Software Research Seminar and giving X number of presentations per school year. If you have experience with your department that might help others in your department, please feel free to contribute your knowledge by emailing us. Thank you!

SSS Coordinators

Armaghan Naik, Computational Biology
Lin Xiao, CSD


Web contact: sss+www@cs