Compositional and contract-based verification for autonomous driving on road networks

Lucas Liebenwein, Wilko Schwarting, Cristian-Ioan Vasile, Jonathan DeCastro, Javier Alonso Mora, Sertac Karaman, Daniela Rus

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

15 Downloads (Pure)


Recent advances in autonomous driving have raised the problem of safety
to the forefront and incentivized research into establishing safety guarantees. In this paper, we propose a safety verification framework as a safety standard for driving controllers with full or shared autonomy based on compositional and contract-based principles. Our framework enables us to synthesize safety guarantees over entire road networks by first building a library of locally verified models, and then composing local models together to verify the entire network. Composition is achieved using assume-guarantee contracts that are synthesized concurrently during verification. Thus, we can reuse local models within and across networks, add additional models to cover local road geometries without re-verifying the entire library, and perform all computations in a parallel and distributed way, which enables computational tractability. Furthermore, we employ controller contracts such that any controller satisfying them can be certified safe. We demonstrate the practical effectiveness of our framework by certifying controllers over parts of the Manhattan road network.
Original languageEnglish
Title of host publicationProceedings ot the International Symposium on Robotics Research (ISRR)
Place of PublicationCambridge, MA, USA
Number of pages16
Publication statusPublished - 2017
EventISRR 2017: 18th International Symposium on Robotics Research - Puerto Varas, Chile
Duration: 11 Dec 201714 Dec 2017


ConferenceISRR 2017: 18th International Symposium on Robotics Research
CityPuerto Varas


  • Verification
  • Safety
  • Autonomous Car
  • Composition
  • Contracts

Fingerprint Dive into the research topics of 'Compositional and contract-based verification for autonomous driving on road networks'. Together they form a unique fingerprint.

Cite this