University of Luxembourg, FSTC, LU
Freie Universität Berlin, Dep. of Maths and CS
Saarland University, Dep. CS, DE
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.
University of York, UK
Department of Computer Science
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.
Federal University of Campina Grande, BR
Computing and Systems Department
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.
Federal University of Rio Grande do Sul, BR
Institute of Informatics
BIO: Daltro Nunes is an invited full professor at the Federal University of Rio Grande do Sul (UFRGS). Hi received his Der Naturwissenschaften - Informatik (1985) from the Universität Stuttgart. In 2010, he was awarded by the Special Comission of Software Engineering (SBC -- Brazilian Computer Society) for his contribution on the creation and consolidation of the software engineering field in Brazil. In the following year (2011), he received the Newton Faller prize (SBC). He has a solid experience in Computer Science, with emphasis on program logics and semantics, working on the following topics: software engineering, software development processes, and formal methods.
Commemorative pannel for the 20th year of the SBMF
Professor Daltro, the general chair 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.