Peter Backeman is a Post Doc at MDH. 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 exprience 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). Currently, 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:
5G Service Orchestration
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.
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 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.
UML-based Modeling and Analysis of 5G Service Orchestration (Nov 2020) Ashalatha Kunnappilly, Peter Backeman, Cristina Seceleanu THE 27TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2020)
Towards Efficient Bit-Vector Interpolation (Oct 2018) Peter Backeman, Philipp Rümmer , Aleksandar Zeljic
Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis (Jun 2016) Peter Backeman, Christoph Wintersteiger , Bordan Yordanov , Sara-Jane Dunn
Efficient algorithms for bounded rigid E-unification Peter Backeman, Philipp Rümmer TABLEAUX 2015 (TABLEAUX)
Free variables and theories: Revisiting rigid E-unification Peter Backeman, Philipp Rümmer rontiers of Combining Systems - 10th International Symposium (FroCoS)