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