LPAR-22 will feature the following invited talks:
Holger Hermanns, Saarland University, Germany
TITLE: Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
ABSTRACT:
Emission cleaning in modern cars is controlled by embedded software. In this context, the diesel emissions scandal has made it apparent that the automotive industry is susceptible to fraudulent behaviour, implemented and effectuated by that control software. Mass effects make the individual controllers altogether have statistically significant adverse effects on people's health. This talk surveys recent work on the use of rigorous formal techniques to attack this problem. It starts off with an introduction into the dimension and facets of the problem from a software technology perspective. It then details approaches to use (i) model checking for the white-box analysis of the embedded software, (ii) model-based black-box testing to detect fraudulent behaviour under standardized conditions, and (iii) synthesis of runtime monitors for real driving emissions of cars in-the-wild. All these efforts aim at finding ways to eventually ban the problem of doped software, that is, of software that surreptitiously alters its behaviour in certain circumstances - against the interest of the owner or of society.
Ben Goertzel, SingularityNET
TITLE: Commonsense Reasoning for Robotics and Bioscience via Probabilistic Logic and Meta-learning
ABSTRACT: TBA
Orna Kupferman, Hebrew University, Israel
TITLE: Variations on the Classical Maximum-Flow Problem
ABSTRACT:
The fundamental maximum-flow problem gets as input a flow network with a source vertex and a target vertex, and searches for a maximal flow from the source to the target. We consider several extensions to the problem, corresponding to rich settings in which the problem is applied. The extensions are well studied in the context of formal verification and the algorithmic problem of model checking, but are new to classical graph-theory problems, and in particular to the maximum-flow problem. The extensions we study include (1) labeled networks, where the edges of the network are labeled by letters from some alphabet, and flow is restricted to travel only along paths that satisfy a given specification, (2) network games, where the vertices of the network are partitioned among selfish players, each directing flow that arrives to vertices she owns, aiming to maximize the flow that reaches her target, and (3) hierarchical networks, which are succinctly represented, and where the goal is to find a maximum flow by reasoning about the succinct representation.
Based on joint work with Rachel Faran, Shibashis Guha, Tami Tamir, Gal Vardi, and Moshe Y. Vardi