|
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.
|
|