5 citations · 9 across the 7 of their papers we have counts for
9 papers
Quantitative Monitoring of Signal First-Order Logic
Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç +1
Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real…
Flavors of Quantifiers in Hyperlogics
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple trace…
Monitoring Hyperproperties over Observed and Constructed Traces
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
Hyperproperties specify system requirements that relate multiple executions. Reasoning about such properties naturally involves executions that play different roles: some correspon…
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize…
QuAK: Quantitative Automata Kit
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and execut…
Monitoring Hyperproperties With Prefix Transducers
Marek Chalupa, Thomas A. Henzinger
Hyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in Hyper…
Fast Computation of Strong Control Dependencies
Marek Chalupa, David Klaška, Jan Strejček +1
We introduce new algorithms for computing non-termination sensitive control dependence (NTSCD) and decisive order dependence (DOD). These relations on control flow graph vertices h…
SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode
Martina Vitovská, Marek Chalupa, Jan Strejček
The paper describes a member of the Symbiotic toolbox called sbt-instrumentation, which is a tool for configurable instrumentation of LLVM bitcode. The tool enables a user to speci…
Data-centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis +2
We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating…