|
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, C. H., Florian Lonsing, Makai Mann, Raghuram Ramanujan, and Clark Barrett
arXiv preprint, 2023.
arXiv
We present Self-Driven Strategy Learning (sdsl), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems.
|
|
Generating Temporal Logical Formulas with Transformer GANs
Jens U. Kreber and C. H.
Neurosymbolic Generative Models (NeSy-GeMs @ ICLR), 2023.
Workshop website.
We consider the scarcity of training data for temporal logics. We summarize a recently performed study on the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging formulas in the prototypical temporal logic LTL.
|
|
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Matthias Cosler, C. H., Daniel Mendoza, Frederik Schmitt, and Caroline Trippel
arXiv preprint, 2023.
arXiv
We present nl2spec, a framework for applying Large Language Models to derive formal specifications from unstructured natural language.
|
|
Iterative Circuit Repair Against Formal Specifications
Matthias Cosler, Frederik Schmitt, C. H., and Bernd Finkbeiner
Eleventh International Conference on Learning Representations (ICLR), 2023.
openreview
We present a deep learning approach for repairing sequential circuits against formal specifications.
|
|
Formal Specifications from Natural Language
C. H., Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner
arXiv Preprint, 2022.
arXiv
We study the ability of language models to translate natural language into formal specifications with complex semantics. In particular, we fine-tune off-the-shelf language models on three datasets consisting of structured English sentences and their corresponding formal representation.
|
|
Temporal Causality in Reactive Systems
Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, C. H., Niklas Metzger, and Julian Siber
20th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2022.
arXiv
We propose an approach to check causality that is tailored to reactive systems, i.e., systems that interact with their environment over a possibly infinite duration.
|
|
Explaining Hyperproperty Violations
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, C. H., Tom Horak, Niklas Metzger, and Julian Siber
34th International Conference on Computer-Aided Verifciation (CAV), 2022.
arXiv
We present an explanation method for counter examples to hyperproperties described in the specification logic HyperLTL.
|
|
Attention Flows for General Transformers
Niklas Metzger, C. H., Julian Siber, Frederik Schmitt, and Bernd Finkbeiner
arXiv Preprint, 2022
arXiv
We study the computation of how much an input token in a Transformer model influences its prediction.
|
|
Visual Analysis of Hyperproperties for Understanding Model Checking Results
Tom Horak, Norine Coenen, Niklas Metzger, C.H., Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt
IEEE Transactions on Visualization and Computer Graphics (VIS), 2022.
arXiv /
online tool /
project page
We introduce HyperVIS, which is a online tool that provides interactive visualizations
of a given system model, specification, and counterexample to a hyperproperty.
|
|
Generating Symbolic Reasoning Problems with Transformer GANs
Jens U. Kreber and C.H.
arXiv Preprint, 2021.
arXiv
We study the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging training data for symbolic reasoning domains.
|
|
Neural Circuit Synthesis from Specification Patterns
Frederik Schmitt, C.H., Markus N. Rabe, and Bernd Finkbeiner
35th Conference on Neural Information Processing Systems (NeurIPS), 2021.
arXiv /
GitHub
We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic.
|
|
Deep Learning for Temporal Logics
Frederik Schmitt, C.H., Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner
6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021.
We report on
current advances in applying deep learning to temporal logical reasoning tasks, showing
that models can even solve instances where competitive classical algorithms timed out.
|
|
Runtime Enforcement of Hyperproperties
Norine Coenen, Bernd Finkbeiner, C.H., Jana Hofmann, and Yannick Schillo
The 19th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2021
arXiv /
talk (start at 31:00) /
GitHub
We study enforcement algorithms for specifications given as formulas in universally quantified HyperLTL.
|
|
Teaching Temporal Logics to Neural Networks
C.H., Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner
Ninth International Conference on Learning Representations (ICLR), 2021.
arXiv /
talk /
poster /
GitHub
We study two fundamental questions in neuro-symbolic computing: can deep
learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics.
|
|
The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
Norine Coenen, Bernd Finkbeiner, C.H., and Jana Hofmann
17th International Conference on Principles of Knowledge Representation and Reasoning (KR), Recently published research track, 2020.
talk (by Jana Hofmann)
We discuss the hierarchy of hyperlogics from a knowledge reasoning perspective
|
|
Realizing ω-regular Hyperproperties
Bernd Finkbeiner, C.H., Jana Hofmann, and Leander Tentrup
32nd International Conference on Computer-Aided Verification (CAV), 2020.
arXiv
We study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies ω-regular hyperproperties.
|
|
Efficient monitoring of hyperproperties using prefix trees
Bernd Finkbeiner, C.H., Marvin Stenger, Leander Tentrup
International Journal on Software Tools for Technology Transfer (STTT), 2020.
Special Issue of TACAS 2018 /
arXiv
We present the monitoring approach implemented in the latest version of RVHyper, a runtime verification tool for hyperproperties.
|
|
Synthesis from Hyperproperties (extended journal version)
Bernd Finkbeiner, C.H., Philip Lukert, Marvin Stenger, and Leander Tentrup
Acta Informatica, 2019
Special Issue on SYNT 2018
We study the reactive synthesis problem for hyperproperties.
|
|
Algorithms for Monitoring Hyperproperties (tutorial)
C. H.
3rd Wold Congress on Formal Methods: 19th International Conference on Runtime Verification (RV), 2019.
tutorial slides
In this tutorial, we summarize recent algorithmic advances in monitoring hyperproperties from logical specifications.
We classify current approaches into two classes: combinatorial approaches and constraint-based approaches.
|
|
Monitoring Hyperproperties (extended journal version)
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
Formal Methods in System Design (FMSD)
Special Issue on Runtime Verification 2017
We investigate the runtime verification problem of HyperLTL
formulas for three different input models: The parallel, the bounded sequential and the unbounded sequential model.
|
|
The Hierarchy of Hyperlogics
Norine Coenen, Bernd Finkbeiner, C.H., and Jana Hofmann
34th Annual ACM/IEE Symposium on Logic in Computer Science (LICS), 2019.
arXiv
We study the expressive power across the spectrum of linear-time and branching-time hyperlogics.
Within the hierarchy of hyperlogics, we identify new boundaries on the decidability of the satisfiability problem.
|
|
Constraint-based Monitoring of Hyperproperties
C. H., Marvin Stenger, and Leander Tentrup
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019.
arXiv /
poster
We monitor hyperproperties by rewriting a
formula in the temporal logic HyperLTL to a Boolean constraint
system.
|
|
MGHyper: Checking Satisfiability of HyperLTL formulas beyond the Exists*-Forall* Fragment
Bernd Finkbeiner, C. H., and Tobias Hans
International Symposium on Automated Technology for Verification and Analysis (ATVA), 2018.
arXiv
We introduce MGHyper, a tool for automatic satisfiability checking and model generation for hyperproperties beyond the decidable Exists*-Forall* fragment of HyperLTL.
|
|
Synthesizing Reactive Systems from Hyperproperties
Bernd Finkbeiner, C. H., Philip Lukert, Marvin Stenger, and Leander Tentrup
30th International Conference on Computer Aided Verification (CAV), 2018.
arXiv /
tool page /
GitHub
We study the reactive synthesis problem for hyperproperties.
|
|
Model Checking Quantitative Hyperproperties
Bernd Finkbeiner, C. H., and Hazem Torfah
30th International Conference on Computer Aided Verification (CAV), 2018.
arXiv
We study model checking of quantitative hyperproperties.
|
|
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
17th International Conference on Runtime Verification (RV), 2017.
arXiv /
tool page /
GitHub /
poster
We present RVHyper, a runtime verification tool for hyperproperties.
|
|
Monitoring Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
17th International Conference on Runtime Verification (RV), 2017.
arXiv /
slides
We investigate the runtime verification problem of HyperLTL
formulas for three different input models: The parallel, the bounded sequential and the unbounded sequential model.
|
|
EAHyper: Satisfiability, Implication and Equivalence Checking of Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger
29th International Conference on Computer-Aided Verification (CAV), 2017.
tool page /
GitHub /
slides
We introduce EAHyper, the first satisfiability solver for hyperproperties expressed in the decidable fragment of HyperLTL.
|
|
Deciding Hyperproperties
Bernd Finkbeiner, C. H.
27th International Conference on Concurrency Theory (CONCUR), 2016.
arXiv /
slides
We study the satisfiability problem of HyperLTL.
|
|