129 citations · 153 across the 17 of their papers we have counts for
4 papers · 1 filter
Runtime Monitoring of Supermartingale Certificates
Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner +2
Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However, these guarantees rely on a mathematical m…
Value Functions as Supermartingale Certificates
Alessandro Abate, Daniel Contro, Mirco Giacobbe +2
Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of -reg…
Complete -Regular Supermartingale Certificates
Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko +1
We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneo…
Zero-Knowledge Model Checking
Pascal Berrang, Mirco Giacobbe, Jacob Swales +1
We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method co…