LECTURE ABSTRACTS |
|
Jean-Raymond Abrial, The course is made of two parts. In the first one, a formalism (derived from the B Method.) is presented. It is used to construct generic mathematical models of discrete transition systems. In such a model you can express a number of static as well as dynamic properties, which must eventually be formally proved. The model can also be instantiated, refined and decomposed, again under the control of some formal proofs. In the second part, a number of applications of this approach will be presented. They cover the developments of sequential programs, distributed programs, electronic circuits, and complete systems (in particular their safety analysis). The usage of some tools will be demonstrated to the attendees. About the speaker: Jean-Raymond Abrial is the developer of the Z notation www.afm.sbu.ac.uk/z and the B method www.afm.sbu.ac.uk/b Ralph Back and Joakim von Wright,
We provide a foundation for refinement calculus where programs and systems are described as contracts, carried out by interacting agents. A contract can be analyzed from the point of view of any participating agent or coalition of agents, to see what kind of goals the agent can achieve by following the contract. We describe the mathematical and logical foundations of the calculus and show how it is used in program development. We also describe the proof format used within the calculus (structured derivations). In a series of applications of the refinement calculus, we then describe
About the speakers: www.abo.fi/~backrj and www.abo.fi/~jwright Eric C. R. Hehner, I present a first-order theory of programming that includes sequential and parallel programming, terminating and nonterminating computations, time and space complexity, boundary and interaction variables, and probabilistic programming. Recommended reading: Eric C.R. Hehner: a Practical Theory of Programming. Springer, New York, 1993, 244 pages. About the speaker: www.cs.toronto.edu/DCS/People/Faculty/hehner.html Patrick Cousot, The objective of this course is to establish a hierarchy of nondeterministic semantics of specification and programming languages by successive abstractions/refinements (or concretizations) as defined in the theory of abstract interpretation. The hierarchy encompasses a wide range of semantics from operational maximal finite, infinite (or transfinite) trace semantics to operational small-step, relational or big-step, Scott-Strachey's denotational, Dijkstra's predicate transformer, Hoare's axiomatic semantics and Floyd's proof methods. Each level in the hierarchy includes a Plotkin's natural semantics which is abstracted into a Hoare's angelic semantics to deal with partial correctness, a Smyth's demoniac semantics to deal with total correctness properties, a termination semantics, a non-termination semantics, etc. All semantics can be presented in various equivalent forms, including a fixpoint form and a rule-based form thanks to the introduction of computational partial orders generalizing Scott/Egli-Milner/Smyth orderings. The various semantics in the hierarchy are related to each other by abstract interpretation. In particular each semantics in the hierarchy is uniquely determined by a Galois connection specifying in which sense the semantics can be understood as an approximation of the most precise, trace-based one, at the root of the hierarchy. The resulting hierarchy provides a complete and uniform account of the structure and the relative precision of most well-known semantics of specification and programming languages, and many other, less known ones, such as safety semantics. About the speaker: www.di.ens.fr/~cousot K. Rustan M. Leino, An approach to finding errors in software is to formalize the correctness criteria of a given program as a logical formula. Counterexamples to the validity of the formula then correspond to errors in the program. This approach requires a semantics of the programming language, and uses some form of specifications for describing the correctness criteria. These lectures give the semantics of an object-oriented language with subtypes and dynamically-dispatched methods, and consider several issues in the specification of object-oriented programs. The lectures also include a demo of an automatic program checker based on this approach, and go through some issues in designing such a checker. About the speaker: http://research.microsoft.com/~leino/ Carroll Morgan, What is the weakest precondition that guarantees the program "flip a fair coin" will terminate in the final state "heads up"? The answer --- 1/2 --- comes from the generalised probabalistic predicate transformers that act on real-valued expressions rather than Boolean-valued predicates, giving a program logic of expected values. Applications range from the formal development of probabilistic programs, to a new style of quantitative temporal logic. A project is currently underway to extend Abrial's B method to use the probabilistic logic; and the lattice of probabilistic transformers extends the Boolean-based lattice explored by Back and von Wright. For preliminary reading see the tutorial "pGCL", and other material. About the speaker: www.cse.unsw.edu.au/school/people/info/carrollm.html Tobias Nipkow, Based on the equation
I introduce programming and proving with the proof assistant Isabelle/HOL in the following steps:
The lectures will follow the LNCS 2283 Tutorial on Isabelle/HOL but will also introduce Isabelle's recent structured proof language due to Markus Wenzel. You are encouraged to get some hands-on experience using Isabelle/HOL during the course. Tobias Nipkow will be happy to help you in coming to grips with Isabelle/HOL and will provide simple exercises. If possible, bring your own laptop with Isabelle/HOL installed on it. Alternatively, access to a limited number of machines at the Turku Centre for Computer Science can be provided. Although a few hard copies of the tutorial will be available during the course, you may want to bring your own copy. About the speaker: www4.informatik.tu-muenchen.de/~nipkow Joachim Parrow, The pi-calculus is a process algebra where agents communicate by sending communication ports, or capabililtes, to each other. In this introduction I shall present some of the basic ideas and intutions and give a small modelling example from mobile telephony Recommended reading: http://www.docs.uu.se/~joachim/intro.ps Gruia-Catalin Roman, Mobile computing is defined as the study of systems that entail the movement of components within a physical or logical space. In practice, code fragments can migrate among hosts and hosts can change physical locations. Mobile UNITY refers to a notation and proof logic specialized to mobile computing. An adaptation of UNITY (a concurrency model proposed by Chandy and Misra), Mobile UNITY separates the description of a system into mobile programs and interactions. Programs represent the basic unit of mobility and are described using a notation that closely resembles UNITY. The key differences are the fact that variables with the same name appearing in distinct programs are presumed to be distinct, and a distinguished variable denoting the location is added to each program. Mobile UNITY uses this location variable to capture movement. By modeling movement as value assignment, the Mobile UNITY proof logic easily accommodates reasoning about space and motion. Interactions among mobile units are captured using a minimalist coordination language whose constructs allow one to specify asynchronous data transfer, reactive processing, and statement inhibition. Most importantly, the UNITY proof logic was extended to accommodate the new constructs and the desired coordination semantics. The expressive power of Mobile UNITY has been investigated through a series of case studies involving: the formulation of novel high-level coordination constructs; formal specification and verification of Mobile IP; modeling and verification of paradigms in logical mobility (i.e., remote evaluation, code on demand, and mobile agents); development of a fine-grained model of code mobility (CodeWeave), which allows for the movement of single variables, single statements, or complex block structured programs; formulation and derivation of mobile algorithms (e.g., termination detection in ad hoc networks); and formal semantic specification of a middleware for mobility (Lime-Linda in a Mobile Environment). About the speaker: www.cs.wustl.edu/~roman Kaisa Sere, These lectures present an approach to system development using the Action Systems formalism as the underlying formal framework. The approach is based on viewing a system, consisting of hardware and/or software, as a set of concurrent, distributed, co-operating entities. We exemplify the development approach via a few case studies on the design of e.g. control systems and software, digital circuits, mobile agents. About the speaker: www.abo.fi/~kaisa Natarajan Shankar, Recent advances in verification technology have yielded a sophisticated suite of automated techniques. We describe some of these techniques and methods for combining them to construct useful analysis tools for hardware and software designs. The methods include propositional satisfiability solvers, explicit-state and symbolic model checkers, typecheckers, ground decision procedures, interactive theorem provers, and property-preserving abstractors. SRI International's SAL, PVS, and ICS tools will be presented as illustrative examples. About the speaker: www.csl.sri.com/~shankar Bernhard Steffen, In current practice, only rarely precise and reliable documentation of a system's behavior is produced during its development. Revisions and last minute changes invalidate design sketches, and while systems are updated in the maintenance cycle, often their implementation documentation is not. Regular extrapolation aims at providing descriptions of systems or system aspects a posteriori in a largely automatic way. These descriptions come in the form of models which offer the possibility of mechanically producing system tests, grading test suites and monitoring running systems. The models are built from observations via techniques from machine learning and finite automata theory. Also expert knowledge about the system enters the model construction in a systematic way. The lectures develop the underlying semantical foundations and illstrate them in the context of concrete application scenarios. About the speaker: ls5-www.cs.uni-dortmund.de/staff/steffen.de.html
|