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
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).
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.