66 citations · 67 across the 3 of their papers we have counts for
3 papers · 1 filter
Bounded Model Checking for Hyperproperties
Tzu-Han Hsu, Cesar Sanchez, Borzoo Bonakdarpour
Hyperproperties are properties of systems that relate multiple computation traces, including security and concurrency properties. This paper introduces a bounded model checking (BM…
Verifying Hyperliveness
Norine Coenen, Bernd Finkbeiner, César Sánchez +1
HyperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can exp…
Declarative Stream Runtime Verification (hLola)
Martin Ceresa, Felipe Gorostiaga, Cesar Sanchez
Stream Runtime Verification is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing to…