FLoC '02 - Thursday July 25th

Thursday July 25th

All assigned slots
See also the by-session program

LICS	IDAY	PAPM-PROBMIV	LL	FCS	VERIFY	CiAD	UNIF	CADE-T1	WG16	HYLO
				08:45-09:00: FCS Opening Remarks (Aud. 5)	VERIFY #1: Applications of ATP in Verification (Aud. 6) 08:45 Welcoming and Opening Remarks
LICS #14 (Aud. 1) Invited tutorial 09:00 Lenzerini: Description logics: Foundations for class-based knowledge representation	IDAY #1 (Aud. 2) 09:00 Welcome			FCS #1: Foundations of Security (Aud. 5) 09:00 Küsters: On the decidability of cryptographic protocols with open-ended data structures	09:00 Kröning: Application specific higher order logic theorem proving	CiAD #1 (Aud. 7) Invited talk 09:00 Cadoli: The expressive power of binary linear programming		09:00-10:30: CADE-T1 #1: ACL2 Architecture and Applications (Aud. 9)	WG16 #1 (A101) 09:00 Welcome	HYLO #1 (A102) Invited talk 09:00 Fitting: AddOns
	IDAY #1 (Aud. 2) 09:00 Welcome	09:10-09:30: PAPM-PROBMIV Welcome and Opening (Aud. 3)							09:10 Giesl: Modular termination proofs using dependency pairs
	09:15 On FME	09:10-09:30: PAPM-PROBMIV Welcome and Opening (Aud. 3)					UNIF #1 (Aud. 8) 09:25 Welcome
	Invited talk 09:30 Thomas: Formal methods in industry: Disease and remedies	PAPM-PROBMIV #1: Invited talk (Aud. 3) 09:30 Schiper: Failure detection vs. group membership in fault-tolerant distributed systems: hidden trade-offs		09:30 Lye and Wing: Game strategies in network security	09:30 Vanackère: The TRUST protocol analyser, automatic and efficient verification of cryptographic protocols		Invited talk 09:30 Kohlhase: Sorted higher-order unification
				09:30 Lye and Wing: Game strategies in network security					09:50 Gramlich: Progress report on strategies in rewriting
10:00 Otto: Modal and guarded characterisation theorems over finite transition systems	Invited talk 10:00 Bolignano: Experience from applying formal methods to critical security issues			10:00 Conchon: Modular information flow analysis for process calculi	10:00 Benzmüller, Giromini, Nonnengart, and Zimmer: Reasoning services in MathWeb-SB for symbolic verification of hybrid systems	10:00 Schmidt-Schauß and Stuber: On the complexity of linear and stratified context matching problems				10:00 Areces, Blackburn, Marx, and Sattler: Welcome to the workshop
R E F R E S H M E N T S
LICS #15 (Aud. 1) 11:00 Laroussinie, Markey, and Schnoebelen: Temporal logic with forgettable past	IDAY #2 (Aud. 2) Invited talk 11:00 Larsen: Practical use of VDM technology in industry	PAPM-PROBMIV #2: Numerical analysis algorithms (Aud. 3) 11:00 Kwiatkowska and Mehmood: Out-of-core solution of large linear systems of equations arising from stochastic modelling	LL #1 (Aud. 4) Invited lecture 11:00 Guerrini: From proof nets to sharing graphs: From logic to implementations	FCS+VERIFY #2: Logical Approaches (Aud. 6) 11:00 Appel, Michael, Stump, and Virga: A trustworthy proof checker		CiAD #2 (Aud. 7) Invited talk 11:00 Kolaitis: On the complexity of model checking and inference in minimal models	UNIF #2 (Aud. 8) 11:00 Schmidt-Schauß and Schulz: Decidability of bounded higher-order unification	11:00-12:30: CADE-T1 #2: ACL2: The Method Demo (Aud. 9)	WG16 #2 (A101) 11:00 Bonacina: Deciding satisfiability problems by rewrite-based deduction: Experiments in the theory of arrays	HYLO #2 (A102) 11:00 Areces and Lutz: Concrete domains and nominals united
11:30 Hodkinson, Wolter, and Zakharyaschev: Decidable and undecidable fragments of first-order branching temporal logics	Invited talk 11:30 Peleska: Formal methods-based testing for large scale industrial applications			11:30 Cohen: Proving protocols safe from guessing			11:30 Hamana: Simple β₀-unification for terms with context holes			11:30 Braüner: Natural deduction for first-order hybrid logic
		11:40 Bohnenkamp and Haverkort: The mean value of the maximum							11:40 Dershowitz: Progress report
			Invited lecture 11:50 Laurent: Polarities in linear logic
