ABSTRACT. The B method is quite popular for developing provably correct software for safety critical railway systems, particularly for driverless trains. In recent years, the B method has also been used successfully for data validation (http://www.data-validation.fr). There, the B language has proven to be a compact way to express complex validation rules, and tools such as predicateB, Ovado or ProB can be used to provide high assurance validation engines, where a secondary toolchain validates the result of the primary toolchain.

This talk will give an overview of our experience in using logic-based formal methods in general and B in particular for industrial applications. We will also touch subjects such as training and readability and the implementation of ProB in Prolog. We will examine which features of B make it well suited for, e.g., the railway domain, but also point out some weaknesses and suggestions for future developments. We will also touch upon other formal methods such as Alloy or TLA+, as well as other constraint solving backends for B, not based on Prolog (SAT via Kodkod/Alloy and SMT via Z3 and CVC4).

ABSTRACT. Answer Set Programming (ASP) is a powerful rule-based language for knowledge representation and reasoning that has been developed in the field of logic programming and nonmonotonic reasoning. After many years of basic research, the ASP technology has become mature for the development of significant real-world applications. In particular, the well-known ASP system DLV has undergone an industrial exploitation by a spin-off company called DLVSYSTEM srl, which has led to its successful usage in a number of industry-level applications. The success of DLV for applications development is due also to its endowment with powerful development tools, supporting researchers and software developers that simplify the integration of ASP in real-world applications which usually require to combine logic-based modules within a complete system featuring user interfaces, services etc. In this talk, we first recall the basics of the ASP language. Then, we overview our advanced development tools, and we report on the recent implementation of some challenging industry-level applications of our system.

ABSTRACT. Role-Based Access Control (RBAC) is a popular security policy framework. User access to resources is controlled by roles and privileges. Constraint Handling Rules (CHR) is a rule-based constraint logic language. CHR has been used to implement security policies for trust management systems like RBAC for more than two decades. In this extended abstract, we give some references to these works.

ABSTRACT. In this position paper we first describe a classic logic programming approach to the solution of (a portion) of the challenge problem involving RBAC. We use the XSB Tabled Prolog Language and system \cite{xsbmanual-07}, with ideas from Transaction Logic \cite{trans-tcs94xs}. Then we discuss issues that involve what would be required to use such an implementation in a real-world application requiring RBAC functionality. And finally we raise issues about the possible design of a general procedural application programming interface to logic (programming) systems. In analogy to ODBC (Open Data Base Connectivity), what might an OLSC (Open Logic System Connectivity) look like?

ABSTRACT. In this paper, we answer the Role-Based Access Control (RBAC) challenge by showcasing the solution of RBAC components by using JASP, a flexible framework integrating ASP with Java. In JASP the programmer can simply embed ASP code in a Java program without caring about the interaction with the underlying ASP system. This way, it is possible solve seamlessly both tasks suitable for imperative and declarative specification as required by RBAC.

ABSTRACT. Both software engineers and business people tend to be reluctant to adopt logic-based methods. On the one hand, this may be due to unfamiliarity with ``scary'' logical syntax. To ameliorate this, we developed an API for a state-of-the-art logic system, using only standard Python syntax. On the other hand, logic-based methods might have more impact if they could be used directly by business people. The recent DMN standard that might help in this respect.

ABSTRACT. We discuss how rules and constraints might be made easier for more conventional programming. We use a language that extends DistAlgo, which extends Python, and we use the RBAC programming challenge plus distributed RBAC as examples.

ABSTRACT. A growing trend in modeling is the construction of high-level modeling languages that invoke a suite of solvers. This requires automatic reformulation of parts of the problem to suit different solvers, a process that typically introduces many auxiliary variables. We show how semantic typing can manage relationships between variables created by different parts of the problem. These relationships must be revealed to the solvers if efficient solution is to be possible. The key is to view variables as defined by predicates, and declaration of variables as analogous to querying a relational database that instantiates the predicates. The modeling language that results is self-documenting and self-checks for a number of modeling errors.

ABSTRACT. This document gives an overview of a Picat-based XCSP3 solver, named PicatSAT, submitted to the 2018 XCSP competition. The solver demonstrates the strengths of Picat, a logic-based language, in parsing, modeling, and encoding constraints into SAT.

ABSTRACT. Computational cognitive modeling tries to explore cognition through developing detailed, process-based understanding by specifying corresponding computational models.

Currently, computational cognitive modeling architectures as well as the implementations of cognitive models are typically ad-hoc constructs. They lack a formalization from the computer science point of view. This impedes analysis of the models.

In this work, we present how cognitive models can be formalized and analyzed with the help of logic programming in form of Constraint Handling Rules (CHR). We concentrate on confluence analysis of cognitive models in the popular cognitive architecture Adaptive Control of Thought -- Rational (ACT-R).

ABSTRACT. If programming was ever a hermitlike activity, those days are in the past. Like other internet-aided social processes, software engineers connect and learn online. Open-source repositories exemplify common coding patterns and best practices, videos and interactive tutorials teach foundations and pass on insight, and online forums invite and answer technical questions. These knowledge-sharing facilities make it easier for engineers to pick up new techniques, coding practices, languages, and libraries. This is good news in a world where software quality is as important as ever, where logic specification can be used to declare intent, and where formal verification tools have become practically feasible.

In this talk, I give one view of the future of software engineering, especially with an eye toward software quality. I will survey some techniques, look at the history of tools, and inspire with some examples of what can be daily routine in the lives of next-generation software engineers.

ABSTRACT. The world is dynamic, and ASP is not! This is a provocative way to say that ASP is not up to dealing with many complex real-world applications having a dynamic nature, let alone transitions over states, not even mentioning more fine-grained temporal structures.

ABSTRACT. We are developing a rule-based implementation of a tool to analyse and generate graphs. It is used in the domain of mason's marks. For thousands of years, stonemasons have been inscribing these symbolic signs on dressed stone. Geometrically, mason's marks are line drawings. They consist of a pattern of straight lines, sometimes circles and arcs. We represent mason's marks by connected planar graphs.

Our prototype tool for analysis and generation of graphs is implemented in the rule-based declarative language Constraint Handling Rules (CHR). It features

- a vertex-centric logical graph representation as constraints, - derivation of properties and statistics from graphs, - recognition of (sub)graphs and patterns in a graph, - automatic generation of graphs from given constrained subgraphs, - drawing graphs by visualization using svg graphics

In particular, we started to use the tool to classify and to invent mason's marks. In principe, our tool can be applied to any problem domain that admits a modeling as graphs. The drawing and generation module of our tool is available online at http://chr.informatik.uni-ulm.de/mason.

ABSTRACT. We propose a system design principle that explains how to use declarative programming (logic and functional) together with imperative programming. The advantages of declarative programming are well known; they include ease of analysis, verification, testing, optimization, maintenance, upgrading, and distributed implementation. We will not elaborate on these advantages here, but rather focus on what part of the software system should be written declaratively. Declarative programming cannot interface directly with the real world since it does not support common real-world concepts such as physical time, named state, and nondeterminism. Other programming paradigms that support these concepts must therefore be used, such as imperative programming (which contains named state). To optimize the system design, we propose that real-world concepts should only be used where they are needed, namely where the system interfaces with the real world. It follows that a software system should be built completely declaratively except where it interfaces with the real world. We motivate this principle with examples from our research and we give it a precise formal definition.