41 citations · 48 across the 2 of their papers we have counts for
3 papers
cs.CR2009★ 7 cited
On formal verification of arithmetic-based cryptographic primitives
David Nowak
Cryptographic primitives are fundamental for information security: they are used as basic components for cryptographic protocols or public-key cryptosystems. In many cases, their s…
cs.LO2006★ 41 cited
On the freeze quantifier in Constraint LTL: decidability and complexity
Stéphane Demri, Ranko Lazic, David Nowak
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze q…
cs.LO2005
Reasoning about transfinite sequences
Stéphane Demri, David Nowak
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequenc…