# Andrius Velykis

I am a research associate in Taming Concurrency project at Newcastle University, working with Prof. Cliff Jones. I do like my mathematics and computer science: my (research) interests range from software development to formal methods, theorem proving and reasoning about concurrency in software.

## Reasoning about concurrency using Rely/Guarantee

Currently I am working on improving reasoning about concurrency in software. The Taming Concurrency project tries to unpick the popular approaches to concurrency reasoning, namely the Rely/Guarantee thinking and Separation Logic to get to the underlying issues, ideas and strengths in order to improve the overall approach to reasoning.

## AI4FM and PhD research

I have completed my PhD thesis “Capturing Proof Process” as part of the AI4FM project, under supervision of Prof. Cliff Jones.

In my research I am interested in understanding and learning from interactive proof. Proof assistants, such as Isabelle, can be used to produce mathematically verified proofs about a formal specification of a system. The process, however, can be laborious and require a lot of manual interaction. My PhD research investigates how we can extract high-level proof ideas from an interactive proof—these ideas could then be reused to complete similar proofs automatically.

Currently I am developing a generic *ProofProcess* framework that realises ideas on capturing and inferring the proof process. It closely integrates with proof assistants: prototype implementations are available for Isabelle (via new Isabelle/Eclipse Prover IDE) and Z/EVES (via new CZT-Z/EVES integration in Community Z Tools).

A bit more details are available on the dedicated page for my research. One could also follow my publications—new outputs may appear there before this page gets updated…

## Towards a PhD in formal methods

In hindsight, a PhD in formal methods looks like a natural continuation of my previous studies. After completing high-school education at Kaunas University of Technology Gymnasium with strong mathematical direction, I gained my BSc in Applied Mathematics at Kaunas University of Technology in Lithuania. To complement mathematics with knowledge that is more directly applicable, I continued my studies with MSc Software Engineering at the University of York, UK, where I was awarded the degree with distinction. Here I got introduced to formal methods and wrote my master’s thesis on formal verification of separation kernel components using Z notation and Z/EVES theorem prover. After that I wanted to look deeper… this lead me to the PhD.

## Coding, coding, and more coding…

I like thinking of coding (software development) as my trade. I have quite a “tools-first” approach to solving problems and like hacking away at tools and solutions for myself and everyone.

I have worked professionally as software developer/analyst, creating software for data management or data analysis. I am most proficient with Java and Eclipse platform, though recently I have got to truly like Scala programming language. I used to know my way about creating websites as well, which still comes in handy running this one. I think having experience in creating software commercially gives a useful perspective in academia—I am planning to put that to good use. Quite a bit more details on my work experience and skills are available on my LinkedIn profile.

## There’s more scattered across the interwebs

Bits about myself can be found in various websites logging my interests and activities. Some of them are conveniently listed in the right sidebar.

~Andrius