ABSTRACT. Stateflow is a widely used modeling framework for embedded and cyber-physical systems where control software interact with physical processes. This is a highly complex language with no formal semantics. In this work, we present a fully automated safety verification technique for Stateflow models. Our approach is two-folded: (i) we faithfully com- pile Stateflow models into hierarchical state machines, and (ii) we use automated logic-based verification engine to decide the validity of safety properties. The starting point of our approach is a denotational semantics of Stateflow. We propose the compilation process using continuation- passing style (CPS) denotational semantics. Our compilation technique preserves the structural and modal behavior of the system, making the safety analysis of such models more tractable. The overall approach is implemented as an open source toolbox that can be integrated into the existing Mathworks Simulink/Stateflow modeling framework. We present preliminary experimental evaluations that illustrate the effectiveness of our approach in the safety verification of industrial scale Stateflow models.

ABSTRACT. In this tool paper we describe a variation of Nintendo's "Super Mario World", dubbed "Super Formula World", that creates its game maps based on an input quantified Boolean formula. Thus in "Super Formula World", Mario, the plumber not only saves his girlfriend princess Peach, but also acts as a QBF solver as a side. The game is implemented in Java and platform independent.

Our implementation rests on abstract frameworks by Aloupis et al. that allow the analysis of the computational complexity of a variety of famous video games. In particular it is a straightforward consequence of these results to provide a reduction from QSAT to "Super Mario World". By specifying this reduction in a precise way we obtain the core engine of "Super Formula World". Similarly "Super Formula World" implements a reduction from SAT to "Super Mario Bros.", yielding significantly simpler game worlds.

ABSTRACT. Context-free language reachability (CFL-R) is a fundamental solving vehicle for computing essential compiler optimisations and static program analyses. Unfortunately, solvers for CFL-R encounter both inherently expensive problem formulations and frequent alterations to the underlying formalism. As such, tool designers are forced to create custom-tailored implementations with long development times and limited reusability. A better framework is crucial to facilitate research and development in CFL-R.

In this work we present Cauliflower, a CFL-R solver generator, that creates parallel executable C++ code from an input CFL-R rule-based specification. With Cauliflower, developers create working tools rapidly, avoiding lengthy and error-prone manual implementations. Cauliflower's domain-specific language provides semantic extension including reversal, branching, disconnection and templating. In practical experiments, Cauliflower achieves an average speedup of 1.8x compared with the best general purpose tools, and matches the performance of application-specific tools on many benchmarks.

ABSTRACT. We present new results on a constraint satisfaction problem arising from the inference of resource types in automatic amortized analysis for object-oriented programs by Rodriguez and Hofmann. These constraints are essentially linear inequalities between infinite lists of nonnegative rational numbers which are added and compared pointwise. We study the question of satisfiability of a system of such constraints in two variants with significantly different complexity. We show that in its general form (which is the original formulation presented by Hofmann and Rodriguez at LPAR 2012) this satisfiability problem is hard for the famous Skolem-Mahler-Lech problem whose decidability status is still open but which is at least NP-hard. We then identify a subcase of the problem that still covers all instances arising from type inference in the aforementioned amortized analysis and show decidability of satisfiability in polynomial time by a reduction to linear programming. We further give a classification of the growth rates of satisfiable systems in this format and are now able to draw conclusions about resource bounds for programs that involve lists and also arbitrary data structures if we make the additional restriction that their resource annotations are generated by an infinite list (rather than an infinite tree as in the most general case). Decidability of the tree case which was also part of the original formulation by Hofmann and Rodriguez still remains an open problem.

ABSTRACT. In this paper, we introduce RACCOON, a reasoner based on the connection calculus ALC theta-CM for the description logic (DL) ALC. We describe briefly the calculus, while RACCOON’s internal data structures and functioning are presented in detail. Currently, RACCOON carries out consistency checks, and could be run online; its code is also publicly available. Besides the calculus and the system description, promising results of a comparison between the new system and other ALC reasoners are shown and discussed.

