1 citations · 1 across the 3 of their papers we have counts for
5 papers
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos
We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations simi…
Symbolic Execution Game Semantics
Yu-Yang Lin, Nikos Tzevelekos
We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular w…
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos +1
This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and…
Higher-Order Bounded Model Checking
Yu-Yang Lin, Nikos Tzevelekos
We present a Bounded Model Checking technique for higher-order programs. The vehicle of our study is a higher-order calculus with general references. Our technique is a symbolic st…
Trace Properties from Separation Logic Specifications
Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber +2
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Se…