Category: Honors and Awards

Categories
Honors and Awards News

Best Artifact Award for security verification

The paper “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”, coauthored with Hamed Arshad, Ross Horne, Olaf Owe, and Tim Willemse, wins the Best Artifact Award at the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems

This work was part of the PhD thesis of Hamed, and the paper is coauthored by five people (from Luxembourg, Netherlands, University of Oslo, and NTNU). The paper was presented at FORTE during the confederated conferences called DisCoTec 2022 and the new tool called XACML2mCRL2 was demoed to the whole community during the plenary demos session. The tool was given the Best Artifact Award (https://www.discotec.org/2022/programme#discotec-best-artefacts) and was also invited for a special issue of the prestigious Elsevier journal Science of Computer Programming appearing in 2023.

Image showing an overview of the verification tool chain, with our tool in green.

The tool is meant to help verify correctness of access control policies, especially applicable to the health domain where our usecase is taken from (hence the playful title of the paper, “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”).

In academia one can use this tool in teaching (it is already used in the MSc course IMT4123 Systems Security at NTNU) or one can build MSc theses topics using the tool for various applications or extensions. More widely, one can use this tool in projects and help industry with their verification tasks.

Categories
Honors and Awards

Best Paper Award for Capacity Verification at FMCAD 2018

My work with Bjørnar Luteberget and Koen Claessen (from Chalmers) won the Best Paper Award at the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), which was held in Texas, USA, in November 2018.

The paper is on automatically verifying capacity specifications against railway designs, and contains an associated tool chain based on SAT solvers and Discrete Event Simulation. The paper was selected from 73 papers that were submitted to FMCAD 2018. This conference is ranked as #1 in Formal Methods on the Google Scholar Metrics.

Image showing an overview of the verification tool chain.

One main technical contribution of this paper is the introduction of the method that we called “SAT modulo DES” which combines the speed of verification of SAT solvers with the power of Discrete Event Simulation engines for handling complex problems such as train dynamics.

The talk of Bjørnar Luteberget was equally praised and made one of the highlights of the conference. Bjørnar also had a Student Paper and a lightning talk in the respective session, describing our initial work on Synthesis for railway designs.

The verification tools were tested on realistic models as below.

Categories
Honors and Awards

5th most downloaded paper in JLAMP


My work with Håkon Normann and Thomas Hildebrandt was published in Elsevier’s Journal of Logical and Algebraic Methods in Programming and became the 5th most downloaded paper of 2016.

The paper is entitled “Declarative event based models of concurrency and refinement in psi-calculi”.

Categories
Honors and Awards

Best Paper Award for Railway Verification at iFM 2016

My work with Bjørnar Luteberget and Martin Steffen (from PSY and ConSeRNS groups at UiO) won the Best Paper Award at the 12th International Conference on Integrated Formal Methods, which was held in Reykjavik, Iceland in June 2016. The paper was selected from 99 papers.

The paper is on automatically verifying railway regulations against railway designs, and contains an associated tool that was integrated in the RailComplete railway design engineering tool set.

The talk of Bjørnar Luteberget was equally praised and made one of the highlights of the conference. Other highlights included the talks of Turing laureate Tony Hoare on “Unifying Theories of Concurrency” part of UTP 2016 symposium and the talk of Danish Knight Kim G. Larsen on the amazing verification tool Uppaal part of the PrePost workshop.

A more realistic screenshot from the presented tool.

Categories
Honors and Awards

Scholarship for Marktoberdorf School 2006

Scholarship for Fully Funded Student Participant in Marktoberdorf International Summer School on Software System Reliability and Security, hosted by NATO Security Through Science Committee and Institut fur Informatik of Technische Universitat Munchen, Germany, during 1-13 August 2006.

Categories
Honors and Awards

Scholarship for ICCL School of 2005

Scholarship for Fully Funded Student Participant in ICCL Summer School on Logic-based Knowledge Representation, at the Technische Universitat Dresden, Germany 2-17 July 2005.