12:00 Kreutzer: Expressive equivalence of least and inflationary fixed-point logic	Invited talk 12:00 Sabatier: The use of the B formal method to produce accurate and complete technical documents			12:00 Armando and Compagna: Automatic SAT-compilation of security problems		12:00 Durand and Hermann: The inference problem for propositional circumscription of affine formulas is coNP-complete	12:00 Niehren and Villaret: Parallelism and tree regular constraints			12:00 Heinemann: Axiomatizing modal theories of subset spaces
									12:20 van Oostrom: Term rewriting systems
L U N C H
LICS #16 (Aud. 1) 14:00 Desharnais, Gupta, Jagadeesan, and Panangaden: The metric analogue of weak bisimulation for probabilistic processes	IDAY #3 (Aud. 2) Invited talk 14:00 Bloomfield: Drivers in the application of formal methods	PAPM-PROBMIV #3: Symbolic computation (Aud. 3) 14:00 Kuntz and Siegle: Deriving symbolic representations from stochastic process algebras		FCS+VERIFY #3: VERIFY Invited talk (Aud. 6) Invited talk 14:00 Massacci: Formal verification of SET by Visa and Mastercard: Lessons for formal methods in security		CiAD #3 (Aud. 7) 14:00 Discussion	UNIF #3 (Aud. 8) 14:00 Monate: Parameterized string rewriting systems	14:00-15:30: CADE-T1 #3: ACL2: Flying Demo (Aud. 9)	14:00-15:30: WG16 #3: Business meeting (A101)	HYLO #3 (A102) Invited talk 14:00 Vardi: Logic and automata: Words, trees, and forests
14:30 Hirschkoff, Lozes, and Sangiorgi: Separability, expressiveness, and decidability in the ambient logic	14:30 Summary and Discussion					Invited talk 14:30 Grohe: On the complexity of constraint satisfaction problems	14:30 Ohsaki and Takai: A tree automata theory for unification modulo equational rewriting
		14:40 Kwiatkowska, Norman, and Sproston: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol
15:00 Nygaard and Winskel: Linearity in process languages							15:00 Ghilardi and Sacchetti: Filtering unification: the case of modal logic			15:00 Blackburn and Marx: Constructive interpolants for every bounded fragment definable hybrid logic
R E F R E S H M E N T S
LICS #17 (Aud. 1) 16:00 Tiwari: Deciding confluence of certain term rewriting systems in polynomial time	IDAY #4 (Aud. 2) Invited talk 16:00 Pearce: The EU's future and emerging technologies programme: New themes and instruments in the 6th framework programme	PAPM-PROBMIV #4: Non-interleaving models (Aud. 3) 16:00 Fecher, Majster-Cederbaum, and Wu: Action refinement for probabilistic processes with true concurrency models	LL #2 (Aud. 4) 16:00 Miller: Higher-order quantification and proof search: an extended abstract	FCS+VERIFY #4: Verification of Security Protocols (Aud. 6) 16:00 Meadows: Identifying potential type confusion in authenticated messages		CiAD #4 (Aud. 7) Invited talk 16:00 Narendran: Unification problems with homomorphisms: decidability and complexity results		16:00-17:30: CADE-T1 #4: ACL2: Additional Topics (Aud. 9)	WG16 #4 (A101) 16:00 Lucas: Computational restrictions of rewriting in functional programming	HYLO #4 (A102) 16:00 Blackburn and ten Cate: Beyond pure axioms: Node creating rules in hybrid tableaux
16:30 Björklund and Vorobyov: Two adversary lower bounds for parity games			16:30 Biri and Galmiche: A modal linear logic for distribution and mobility	16:30 Steel, Bundy, and Denney: Finding counterexamples to inductive conjectures and discovering security protocol attacks						16:30 de Freitas, Viana, Veloso, Veloso, and Benevides: On hybrid arrow logic
16:40 Beffara and Vorobyov: Is randomized Gurvich-Karzanov-Khachiyan's algorithm for parity games polynomial?		16:40 Haar: Probabilistic unfoldings and partial order fairness in Petri nets							16:40 Discussion
16:50 Covino and Pani: Time-space computational complexity of imperative programming languages									16:40 Discussion
			17:00 Harland: Issues for proof-theoretic modelling of embedded infinitary computations			17:00 Discussion				17:00 Palm: Characterizing tree-adjoining grammars with hybrid logic

		18:30-19:30: PAPM-PROBMIV PAPM-ProbMiV business meeting (Aud. 3)