Keynote Speakers

BIO: Christoph Benzmüller is affiliated as Privatdozent for Computer Science and Mathematics with Freie Universität Berlin and Saarland University, Saarbrücken. At present, he is visiting University of Luxemburg. Previous research stations of Christoph include Stanford University, USA (visiting scholar), Articulate Software, USA (senior researcher), Intl. University of Germany, Bruchsal (full professor), University of Cambridge, UK (senior researcher), Saarland University (associate professor), University of Birmingham, UK and the University of Edinburgh, UK (postdoc). Christoph received his PhD (1999) and his Habilitation (2007) in computer science from Saarland University. His PhD was partly conducted at Carnegie Mellon University, USA. In 2012, Christoph had been awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG). Christoph is an expert in higher-order automated and interactive theorem proving, which he utilises as a basis for an approach towards universal logic reasoning. His broader interests concern all aspects of knowledge representation and reasoning. Moreover, Christoph is well known for his interdisciplinary applications. Most recently, for example, he has pioneered, together with colleagues, the area of computational metaphysics. Christoph is trustee and vice-president of CADE (Conference on Automated Deduction), board member of AAR (Association of Automated Reasoning) and spokesman of the section Deduction Systems of the Gesellschaft für Informatik. He serves in various further functions (chair, editorial board, steering committee, trustee, etc.) for various conferences and organisations. Prior to his academia career, Christoph Benzmüller was a successful long-distance runner at German national level.

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning

The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis, that is, a most universal formal language in which all knowledge about the world and the sciences can be encoded. A quick study of the survey literature on logical formalisms suggests that quite the opposite to Leibniz’ dream has become todays reality. Instead of a characteristica universalis, we are today facing a very rich and heterogenous zoo of different logical systems. Instead of converging towards a single superior logic, this logic zoo is further expanding, eventually even at accelerated pace. As a consequence, the unified vision of Leibniz seems further remote from todays reality than ever before.

However, there are also some promising initiatives to counteract these diverging developments. Attempts at unifying approaches to logic e.g. include categorial logic, algebraic logic and coalgebraic logic. In my presentation at SBFM I will argue for another alternative: the shallow semantical embeddings approach. This approach has a very pragmatic motivation, foremost reuse of tools, simplicity and elegance. It utilises classical higher-order logic (HOL) as a unifying meta-logic in which the syntax and semantics of various other logics can be explicitly modelled. Off-the-shelf higher-order interactive and automated theorem provers can then be employed to reason about and within the shallowly embedded logics.

In my presentation I will survey very recent experiments (conducted with/by colleagues and students) in which this approach has been successfully utilised:

• Mathematics: “First-order free logic” has been embedded in HOL and subsequently utilised to explore axiom systems for category theory; as part of study a flaw in a well known category theory textbook has been revealed.
• Metaphysics: Variants of “intensional, functional higher-order modal logics” have been embedded in HOL and subsequently employed to encode and verify the most essential parts of Fitting’s prominent textbook “Types, Tableaus, and Gödel’s God”
• Metaphysics: A “hyper-intensional, relational higher-order modal logic” has been embedded in HOL and subsequently employed to encode Ed Zalta’s proposal of a “Principia-logico Metaphysica”; as part of this study a deeply rooted paradox has been revealed.

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 150 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 formalisation of a state-rich process algebra, namely, Circus, and its development techniques using the Hoare and He’s Unifying Theories of Programming. She is currently Chair of the Formal Methods Europe association.

Safe simulation for robotics

There are many challenging aspects involved in ensuring safety of mobile and autonomous robots. Perhaps surprisingly, the engineering of their software needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. The modern outlook of the applications is not matched by the outdated practices on validation and verification. In this seminar, we present a model-based approach for early validation and sound generation of simulations. In robotics, simulation is the favoured technique for analysis in this domain. Our approach is based on RoboChart, a domain-specific modelling notation with a formal semantics, and on analysis based on model checking and theorem proving to complement simulation. RoboChart is a UML-like notation that includes timed and probabilistic primitives for modelling of controllers. We link it to RoboSim, another graphical notation defined as a gateway between RoboChart models and customised simulations developed for traditional robotics simulators.

BIO: Dimitra Giannakopoulou is a Research Computer Scientist with the NASA Ames Research Center. She leads the Models and Algorithms for Reliable Software (MARS) Group within the Robust Software Engineering Area. Her work is concerned with the development of scalable verification and validation techniques for safety critical systems. She holds a PhD in Distributed Computing from Imperial College, University of London. She has authored over 60 peer-reviewed publications and has delivered several keynote talks at international conferences.

To Autonomy and Beyond: New Challenges for Verification and Validation

Autonomy brings the complexity of systems to new dimensions, and as such, it needs breakthroughs in assurance technologies and certification processes. This talk will review some of our recent work on the verification and validation (V&V) of the next generation airborne collision avoidance system (ACAS X). ACAS X uses probabilistic models of aircraft encounters in a safety-critical context, and as such, poses novel challenges for V&V. Based on our experience with ACAS X, we will discuss challenges that are inherent in V&V of autonomy, and potential approaches to addressing them.

BIO: Patrícia D. L. Machado is a Professor in the Computing and Systems Department at Federal University of Campina Grande (UFCG), Brazil, since 1995. She received her PhD Degree in Computer Science from the University of Edinburgh, UK, in 2001, Master Degree in Computer Science from the Federal University of Pernambuco, Brazil, in 1994 and Bachelor Degree in Computer Science from the Federal University of Paraiba, Brazil, in 1992. Her research interests include software testing, formal methods, mobile computing, component based software development and model-driven development. Since 1998, she has produced a number of contributions in the area of software testing, including research projects, publications, tools, supervising, national/international cooperation and teaching. She has investigated and applied model-based testing techniques in industry, particularly in cooperation with Motorola and Ingenico.

Automatic Test Selection: Progress and Challenges

Test automation is a promising approach to make testing a more feasible, reproducible and reliable activity. Testing is a key part of system development processes, including the ones based on formal methods. By the use of different strategies such as search-based algorithms, constraint solving and meta-heuristics, automatic test selection may provide a way of systematically exercising system functionalities. To make test automation possible, formal methods play an important role, particularly for functional testing where formal specification/models are required as a basis. Steady progress has been made in the last 40 years on model-based approaches to testing. Application has reached industry, particularly in the last 10 years. Yet a number of challenges still need to be faced, particularly regarding adoption in industry as well as limitations on current test generation and selection algorithms. For instance, studies show that manually written test suites may have stronger defect detection capability.

BIO: Leila Ribeiro is a full professor at the Federal University of Rio Grande do Sul (UFRGS). She recieved her doctoral degree from the Technische Universitat Berlin (1996). She holds a scholarship as Productive Researcher from CNPq (the Brazilian National Research Agency), besides being an IFIP member (Working Group 1.3 -- Foundations of System Specification). Her main research interests are on formal methods, working mainly with the following topics: specification and formal semantics, bioinformatics, formal verification and models of computation. Currently, she is the coordinator of the Special Commission on Formal Methods (CEMF) of the Brazilian Computer Society (SBC).

Commemorative pannel for the 20th year of the SBMF

Professor Leila, involved with the organisation of the first Workshop on Formal Methods (WMF), which later became the Brazilian Symposium on Formal Methods (SBMF), will take part in a commemorative pannel to discuss the past, the present and the future of the research and application of formal methods in Brazil.

• ghpc@cin.ufpe.br
• Av. Jornalista Aníbal Fernandes, s/n
  50.740-560, Recife-PE, Brazil