44 citations · 55 across the 3 of their papers we have counts for
3 papers
cs.PL2020★ 7 cited
Decidability and Synthesis of Abstract Inductive Invariants
Francesco Ranzato
Decidability and synthesis of inductive invariants ranging in a given domain play an important role in many software and hardware verification systems. We consider here inductive i…
cs.LO2006★ 4 cited
On Completeness of Logical Relations for Monadic Types
Slawomir Lasota, David Nowak, Yu Zhang
Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In particular, programs can be mode…
cs.LO2005★ 44 cited
Logical Relations for Monadic Types
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak
Logical relations and their generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propos…