ABSTRACT. Inclusion dependencies are one of the most important database constraints. In isolation their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. In contrast, finite and unrestricted implication problems for the combined class of functional and inclusion dependencies deviate from one another and are each undecidable. The same holds true for the class of embedded multivalued dependencies. An important embedded tractable fragment of embedded multivalued dependencies are independence atoms. These stipulate independence between two attribute sets in the sense that for every two tuples there is a third tuple that agrees with the first tuple on the first attribute set and with the second tuple on the second attribute set. For independence atoms, their finite and unrestricted implication problems coincide, are finitely axiomatizable, and decidable in cubic time. In this article, we study the implication problems of the combined class of independence atoms and inclusion dependencies. We show that their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. Hence, significant expressivity is gained without sacrificing any of the desirable properties that inclusion dependencies have in isolation. Finally, we establish an efficient condition that is sufficient for independence atoms and inclusion dependencies not to interact. The condition ensures that we can apply known algorithms for deciding implication of the individual classes of independence atoms and inclusion dependencies, respectively, to decide implication for an input that combines both individual classes.

ABSTRACT. Solving complex problems can involve non-trivial combinations of distinct knowledge bases and problem solvers. The Algebra of Modular Systems is a knowledge representation framework that provides a method for formally specifying such systems in purely semantic terms. Many practical systems based on expressive formalisms solve the model expansion task. In this paper, we construct a solver for the model expansion task for a complex modular systems from an expression in the algebra and black-box propagators or solvers for the primitive modules. To this end, we define a general notion of propagators equipped with an explanation mechanism, an extension of the algebra to propagators, and a lazy conflict-driven learning algorithm. The result is a framework for seamlessly combining solving technology from different domains to produce a solver for a combined system.

ABSTRACT. Ontologies are notoriously hard to define, express and reason about. Many tools have been developed to ease the debugging and the reasoning process with ontologies, however they often lack accessibility and formalisation. We developed a visual representation language, concept diagrams, that enables expressing and reasoning about ontologies in an accessible way. Indeed, concept diagrams have been shown through empirical studies to be cognitively more accessible to users in ontology debugging tasks such as (in)coherence checking. In this paper we answer the question of “ How can concept diagrams be used to reason about (in)consistencies and (in)coherence of ontologies?”. We do so by proposing a set of inference rules for concept diagrams that enables stepwise verification of the (in)consistency and/or (in)coherence of a set of ontology axioms. The design of inference rules is based on empirical evidence that concise (merged) diagrams are easier to comprehend for users than a set of lower level diagrams that offer a one-to-one translation of ontology axioms into concept diagrams. We prove that our proposed inference rules are sound and exemplify how they can be used to reason about (in)consistencies and (in)coherence in ontologies. Finally, we indicate how the set of rules introduced can serve as a foundation of additional rules for other reasoning tasks in ontologies such as query-answering.

ABSTRACT. We present fully formalized proofs of some central theorems from combinatorics. These are Dilworth's decomposition theorem, Mirsky's theorem, Hall's Marriage theorem and the Erdős-Szekeres theorem. Dilworth's decomposition theorem is the key result among these. It states that in any finite partially ordered set (poset), the size of a smallest chain cover and a largest antichain are the same. Mirsky's theorem is a dual of Dilworth's decomposition theorem, which states that in any finite poset, the size of a smallest antichain cover and a largest chain are the same. We use Dilworth's theorem in the proofs of Hall's Marriage theorem and the Erdős-Szekeres theorem. The combinatorial objects involved in these theorems are sets, posets and sequences. We develop a library of definitions and facts on finite posets that can be used as a framework for formalizing other related theorems. All the proofs are formalized in the Coq proof assistant.

ABSTRACT. Crowdsourcing promises to quasi-automate tasks that cannot be automated otherwise. Success stories like natural language translation or recognition of cats in images show that carefully crafted crowdsourcing tasks solve large problem instances which could not be solved otherwise. To utilize crowdsourcing, one has to define the problem in a way that is easy to split into small tasks, that the tasks are easy to solve for humans and hard to solve for a machine, and that the machine can efficiently check if the solution is correct.

In this paper we discuss a novel approach of using crowdsourcing to assist software verification. We argue that Horn clauses form a good base for crowdsourcing since they are easy to subdivide, and that logic abduction is a suitable task since it is hard to automatically find abductive inferences for Horn clauses, but it is easy to check if an inference makes a Horn clause valid. We describe a prototype implementation, we show how crowdsourcing integrates in the verification process, and present some preliminary results.