Peter Backeman, Associated Senior Lecturer

E-mail:
peter.backeman@mdu.se
Room:
U1-191
Division:
Division of Networked and Embedded Systems
Research group:
Formal Modelling and Analysis of Embedded Systems


Peter Backeman is an associated senior lecturer at MDU. He obtained his PhD from Uppsala University in Computer Science in 2019. His research interests in mainly focused on formal methods, including automated therorem proving (ATP), satisfiability modulo theories (SMT), and it's application in various areas.

Peter also likes to teach and has teaching experience of different levels, ranging from being co-responsible for a real-time embedded programming course to teaching freshmen in introduction to programming and also teaching elementary school and high school teachers programming.

Peter's research is focused on automatic reasoning and verification. His PhD thesis dealt with both Satisfiability Modulo Theories (SMT) as well as Automated Theorem Proving (ATP). He is part of the Formal Modeling and Analysis of Embedded Systems research group, working with applications of automated reasoning in the context of verification, as well as testing, of embedded systems. He is a member of the Health5G (http://health5g.eu/) and XIVT (https://www.xivt.org/) projects.

Past and current projects:

ACISC, PerFlex, ESCAPE


As a part of a larger project (see Projects tab) we are constructing a theoretical framework for verification of 5G service orchestration systems, as well as a protoype tool-chain. The goal is to provide an engineer with support for automatically verifying certain properties of 5G systems, specified in UML, by translating the problem to networks of timed automata and use UPPAAL as a backend for model checking.

Bit-Vector Interpolation


We developed a novel interpolation procedure for formulas containing bit-vectors. The method works by abstracting all bit-vector operations as integer operations (thus ignoring bit-specific interactions). Then lazily, parts of the formula is refined to work over bit-vectors instead resulting in a faster processing of many formulas. This is integrated into the Princess theorem prover: http://www.philipp.ruemmer.org/princess.shtml.

UppSAT

UPPSAT is an abstract SMT-solver framework, which wraps around a backend SMT-solver (e.g., MathSAT), reads a specification (written in Scala), and generates a "new" SMT-solver which uses an iterative approximation framework to quickly find models to complicated formulas. It shows strong results especially in the floating-point domain. More information (as well as source code, etc) at github: https://github.com/uuverifiers/uppsat.

 

Bounded Rigid E-Unification

Unification is a core subprocedure in many automated theroem provers. Unfortunately, the special case of simultaneous rigid E-unification (which is important in many tableaux-based procedures) is undecidable. Therefore we formulated a new variant: Bounded Rigid E-Unification (BREU), which, if used correctly, can be applied to form a sound and complete theorem proving procedure. It was integrated as a part of the Princess theorem prover and showed promising results when looking at first-order logic with equality. More information (and executable) is located at: http://user.it.uu.se/~petba168/#eprincess.

 

Program Committees

 

Reviewer

  • NFM2020    
  • iFM 2019
  • SMT 2019    
  • CADE-27    
  • FMCAD 2014    
  • NFM-2017    
  • PAAR-2016    
  • IJCAR 2016    
  • VMCAI 2016    
  • ATVA 2015    
  • CAV 2015    
  • TACAS 2015    
  • LCTES-2014
PhD students supervised as assistant supervisor:

Ashalatha Kunnappilly (former)