6 citations · 13 across the 6 of their papers we have counts for
6 papers
Verifying Device Drivers with Pancake
Junming Zhao, Miki Tanaka, Johannes Åman Pohjola +10
Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant d…
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In…
A Mechanised Semantics for HOL with Ad-hoc Overloading
Johannes Åman Pohjola, Arve Gengelbach
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. I…
Psi-Calculi Revisited: Connectivity and Compositionality
Johannes Åman Pohjola
Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calcul…
A Sorted Semantic Framework for Applied Process Calculi
Johannes Borgström, Ramūnas Gutkovas, Joachim Parrow +2
Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondetermi…
Priorities Without Priorities: Representing Preemption in Psi-Calculi
Johannes Åman Pohjola, Joachim Parrow
Psi-calculi is a parametric framework for extensions of the pi-calculus with data terms and arbitrary logics. In this framework there is no direct way to represent action prioritie…