Source author record

Tiark Rompf

Tiark Rompf appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Programming Languages cs.CY Distributed, Parallel, and Cluster Computing eess.SY Formal Languages and Automata Theory Machine Learning Systems and Control

Catalog footprint

What is connected

4works

7topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

OCTAL: Graph Representation Learning for LTL Model Checking

Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical for large scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a Büchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.

preprint2019arXiv

Resilient Cyberphysical Systems and their Application Drivers: A Technology Roadmap

Cyberphysical systems (CPS) are ubiquitous in our personal and professional lives, and they promise to dramatically improve micro-communities (e.g., urban farms, hospitals), macro-communities (e.g., cities and metropolises), urban structures (e.g., smart homes and cars), and living structures (e.g., human bodies, synthetic genomes). The question that we address in this article pertains to designing these CPS systems to be resilient-from-the-ground-up, and through progressive learning, resilient-by-reaction. An optimally designed system is resilient to both unique attacks and recurrent attacks, the latter with a lower overhead. Overall, the notion of resilience can be thought of in the light of three main sources of lack of resilience, as follows: exogenous factors, such as natural variations and attack scenarios; mismatch between engineered designs and exogenous factors ranging from DDoS (distributed denial-of-service) attacks or other cybersecurity nightmares, so called "black swan" events, disabling critical services of the municipal electrical grids and other connected infrastructures, data breaches, and network failures; and the fragility of engineered designs themselves encompassing bugs, human-computer interactions (HCI), and the overall complexity of real-world systems. In the paper, our focus is on design and deployment innovations that are broadly applicable across a range of CPS application areas.

preprint2016arXiv

From F to DOT: Type Soundness Proofs with Definitional Interpreters

Scala's type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Scala and similar languages. Unfortunately, it is not clear how DOT relates to any well-known type systems, and type soundness has only been established for very restricted subsets. In fact, important Scala features are known to break at least one key metatheoretic property such as environment narrowing or subtyping transitivity, which are usually required for a type soundness proof. First, and, perhaps surprisingly, we show how rich DOT calculi can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisen's syntactic approach, is based on term rewriting, which does not a priori make a distinction between runtime and type assignment time. Second, we demonstrate how type soundness can be proved for advanced, polymorphic, type systems with respect to high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof in this style for System F<: and several extensions, including mutable references. Our proofs use only simple induction: another surprising result, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require co-inductive proof techniques. Third, we show how DOT-like calculi emerge as generalizations of F<:, exposing a rich design space of calculi with path-dependent types which we collectively call System D. Armed with insights from the definitional interpreter semantics, we also show how equivalent small-step semantics and soundness proofs in Wright-Felleisen-style can be derived for these systems.

preprint2011arXiv

Building-Blocks for Performance Oriented DSLs

Domain-specific languages raise the level of abstraction in software development. While it is evident that programmers can more easily reason about very high-level programs, the same holds for compilers only if the compiler has an accurate model of the application domain and the underlying target platform. Since mapping high-level, general-purpose languages to modern, heterogeneous hardware is becoming increasingly difficult, DSLs are an attractive way to capitalize on improved hardware performance, precisely by making the compiler reason on a higher level. Implementing efficient DSL compilers is a daunting task however, and support for building performance-oriented DSLs is urgently needed. To this end, we present the Delite Framework, an extensible toolkit that drastically simplifies building embedded DSLs and compiling DSL programs for execution on heterogeneous hardware. We discuss several building blocks in some detail and present experimental results for the OptiML machine-learning DSL implemented on top of Delite.