Browsing by Author "Koutavas, Vasileios"

Now showing items 1-5 of 5

    • From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques 

      Koutavas, Vasileios (Springer, 2022)
      We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, novel up-to ...

    • From CCS to CSP: the m-among-n Synchronisation Approach 

      Butterfield, Andrew; Ekembe Ngondi, Gerard; Koutavas, Vasileios (Open Publishing Association, 2022)
      We present an alternative translation from CCS to an extension of CSP based on m-among-n syn chronisation (called CSPmn). This translation is correct up to strong bisimulation. Unlike the g-star renaming approach ([4]), ...

    • Fully Abstract Normal Form Bisimulation for Call-by-Value PCF 

      Koutavas, Vasileios; Lin Hou, Yu (IEEE, 2023)
      We present the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental ...

    • Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques 

      Koutavas, Vasileios; Lin, Yu-Yang (2021)
      We present a bounded equivalence verification tool called Hobbit for higher-order programs with local state—based on a subset of OCaml—that combines fully abstract symbolic environmental bisimulations, novel up-to techniques, ...

    • Translation of CCS into CSP, Correct up to Strong Bisimulation 

      Butterfield, Andrew; Ekembe Ngondi, Gerard; Koutavas, Vasileios (Springer, 2021)
      We present a translation of CCS into CSP which is correct with respect to strong bisimulation. To our knowledge this is the first such translation to enjoy a correctness property. This contributes to the unification of the ...