Saturday July 20th

All assigned slots
See also the by-session program


08:45-09:00: REFINE #1: Opening and introduction (Aud. 4)

FICS #1 (Aud. 2)
Invited talk
09:00  Winskel: Calculus for categories
DOMAIN #1 (Aud. 3)
Invited talk
09:00  Hyland: Thirty years on! domain models for lambda calculus: the categorical logic perspective
REFINE #2: Refinement calculus I (Aud. 4)
Invited talk
09:00  Back and von Wright: Compositional action system refinement
FME-T2 #1: Introduction (Aud. 9)
09:00  Business Process Engineering

09:00-10:30: FME-T1 #1: Introduction to PVS (Aud. 10)

09:15  Benefits of Process Modeling
FME-T2 #2: Basic Concepts (Aud. 9)
09:30  Requirements to Modeling Methods
09:40  Dunne: Junctive compositions of specifications in total and general correctness
10:00  Adamek, Milius, and Velebil: Parametric corecursion and completely iterative monads10:00  Plotkin and Power: Computational effects and operations: an overview10:00  Established Modeling Methods
10:05  Aichernig: Contract-based mutation testing in the refinement calculus


FICS #2 (Aud. 2)
11:00  Ghani, Lüth, and Marchi: Coalgebraic approaches to algebraic terms
DOMAIN #2 (Aud. 3)
Invited talk
11:00  Reynolds: Relating intrinsic and extrinsic semantics in domain theory
REFINE #3: Refinement calculus II (Aud. 4)
Invited talk
10:50  Naumann: OO/higher order refinement calculus
ICC #1 (Aud. 8)
Invited talk
11:00  Voda: Two simple intrinsic characterizations of main complexity classes
FME-T2 #3: Modeling and Analysis (Aud. 9)
11:00  Modeling Tasks

11:00-12:30: FME-T1 #2: New Capabilities in PVS 3.0 (Aud. 10)

11:30  Uustalu: Generalizing substitution11:30  Lopes and Fiadeiro: Superposition: Composition vs refinement of non-deterministic, action-based systemsVDM Invited talk (Aud. 7)
11:30  Oliveira: On the design of a "periodic table" of VDM specifications
11:30  Modeling Resources and Roles
Invited talk
11:50  Wildman and Fidge: The variety of variables in computer-aided real-time programming
12:00  Benton and Hyland: Traced pre-monoidal categories12:00  Flax: Approximation of entailment12:00  Bournez, de Naurois, and Marion: Safe recursion and calculus over an arbitrary structure12:00  Quality of Models
12:15  Hilton and Hall: Refining specifications to programmable logic


FICS #3 (Aud. 2)
Invited talk
14:00  Aceto: Kleene through the process algebraic glass
DOMAIN #3 (Aud. 3)
Invited talk
14:00  Curien: Playful computation
REFINE #4: Z and Concurrency I (Aud. 4)
14:00  Stepney, Polack, and Toyn: Refactoring in maintenance and development of Z specifications and proofs
VDM #1 (Aud. 7)
14:00  Maury, Ledru, Bontron, and du Bousquet: Using TOBIAS for the automatic generation of VDM test cases
ICC #2 (Aud. 8)
Invited talk
14:00  Frederiksen and Jones: Program analysis for implicit computational complexity
FME-T2 #4: Web Services (Aud. 9)
14:00  New Challenges

14:00-15:30: FME-T1 #3: Introduction to ICS (Aud. 10)

14:30  Groves: Refinement and the Z schema calculus14:30  Koptelov, Kuliamin, and Petrenko: VDM++TesK: Testing of VDM++ programs14:30  Extension of Existing Approaches
15:00  Sprenger and Dam: A note on global induction in a mu-calculus with explicit approximations15:00  Karazeris and Velebil: Left exact Kan extensions, powerdomain distributivity, preservation of bisimulation15:00  Bolton and Davies: A comparison of refinement orderings and their associated simulation rules15:00  Aguirre, Bicarregui, Dimitrakos, and Maibaum: Structuring in VDM and B15:00  Kristiansen: New recursion-theoretic characterizations of well known complexity classes15:00  Perspective and Limitations


FICS #4 (Aud. 2)
16:00  Shilov and Garanina: Model checking knowledge and fixpoints
DOMAIN #4 (Aud. 3)
16:00  Adámek: On a description of free iterative theories
REFINE #5: Z and Concurrency II (Aud. 4)
Invited talk
15:50  Derrick and Boiten: Unifying concurrent and relational refinement
VDM #2 (Aud. 7)
16:00  Terada: Integrity analysis of digital ATC track database with automatic proofs
ICC #3 (Aud. 8)
16:00  Aehlig and Johannsen: An elementary fragment of second-order lambda calculus
FME-T2 #5: Software Support (Aud. 9)
16:00  Overview on Available Software Tools

16:00-17:30: FME-T1 #4: Introduction to SAL (Aud. 10)

16:30  Devereux: Strong next-time operators for multiple-valued mu-calculusInvited talk
16:30  Escardó: Interactions between domain theory and topology
Invited talk
16:30  Cavalcanti and Woodcock: Refinement of actions in Circus
16:30  Araki and Chang: Formal methods in Japan: Current state, problems and challenges16:30  Niggl: Control structures in programs and computational complexity16:30  Tool Demonstration
REFINE #6: Architecture I (Aud. 4)
Invited talk
17:15  Börger: Refinement method for Abstract State Machines
18:00  Anlauff and Sünbül: Towards component based systems: refining connectors

19:00-23:00: DOMAIN DOMAIN dinner (Restaurant Langelinie Pavillonen)