|8:55 – 9:00||
Welcome Note, Dieter Hutter (DFKI)
|9:00 – 9:30||
Deductive Synthesis of Plans using Linear Logic in Isabelle, Lucas Dixon (University of Edinburgh)
|9:30 – 10:00||
Reasoning about Incompletely Defined Programs, Christoph Walther (TU Darmstadt)
|10:00 – 10:30||
Proof Critics in IsaPlanner, Moa Johansson (University of Edinburgh)
|10:30 – 11:00||Coffee Break|
|11:00 – 11:30||
Inference Rules and their Application in the New Prover, Dominik Dietrich (Saarland University)
|11:30 – 12:00||
Discovering Inductive Theorems in MATHsAiD, Roy McCasland (University of Edinburgh)
|12:00 – 12:15||
Future Work in Edinburgh, Serge Autexier (Saarland University)
|12:30 – 14:00||Lunch|
|14:00 – 14:30||
Adding Higher-Order Functions to VeriFun, Markus Aderhold (TU Darmstadt)
|14:30 – 15:00||
Ordinals, Chad Brown (Saarland University)
|15:00 – 15:30||
Polymorphic Specifications in VeriFun, Andreas Schlosser (TU Darmstadt)
|15:30 – 16:00||Coffee Break|
|16:00 – 16:30||
A Hiproof-Based User Interface, Alan Bundy (University of Edinburgh)
|16:30 – 17:00||
Mediating between Scientific Text Editors and Proof Assistance Systems, Marc Wagner (Saarland University)
|17:00 – 17:30||
Towards the Mechanization of Granularity Judgments for Mathematics, Marvin Schiller (Saarland University)
|19:00 – 19:30||
|8:30 – 9:00||
Formal Analysis of PIN Block Attacks, Graham Steel (University of Edinburgh)
|9:00 – 9:30||
Patching Faulty Security Protocols (joined work with Raul Monroy and Juan Carlos Lopez) ), Dieter Hutter (DFKI)
|9:30 – 10:00||
Dynamic Refinement and the OpenKnowledge Project, Fiona McNeill (University of Edinburgh)
|10:00 – 10:30||Coffee Break|
|10:30 – 11:00||
Description Logics for Shape Analysis, Lilia Georgieva (University of Edinburgh)
|11:00 – 11:30||
Agent oriented theorem proving in Isabelle , Priya Gopalan (University of Edinburgh)
|11:30 – 12:00||
A parallel interpreter for linear logic programs, Alan Smaill (University of Edinburgh)
|12:00 – 13:00||Lunch|
Markus AderholdAdding Higher-Order Functions to VeriFun Abstract: Higher-order functions are frequently used in elegant implementations of everyday algorithms such as Quicksort, for example. Therefore a theorem prover designed for program verification should be able to deal with such higher-order implementations so that the program to be verified does not need to be transformed into a first-order representation beforehand. This raises the question of how much higher-order functionality a theorem prover needs to have so that we can use it to verify the correctness of higher-order algorithms. The idea is to spare the user from having to specify particular induction schemes or proof tactics but to allow him to focus on the properties of the algorithm at hand. Our work is based on VeriFun, a semi-automated inductive theorem prover. We describe the extension of the type system and the restricted addition of higher-order features. The purpose of these changes is to facilitate the verification of higher-order algorithms without arriving at a fully-fledged higher-order theorem prover so as to maintain a high degree of automation. The talk will also include examples showing some issues in the context of mutually recursive data structures.
short talk about his intented stay in Edinburgh (tentative)
OrdinalsAbstract: Set-theoretic ordinals are objects which are inherently untyped. I will discuss a formalization of the ordinals in a version of (untyped) set theory. The set theory is represented within a dependent type theory. The representation of proofs and objects in the type theory allows one to interactively work with partial proofs and in the end obtain complete, formally checkable proofs. I will use the ordinals as an example to demonstrate how one can work with an untyped universe of mathematical objects within the meta-theory of a dependent type theory.
A Hiproof-Based User InterfaceAbstract: We propose a graphical user interface to a proof development system based on hiproofs. This would enable the genuinely top-down development of proofs. By this I mean not the development of the proof from the conjecture backwards, using the lowest level of logical reasoning. Rather, I mean the sketching of the outline of the proof, with detail gradually being added to taste. There is some indication that working mathematicians might find this a congenial way to develop proofs.
Inference Rules and their Application in the New Prover (tentative)tbd.
Deductive Synthesis of Plans using Linear Logic in IsabelleAbstract: We will describe how we are using a formalisation of intuitionistic linear logic in Isabelle, based on Abramsky's presentation (1993), with a framework for middle out reasoning for the derivation of grid services that meet a given specification.
Description Logics for Shape Analysis (joint work with P.Maier)Abstract: Verification of programs requires reasoning about sets of program states. In the case of programs that manipulate pointers, program states are pointer graphs. Verification of such programs involves reasoning about unbounded sets of graphs. We study well-known description logics as a framework for symbolic shape analysis. We propose a predicate abstraction based shape analysis, parametrized by description logics to represent the abstraction predicates. Depending on the particular logic chosen sharing, reachability and separation in pointer data structures are expressible. In addition, we investigate the relationship to other logics for symbolic shape analysis.
Agent oriented theorem proving in IsabelleTitle: Abstract: I will be talking about the perspectives of Agent-oriented theorem-proving that am looking into, for my PhD. I will outline the first phase of my project, which is the design of an agent-oriented-framework on Isabelle, using the existing Isabelle/Isar tactics as building blocks. My talk will also touch upon two other past projects and the opportunities provided by them for the application of an agent-based-paradigm. These two involve: deductive synthesis and middle-out-reasoning. I will be grateful for feedback on the ideas as it is work still at an early stage.
Patching Faulty Security Protocols (joined work with Raul Monroy and Juan Carlos Lopez Pimentel)
Proof Critics in IsaPlannerAbstract: Discovering unknown lemmas, generalisations and other eureka steps is a major challenge for automated theorem proving. Proof-planning critics can help automate these steps by making use of information from failed proof attempts. I will talk about plans to extend existing critics for use in higher-order logic in the IsaPlanner system, as well as development of new critics.
Discovering Inductive Theorems in MATHsAiDAbstract: MATHsAiD is a system designed to discover mathematical theorems, given only the axioms and definitions of a mathematical theory as input. In particular, MATHsAiD has had some success at discovering inductive theorems. I'll explain the methods used by the system to generate these theorems, and give a brief demo.
Fiona McNeillDynamic Refinement and the OpenKnowledge Project OpenKnowledge is an EU project aimed at attempting to provide a framework to enable a Semantic Web like system to become open, in the sense that anyone can join and the cost of individual participation is very low. This is not generally the case in sematic based systems because the cost of being precise about semantics and ensuring an individual, absolute semantics for a component is very high. The OK project proposes to resolve this problem by focussing on semantics related to interaction, acquired at low cost during participation, and thus avoiding dependency on a priori semantic agreement. One important aspect of this work is aligning different representations (ontologies, protocols, service descriptions, etc.) that are wholly or partially mismatched.
Towards the Mechanization of Granularity Judgments for MathematicsAbstract: We discuss an important subproblem for the automatization of proof tutoring with the help of deduction techniques. Human tutors in mathematics are observed to reject correct proof steps by their student if the step size of the student's argumentation does not match the tutor's expectations, i.e. the steps are considered to be too coarse or too fine-grained. We present a recent empirical study in the DIALOG project on tutorial dialog for teaching mathematical proof. Furthermore, we present our approach to the mechanization of judgments about the grain size of mathematical proof steps. The data from the empirical study is taken as a basis for a first evaluation of our method.
Polymorphic Specifications in VeriFunAbstract: Most up-to-date programming languages allow modularization of code to organize increasing amounts of lines of code. Modules provide interfaces for the communication with external code. The behavior of a module is mostly described by additional textual comments. Programmers implementing the same interface in another module know in which way the methods should behave and hopefully stick to the given comments. This method is not admissible for program verification. The behavior of methods declared by an interface needs to be present in a formal representation which can be utilized during the course of verification of some properties about the given interface. An interface used for program verification has to specify the operators and additionally some axioms which constrain the operators to a specific behavior. The tuple of the domain on which the operators are defined, the operators, and the axioms is a specification. This talk describes the semantics of specifications, the integration into the theorem prover VeriFun, and some problems arising when dealing with specifications.
A parallel interpreter for linear logic programsSeveral people have suggested that linear logic can be used as a specification language for planning problems. Abramsky, as amended by others, gave a computational interpretation to the language that associates programs with proofs in the logic. I describe an interpreter for such programs that makes use of several features of the programming language Alice, in particular lazy and parallel execution.
Formal Analysis of PIN Block AttacksAbstract: PIN blocks are 64-bit strings that encode a PIN ready for encryption and secure transmission in banking networks. PIN block attacks exploit feedback from error messages during PIN block manipulation operations, to allow an attacker to guess a PIN in far fewer operations than would be required by a brute-force attack. This talk will describe a framework for formal analysis of such attacks. Our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
Mediating between Scientific Text Editors and Proof Assistance SystemsAbstract: Mathematical proof assistance systems have not yet achieved considerable recognition and relevance in mathematical practise. Significant progress is still required, in particular with respect to the user-friendliness of these systems. Rather than developing a new user interface we present a generic tool to integrate proof assistance systems into scientific text editors by using a semantic annotation language which is parameterized over specific languages for formulas, definitions and menus. The annotations allow to capture the logical structures defining theories and proofs contained in a document while following closely its textual structure. The tool supports the writing of mathematical documents in interaction with a proof assistant system by maintaining consistent representations on either side, dealing with all management aspects arising from changes and providing contextual menus.
Reasoning about Incompletely Defined ProgramsAbstract: We consider automated reasoning about recursive partial functions with decidable domain, i.e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e.g. when attempting to divide by zero. We investigate the semantics of incompletely defined programs, define an interpreter for those programs and discuss the termination of incompletely defined procedures. We then analyze which problems need to be solved if a theorem prover designed for verification of completely defined programs is modified to work for incompletely defined programs as well. We also discuss how to reason about stuck computations which arise when calling incompletely defined procedures with invalid arguments. Our method of automated reasoning about incompletely defined programs has been implemented in the verification tool VeriFun. We conclude by discussing experiences obtained in several case studies with this implementation and also compare and relate our proposal to other work. (Joint work with Stephan Schweitzer)