Bit-vector interpolation and quantifier elimination by lazy reduction P Backeman, P Rummer, A Zeljic 2018 Formal Methods in Computer Aided Design (FMCAD), 1-10, 2018 | 22 | 2018 |

Exploring Approximations for Floating-Point Arithmetic Using *UppSAT*A Zeljić, P Backeman, CM Wintersteiger, P Rümmer International Joint Conference on Automated Reasoning, 246-262, 2018 | 15 | 2018 |

Theorem Proving with Bounded Rigid *E*-UnificationP Backeman, P Rümmer Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 12 | 2015 |

Efficient Algorithms for Bounded Rigid *E*-unificationP Backeman, P Rümmer Automated Reasoning with Analytic Tableaux and Related Methods: 24th …, 2015 | 9 | 2015 |

From UML modeling to UPPAAL model checking of 5G dynamic service orchestration A Kunnappilly, P Backeman, C Seceleanu 7th Conference on the Engineering of Computer Based Systems, 1-10, 2021 | 8 | 2021 |

Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic P Backeman, P Rümmer, A Zeljić Formal methods in system design 57 (2), 121-156, 2021 | 3 | 2021 |

UML-based Modeling and Analysis of 5G Service Orchestration A Kunnappilly, P Backeman, C Seceleanu 2020 27th Asia-Pacific Software Engineering Conference (APSEC), 129-138, 2020 | 3 | 2020 |

5G Service Orchestration Supported by Model Checking-A Case Study of Health Applications A Kunnappilly, P Backeman, C Seceleanu, M Johanson Mälardalens högskola, 2021 | 1 | 2021 |

Free Variables and Theories: Revisiting Rigid *E*-unificationP Backeman, P Rümmer Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015 …, 2015 | 1 | 2015 |

Propagating the nvector constraint: Haplotype inference using constraint programming P Backeman | 1 | 2013 |

Supporting 5G service orchestration with formal verification P Backeman, A Kunnappilly, C Seceleanu Computer Science and Information Systems, 59-59, 2022 | | 2022 |

Quantifiers and Theories: A Lazy Approach P Backeman Acta Universitatis Upsaliensis, 2019 | | 2019 |

Towards Efficient Bit-Vector Interpolation P Backeman, P Rümmer, A Zeljic Workshop on Programming Theory, 19, 2018 | | 2018 |

New techniques for handling quantifiers in Boolean and first-order logic P Backeman Uppsala University, 2016 | | 2016 |

Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis. P Backeman, CM Wintersteiger, B Yordanov, SJ Dunn SMT@ IJCAR, 41-50, 2016 | | 2016 |

Demonstrating the Effects of Power Management on a Real-Time Operating System P Backeman, E Gustafsson | | 2010 |

The Next 104 UppSAT Approximations A Zeljic, P Backeman, CM Wintersteiger, P Rümmer | | |