Bounded Model Checking and Inductive Verification of Hybrid Discrete-Continuous Systems

Bernd Becker, Markus Behle, Fritz Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Joerg Hoffmann, Daniel Kröning, Bernhard Nebel

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    29 Downloads (Pure)

    Abstract

    We present a concept to signicantly advance the state of the art for bounded model checking (BMC) and inductive verication (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from dierent domains, like hybrid systems modeling and digital circuit verication, bounded plan- ning and heuristic search, combinatorial optimization and integer programming. Af- ter sketching the overall verication ow we present rst results indicating that the combination and tight integration of dierent verication engines is a rst step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.
    Original languageEnglish
    Title of host publicationGI/ITG/GMM Workshop ''Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen''
    PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
    Publication date2004
    Publication statusPublished - 2004
    EventGI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" -
    Duration: 1 Jan 2004 → …

    Conference

    ConferenceGI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen"
    Period01/01/2004 → …

    Keywords

    • Hybrid system verification; bounded model checking; inductive verification; verification engines; BDD
    • SAT
    • and LP

    Fingerprint Dive into the research topics of 'Bounded Model Checking and Inductive Verification of Hybrid Discrete-Continuous Systems'. Together they form a unique fingerprint.

    Cite this