Invited Speakers

Logic and Practice of Programming (LPOP)

John Hooker Carnegie Mellon University

Constraint programming, mathematical programming, optimization methods, ...

Rustan Leino Amazon Web Services

Program verification, specification, programming languages, automated verification tools, ...

Nicola Leone University of Calabria

Answer set programming, knowledge representation, database theory, ...

Michael Leuschel University of Düsseldorf

Model checking, partial evaluation, SMT solvers, program verification, ...

Abstracts

Title: A Modeling Language Based on Semantic Typing (Joint work with André Ciré and Tallys Yunes)

Speaker: John Hooker

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.

Title: The Young Software Engineer’s Guide to Using Formal Methods

Speaker: Rustan Leino

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.

Title: On the Development of Industrial Applications with ASP (Joint work with Bernardo Cuteri, Marco Manna, Francesco Ricca)

Speaker: Nicola Leone

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.

Title: Practical uses of Logic, Formal Methods, B and ProB

Speaker: Michael Leuschel

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).