Security protocols are small distributed programs, aiming at securely achieving some transaction, while relying on a public network. Getting formal guarantees that such protocols satisfy their specifications is an important issue, because of the numerous applications and the economical and societal impact of possible failures. On the other hand, security protocols constitute an ideal field of applications for research in automated deduction: the protocols are small, as well as their specification, yet their verification is non-trivial. The purpose of this note is to show several interesting problems in automated deduction, that are raised by this verification problem.
We describe an abstract proof-theoretic framework based on normal-form proofs, defined using well-founded orderings on proof objects. This leads to robust notions of canonical presentation and redundancy. Fairness of deductive mechanisms - in this general framework - leads to completeness or saturation.
Software model checking has become popular with the successful use of predicate abstraction and refinement techniques to find real bugs in low-level C programs. At the same time, verification approaches based on abstract interpretation and symbolic execution are also making headway in real practice. Much of the recent progress is fueled by advancements in automatic decision procedures and constraint solvers, which lie at the computational heart of these approaches. In this talk, I will describe our experience with several of these verification approaches, highlighting the roles played by automatic decision procedures and their interplay with the applications. Specifically, I will focus on SAT- and SMT-based model checking, combined with abstract domain analysis based on polyhedra representations. I will also describe some challenges from software verification that can motivate interesting research problems in this area.
Traditionally, description logic (DL) research has concentrated on reasoning about the conceptual modeling of a domain, as provided e.g. by an ontology. This kind of reasoning is not sufficient when DLs are used in applications that emphasize instance data, such as information integration and ontology-mediated data access. In the last couple of years, this shortcoming has stimulated lively research on (instance) query answering in DLs. The talk gives an overview of the area and presents and summarizes recent results for query answering in expressive and lightweight DLs.