Sort by: Order: Results:

Now showing items 1-9 of 9

  • Bisimulations for Communicating Transactions (Extended Abstract) 

    HENNESSY, MATTHEW; KOUTAVAS, VASILEIOS; Spaccasassi, Carlo (Springer Berlin Heidelberg, 2014)
    We develop a theory of bisimulations for a simple language containing communicating transactions, obtained by dropping the isolation requirement of standard transactions. Such constructs have emerged as a useful programming ...
  • Communicating Transactions 

    DE VRIES, EDSKO; HENNESSY, MATTHEW; KOUTAVAS, VASILEIOS (Springer, 2010)
    We propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error re- covery in distributed ...
  • First-Order Reasoning for Higher-Order Concurrency. 

    HENNESSY, MATTHEW; KOUTAVAS, VASILEIOS (2012)
    We present a practical first-order theory of a higher-order pi-calculus which is both sound and complete with respect to a standard semantic equivalence. The theory is a product of combining and simplifying two of the most ...
  • From Applicative to Environmental Bisimulation 

    KOUTAVAS, VASILEIOS (Elsevier, 2011)
  • Liveness of Communicating Transactions (Extended Abstract) 

    DE VRIES, EDSKO; HENNESSY, MATTHEW; KOUTAVAS, VASILEIOS (2010)
    We study liveness and safety in the context of CCS extended with communicating transactions, a construct we recently proposed to model automatic error recovery in distributed systems. We show that fair-testing and ...
  • Reverse Hoare Logic 

    KOUTAVAS, VASILEIOS (Springer Berlin Heidelberg, 2011)
    We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or ...
  • Symbolic bisimulation for a higher-order distributed language with passivation (extended abstract) 

    KOUTAVAS, VASILEIOS; HENNESSY, MATTHEW (2013)
    We study the behavioural theory of a higher-order distributed calculus with private names and locations that can be passivated. For this language, we present a novel Labelled Transition System where higher-order inputs are ...
  • A Testing Theory for a Higher-Order Cryptographic Language 

    KOUTAVAS, VASILEIOS (Springer Berlin Heidelberg, 2011)
    We study a higher-order concurrent language with cryptographic primitives, for which we develop a sound and complete, first-order testing theory for the preservation of safety properties. Our theory is based on co-inductive ...
  • Towards Efficient Abstractions for Concurrent Consensus 

    KOUTAVAS, VASILEIOS (Springer Berlin Heidelberg, 2013)
    Consensus is an often occurring problem in concurrent and distributed programming. We present a programming language with simple semantics and build-in support for consensus in the form of communicating transactions. We ...