Peter Backeman, Associated Senior Lecturer

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

• ECBS2023
• TAP23
• ECBS 2021 (https://ecbs-conference.org/)
• Tacas 2020 (Artifact Evaluation Committee)

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

[Show all publications]

[Google Scholar author page]

Safety Argumentation for Machinery Assembly Control Software (Sep 2024)
Julieth Patricia Castellanos Ardila, Sasikumar Punnekkat, Hans Hansson, Peter Backeman
43rd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2024)

Modeling and Verification of ROS Systems Using Stochastic Timed Automata (Jun 2024)
Peter Backeman, Cristina Seceleanu
MRTC Report, Mälardalen Real-Time Research Centre (MRTC 2024)

Synthesizing Understandable Strategies (Nov 2023)
Peter Backeman
8th International Conference on Engineering of Computer-based Systems (ECBS2023)

Supporting 5G Service Orchestration with Formal Verification (Mar 2023)
Peter Backeman, Ashalatha Kunnappilly, Cristina Seceleanu
Computer Science and Information Systems (ComSIS,10(1))

5G Service Orchestration Supported by Model Checking - A Case Study of Health Applications (Sep 2021)
Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu, Mathias Johanson
MRTC Report, Mälardalen Real-Time Research Centre (MRTC 2021)

From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration (May 2021)
Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu
7th international Conference on the Engineering of Computer Based Systems (ECBS 2021)

Ashalatha Kunnappilly (former)