Joshua Schneider


Last Name

Schneider

First Name

Joshua

ORCID

0000-0001-8253-4513

Organisational unit

Filters

2015 - 201982020 - 202313
Reset filters

Search Results

Publications 1 - 10 of 21
  • A Formally Verified Monitor for Metric First-Order Temporal Logic
    Item type: Conference Paper
    Schneider, Joshua; Basin, David; Krstić, Srđan; et al. (2019)
    Lecture Notes in Computer Science ~ Runtime Verification
  • Scalable Online First-Order Monitoring
    Item type: Conference Paper
    Schneider, Joshua; Basin, David; Brix, Frederik; et al. (2018)
    Lecture Notes in Computer Science ~ Runtime Verification: 18th International Conference, RV 2018 Limassol, Cyprus, November 10–13, 2018: Proceedings
  • Bounded Natural Functors with Covariance and Contravariance
    Item type: Journal Article
    Lochbihler, Andreas; Schneider, Joshua (2018)
    Archive of Formal Proofs
  • Applicative Lifting
    Item type: Journal Article
    Lochbihler, Andreas; Schneider, Joshua (2015)
    Archive of Formal Proofs
  • Correct and Efficient Policy Monitoring, a Retrospective
    Item type: Conference Paper
    Basin, David; Krstić, Srđan; Schneider, Joshua; et al. (2023)
    Lecture Notes in Computer Science ~ Automated Technology for Verification and Analysis
    The MonPoly project started over a decade ago to build effective tools for monitoring trace properties, including functional correctness, security, and compliance policies. The original MonPoly tool supported monitoring specifications given in metric first-order temporal logic, an expressive specification language. It handled both the online case, where system events are monitored as they occur, and the offline case, monitoring logs. Our tool has evolved over time into a family of tools and supporting infrastructure to make monitoring both scalable and suitable for high assurance applications. We survey this evolution which includes: (1) developing more expressive monitors, e.g., adding aggregation operators, regular expressions, and limited forms of recursion; (2) delimiting efficiently monitorable fragments and designing new monitoring algorithms for them; (3) supporting parallel and distributed monitoring; (4) using theorem proving to verify monitoring algorithms and explore extensions; and (5) carrying out ambitious case studies.
  • Verified First-Order Monitoring with Recursive Rules
    Item type: Conference Paper
    Zingg, Sheila; Krstić, Srđan; Raszyk, Martin; et al. (2022)
    Lecture Notes in Computer Science ~ Tools and Algorithms for the Construction and Analysis of Systems
    First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.
  • Monad normalisation
    Item type: Journal Article
    Schneider, Joshua; Eberl, Manuel; Lochbihler, Andreas (2017)
    Archive of Formal Proofs
  • Relational Parametricity and Quotient Preservation for Modular (Co)datatypes
    Item type: Conference Paper
    Lochbihler, Andreas; Schneider, Joshua (2018)
    Lecture Notes in Computer Science ~ Interactive Theorem Proving: 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018, Proceedings
  • Randomized First-Order Monitoring with Hashing
    Item type: Conference Paper
    Schneider, Joshua (2022)
    Lecture Notes in Computer Science ~ Runtime Verification
    Online monitors for first-order specifications may need to store many domain values in their state, requiring significant memory. We propose an approach that compresses the monitor’s state using randomized hash functions. Unlike input sampling, our approach does not require the knowledge of distributions over traces to achieve low error probability. We develop algorithms that insert hash functions into temporal–relational algebra specifications and compute upper bounds on the resulting error probability. We employ a special hashing scheme that allows us to merge values across attributes, which further reduces memory usage. We evaluated our implementation and achieved memory reductions up to 33% when monitoring traces with large domain values, with error probability less than two in a million.
  • Adaptive Online First-Order Monitoring
    Item type: Conference Paper
    Schneider, Joshua; Basin, David; Brix, Frederik; et al. (2019)
    Lecture Notes in Computer Science ~ Automated Technology for Verification and Analysis
Publications 1 - 10 of 21