Showing 1–5 of 5 results for author: Furbach, F

Verification under TSO with an infinite Data Domain

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Shashwat Garg

Abstract: We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the sta… ▽ More We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable). In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete. △ Less

Submitted 18 January, 2024; originally announced January 2024.

Parameterized Verification under TSO with Data Types

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Adwait Godbole, Yacoub G. Hendi, Shankaranarayanan Krishna, Stephan Spengler

Abstract: We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obta… ▽ More We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obtain tight complexity bounds for TSO-based parameterized verification over several abstract data types, such as push-down automata, ordered multi push-down automata, one-counter nets, one-counter automata, and Petri nets. We apply the framework to get complexity bounds for higher order stack and counter variants as well. △ Less

Submitted 12 February, 2023; v1 submitted 4 February, 2023; originally announced February 2023.

Petri Net Invariant Synthesis

Authors: Peter Chini, Florian Furbach

Abstract: We study the synthesis of inductive half spaces (IHS). These are linear inequalities that form inductive invariants for Petri nets, capable of disproving reachability or coverability. IHS generalize classic notions of invariants like traps or siphons. Their synthesis is desirable for disproving reachability or coverability where traditional invariants may fail. We formulate a CEGAR-loop for the… ▽ More We study the synthesis of inductive half spaces (IHS). These are linear inequalities that form inductive invariants for Petri nets, capable of disproving reachability or coverability. IHS generalize classic notions of invariants like traps or siphons. Their synthesis is desirable for disproving reachability or coverability where traditional invariants may fail. We formulate a CEGAR-loop for the synthesis of IHS. The first step is to establish a structure theory of IHS. We analyze the space of IHS with methods from discrete mathematics and derive a linear constraint system closely over-approximating the space. To discard false positives, we provide an algorithm that decides whether a given half space is indeed inductive, a problem that we prove to be coNP-complete. We implemented the CEGAR-loop in the tool INEQUALIZER and our experiments show that it is competitive against state-of-the-art techniques. △ Less

Submitted 7 May, 2021; originally announced May 2021.

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models

Authors: Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer

Abstract: We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, Porthos finds a bug in the form of an unexpected execution - an execution that is consistent with the target bu… ▽ More We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, Porthos finds a bug in the form of an unexpected execution - an execution that is consistent with the target but inconsistent with the source memory model. Technically, Porthos implements a bounded model checking method that reduces the portability analysis problem to satisfiability modulo theories (SMT). There are two main problems in the reduction that we present novel and efficient solutions for. First, the formulation of the portability problem contains a quantifier alternation (consistent + inconsistent). We introduce a formula that encodes both in a single existential query. Second, the supported memory models (e.g., Power) contain recursive definitions. We compute the required least fixed point semantics for recursion (a problem that was left open in [47]) efficiently in SMT. Finally we present the first experimental analysis of portability from TSO to Power. △ Less

Submitted 28 April, 2017; v1 submitted 22 February, 2017; originally announced February 2017.

Relating Strong Spatial Cognition to Symbolic Problem Solving --- An Example

Authors: Ulrich Furbach, Florian Furbach, Christian Freksa

Abstract: In this note, we discuss and analyse a shortest path finding approach using strong spatial cognition. It is compared with a symbolic graph-based algorithm and it is shown that both approaches are similar with respect to structure and complexity. Nevertheless, the strong spatial cognition solution is easy to understand and even pops up immediately when one has to solve the problem. In this note, we discuss and analyse a shortest path finding approach using strong spatial cognition. It is compared with a symbolic graph-based algorithm and it is shown that both approaches are similar with respect to structure and complexity. Nevertheless, the strong spatial cognition solution is easy to understand and even pops up immediately when one has to solve the problem. △ Less

Submitted 14 June, 2016; originally announced June 2016.