I am a computer scientist interested in programming language theory and concurrent system research. Here you can find published work, talks, and software that I authored.

I am currently unaffiliated, but previously I was a research fellow at NOVA LINCS, working with Luís Caires and the Software Systems group.

I earned a computer science doctorate degree from Uppsala University for my work on concurrent system verification. There, I was advised by Johannes Borgström and Björn Victor.

Email me at ramunasg@gmail.com.

Publications

My publication list can also be found on this dblp page.

• A Sorted Semantic Framework for Applied Process Calculi

  J. Borgström, R. Gutkovas, J. Parrow, B. Victor and J. Å. Pohjola
  Logical Methods in Computer Science 12(1), 2016
  doi pdf

• Modal Logics for Nominal Transition Systems

  J. Parrow, J. Borgström, L.-H. Eriksson, R. Gutkovas, and T. Weber
  26th International Conference on Concurrency Theory (CONCUR 2015), 2015
  doi pdf html

• The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi

  J. Borgström, R. Gutkovas, I. Rodhe, and B. Victor
  ACM Transaction on Embedded Computing, ACSD Special Issue, Journal, 2015
  doi pdf

• Session types for broadcasting

  D. Kouzapas, R. Gutkovas, and S. J. Gay
  Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES), Workshop, 2014
  doi pdf

• A sorted semantic framework for applied process calculi (extended abstract)

  J. Borgström, R. Gutkovas, J. Parrow, B. Victor, and J. Å. Pohjola
  Trustworthy Global Computing (TGC), Symposium, 2014
  doi pdf

• A parametric tool for applied process calculi

  J. Borgström, R. Gutkovas, I. Rodhe, and B. Victor
  Application of Concurrency to System Design (ACSD), Conference, 2013
  doi

Licentiate Thesis

• Advancing Concurrent System Verification: Type based approach and tools

  R. Gutkovas
  Licentiate, Uppsala University, Department of Information Technology, 2014
  pdf

PhD Thesis: Languages, Logics, Types and Tools for Concurrent System Modelling

• Full text.
• The official Uppsala University archived version (DiVA) with only the introduction (Kappa).

I defended my Ph.D. thesis on Sep 9, 2016. The opponent was associate professor Thomas T. Hildebrandt of IT University of Copenhagen. The grading comitee was comprised of Prof. Nobuko Yoshida, Prof. Jan Frisco Groote, and Assoc. Prof. Tobias Wrigstad.

Abstract

A concurrent system is a computer system with components that run in parallel and interact with each other. Such systems are ubiquitous and are notably responsible for supporting the infrastructure for transport, commerce and entertainment. They are very difficult to design and implement correctly: many different modeling languages and verification techniques have been devised to reason about them and verifying their correctness. However, existing languages and techniques can only express a limited range of systems and properties.

In this dissertation, we address some of the shortcomings of established models and theories in four ways: by introducing a general modal logic, extending a modelling language with types and a more general operation, providing an automated tool support, and adapting an established behavioural type theory to specify and verify systems with unreliable communication.

A modal logic for transition systems is a way of specifying properties of concurrent system abstractly. We have developed a modal logic for nominal transition systems. Such systems are common and include the pi-calculus and psi-calculi. The logic is adequate for many process calculi with regard to their behavioural equivalence even for those that no logic has been considered, for example, CCS, the pi-calculus, psi-calculi, the spi-calculus, and the fusion calculus.

The psi-calculi framework is a parametric process calculi framework that subsumes many existing process calculi. We extend psi-calculi with a type system, called sorts, and a more general notion of pattern matching in an input process. This gives additional expressive power allowing us to capture directly even more process calculi than was previously possible. We have reestablished the main results of psi-calculi to show that the extensions are consistent.

We have developed a tool that is based on the psi-calculi, called the psi-calculi workbench. It provides automation for executing the psi-calculi processes and generating a witness for a behavioural equivalence between processes. The tool can be used both as a library and as an interactive application.

Lastly, we developed a process calculus for unreliable broadcast systems and equipped it with a binary session type system. The process calculus captures the operations of scatter and gather in wireless sensor and ad-hoc networks. The type system enjoys the usual property of subject reduction, meaning that well-typed processes reduce to well-typed processes. To cope with unreliability, we also introduce a notion of process recovery that does not involve communication. This is the first session type system for a model with unreliable communication.

Talks/Slides

• 

  Languages, Logics, Types and Tools for Concurrent System Modelling

  NOVA LINCS Seminar

  2016-12-14
• 

  Advancing Concurrent System Verification

  Licentiate Seminar, Uppsala University

  2014-10-20
• 

  A Parametric Tool for Applied Process Calculi

  Psi-Calculi Workbench

  ProFuN Project Seminar, Uppsala

  2014
• 

  Process Calculi for WSNs and more

  ProFuN Project Workshop, Uppsala

  2014
• 

  A Parametric Tool for Applied Process Calculi

  Psi-Calculi Workbench

  ACSD13, Barcelona, Spain

  2013
• 

  Presentation of DPLL(T)

  The SMT Reading Group, Uppsala

  2012-10-31
• 

  Psi-Calculi Workbench

  YR-CONCUR, New Castle, UK

  2012

Software

I keep my software projects on GitHub.

Psi-Calculi Workbench (source code) is a tool for concurrent system verification (e.g., internet protocols, security protocols, cache coherence algorithms, etc.) based on the Psi-calculi framework. Produces symbolic execution traces, can be interfaced with external constraint solvers (e.g., SMTs).