Thursday July 25th

All assigned slots
See also the by-session program


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 provingCiAD #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

09:10-09:30: PAPM-PROBMIV Welcome and Opening (Aud. 3)

09:10  Giesl: Modular termination proofs using dependency pairs
09:15  On FMEUNIF #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 security09:30  Vanackère: The TRUST protocol analyser, automatic and efficient verification of cryptographic protocolsInvited talk
09:30  Kohlhase: Sorted higher-order unification
09:50  Gramlich: Progress report on strategies in rewriting
10:00  Otto: Modal and guarded characterisation theorems over finite transition systemsInvited talk
10:00  Bolignano: Experience from applying formal methods to critical security issues
10:00  Conchon: Modular information flow analysis for process calculi10:00  Benzmüller, Giromini, Nonnengart, and Zimmer: Reasoning services in MathWeb-SB for symbolic verification of hybrid systems10:00  Schmidt-Schauß and Stuber: On the complexity of linear and stratified context matching problems10:00  Areces, Blackburn, Marx, and Sattler: Welcome to the workshop


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 logicsInvited talk
11:30  Peleska: Formal methods-based testing for large scale industrial applications
11:30  Cohen: Proving protocols safe from guessing11:30  Hamana: Simple β0-unification for terms with context holes11:30  Braüner: Natural deduction for first-order hybrid logic
11:40  Bohnenkamp and Haverkort: The mean value of the maximum11:40  Dershowitz: Progress report
Invited lecture
11:50  Laurent: Polarities in linear logic
12:00  Kreutzer: Expressive equivalence of least and inflationary fixed-point logicInvited 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 problems12:00  Durand and Hermann: The inference problem for propositional circumscription of affine formulas is coNP-complete12:00  Niehren and Villaret: Parallelism and tree regular constraints12:00  Heinemann: Axiomatizing modal theories of subset spaces
12:20  van Oostrom: Term rewriting systems


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 logic14:30  Summary and DiscussionInvited 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 languages15:00  Ghilardi and Sacchetti: Filtering unification: the case of modal logic15:00  Blackburn and Marx: Constructive interpolants for every bounded fragment definable hybrid logic


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 games16:30  Biri and Galmiche: A modal linear logic for distribution and mobility16:30  Steel, Bundy, and Denney: Finding counterexamples to inductive conjectures and discovering security protocol attacks16: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 nets16:40  Discussion
16:50  Covino and Pani: Time-space computational complexity of imperative programming languages
17:00  Harland: Issues for proof-theoretic modelling of embedded infinitary computations17:00  Discussion17:00  Palm: Characterizing tree-adjoining grammars with hybrid logic

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