Name: Marijn J.H. Heule
Affiliation: Carnegie Mellon University, USA
Homepage: https://www.cs.cmu.edu/~mheule/

Bio:
Marijn Heule is an Associate Professor of Computer Science at Carnegie Mellon University. His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning satisfiability (SAT) solvers. His preprocessing and proof-producing techniques are used in many state-of-the-art automated reasoning tools. Marijn won multiple best paper awards at international conferences, including at SAT, CADE, IJCAR, TACAS, HVC, LPAR, and IJCAI-JAIR. He is one of the editors of the Handbook of Satisfiability. This 1500+ page handbook (second edition) has become the reference for SAT research.

Without Loss of Satisfaction.
The success of automated reasoning presents us with an interesting peculiarity: while modern solving tools can handle gigantic real-world instances, they often fail miserably on supposedly easy problems. Their poor performance is frequently caused by using reasoning techniques that can only learn logically implied facts. In recent years, a couple of new proof systems for propositional logic have been proposed to overcome this issue by facilitating the learning of facts that are not logically implied, but preserve satisfaction. Moreover, these systems are surprisingly strong, even without the introduction of new definitions, which is the key feature of short proofs presented in the proof-complexity literature.
We demonstrate the effectiveness of reasoning "without loss of satisfaction" using three problems that are hard for automated-reasoning approaches. First, we present short proofs of mutilated chessboard problems that are completely different from proofs based on the classical argument. We can produce them automatically and they are understandable. Second, our proofs of the chromatic number of Mycielski graphs show that these proof systems can compactly express arguments that go beyond symmetry breaking. Finally, we illustrate the impact on the proof size using Ramsey number problems. Resolution proofs of Ramsey number four consist of about a billion resolution steps. In contrast, our "without loss of satisfaction" proof uses just 38 steps. None of these proofs introduce new variables.

Name: Pedro R. D'Argenio
Affiliation: National University of Córdoba, Argentina
Homepage: https://cs.famaf.unc.edu.ar/~dargenio/

Bio:
Pedro R. D'Argenio is a Full Professor in Computer Science at FAMAF, National University of Córdoba. He also holds a research post at CONICET. He studied computer science at the National University of La Plata (Argentina), and obtained his Ph.D. at the University of Twente (Netherlands) where he also did his postdoc. He has also worked at the Université de Provence (FR), and was a Visiting Professor at the University of Twente (NL) and Saarland University (DE). He is a former Director of the Doctoral Program in Computer Science and former Associate Dean of Science and Technology at FAMAF, UNC. He is currently the Chair of the IFIP WG 1.8 on Concurrency Theory. Prof. D'Argenio is a leading researcher in formal techniques for dependable systems, contributing in areas such as model checking, process semantics, fault tolerance, security, and testing. He has led and participated in numerous Argentine and European research projects.

Optimal Route Synthesis in Space DTN using Markov Decision Processes.
Delay-tolerant networks (DTN) are time-evolving networks that do not provide continuous and instantaneous end-to-end communication. Instead, the topological configuration of DTN changes continuously: connections are available only during some time intervals and thus the network may suffer from frequent partitions and high delay. In this sense, the DTN paradigm is fundamental to understand deep-space and near-Earth communications. A particular characteristic of space networks is that, due to the orbital and periodic behavior of the different agents (e.g. satellites and terrestrial or lunar stations), contact times and durations between nodes can be accurately predicted. This type of DTNs is called scheduled and expected contacts can be imprinted in a contact plan that exhaustively describes the future network connectivity. In addition, the contacts may suffer of some quantifiable failure that can be included in the contact plan. Thus, this behavior can be encoded in a Markov decision process (MDP) where the non-determinism corresponds precisely to the routing decisions. With this model at hand, we have developed and studied several offline techniques for deriving optimal and near-optimal routing solutions that ensure maximum likelihood of end-to-end message delivery. In particular, we have devised an analytical solution that exhaustively explores the MDP very much like probabilistic model checking does, and have also explored simulation-based techniques using lightweight scheduler sampling (LSS). The objective of this presentation is to report this research as well as current ongoing developments for multi-objective routing optimization on space DTN.

Name: Ana Cavalcanti
Affiliation: University of York, United Kingdom
Homepage: https://www-users.york.ac.uk/~alcc500/

Bio:
Ana Cavalcanti is a Professor at the University of York and a Royal Society - Wolfson Research Merit Award holder. In 2003, she was awarded a Royal Society Industry Fellowship to work with QinetiQ on formal methods. She has published more than 100 papers and chaired the Programme Committee of various well-established international conferences. Her main research interest is the theory and practice of formal methods. She has a long-term interest in refinement, safety-critical systems, object-orientation , concurrency, and real-time applications. She has played a major role in the design and formalization of a state-rich process algebra, namely, Circus, and its development techniques using Hoare and He’s Unifying Theories of Programming.

Learning in RoboStar.
The RoboStar framework supports a model-based approach in the development of control software for robotics applications. It provides domain-specific tool-independent notations for modelling and simulation, and techniques for automatic generation of artefacts. In this talk, we focus on the RoboStar results on verification in the presence of artificial neural networks (ANN). Existing techniques and tools for ANN verification are concerned with component-level properties. In RoboStar, we deal with properties that may depend on all software components, including traditional and ANN components. Our current focus is on trained neural networks for control, used in the context of behavioural models described using RoboChart, a domain-specific modelling language for robotics with support for formal verification. Our proof approach is based on refinement and provides deductive guarantees on behaviour. ANNs can therefore be treated as reliable, white-box components. We describe our modelling notation and a strategy for automated proof based on Isabelle and Marabou.