CISPA
Browse

Iterative Circuit Repair Against Formal Specifications

Download (557.76 kB)
Version 2 2023-12-11, 20:16
Version 1 2023-11-29, 18:24
conference contribution
posted on 2023-12-11, 20:16 authored by Matthias CoslerMatthias Cosler, Frederik SchmittFrederik Schmitt, Christopher Hahn, Bernd FinkbeinerBernd Finkbeiner
We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by 6.8 percentage points on held-out instances and 11.8 percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.

History

Preferred Citation

Matthias Cosler, Frederik Schmitt, Christopher Hahn and Bernd Finkbeiner. Iterative Circuit Repair Against Formal Specifications. In: International Conference on Learning Representations (ICLR). 2023.

Primary Research Area

  • Threat Detection and Defenses

Name of Conference

International Conference on Learning Representations (ICLR)

Legacy Posted Date

2023-07-25

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3992, title = "Iterative Circuit Repair Against Formal Specifications", author = "Cosler, Matthias and Schmitt, Frederik and Hahn, Christopher and Finkbeiner, Bernd", booktitle="{International Conference on Learning Representations (ICLR)}", year="2023", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC