Friday July 26th

All assigned slots
See also the by-session program


IMLAPAPM-PROBMIVLLFCSVERIFYCiADUNIFRVLFMITRS
RV #1 (Aud. 9)
08:30  Levy, Saïdi, and Uribe: Combining monitors for run-time system verification
IMLA #1 (Aud. 2)
08:50  Opening
PAPM-PROBMIV #5: Invited talk (Aud. 3)
08:50  Sands: Probability and timing: Challenges for secure programming
ITRS #1 (A101)
08:45  Opening
Invited talk
09:00  Scott: Realizability and modality
LL #3 (Aud. 4)
Invited lecture
09:00  Blute: Linear logic, relations and vector spaces
FCS+VERIFY #5: FCS Invited talk (Aud. 6)
Invited talk
09:00  Gollmann: Defining security is difficult and error prone
CiAD #5 (Aud. 7)
Invited talk
09:00  Blumensath and Grädel: Finite presentations of infinite structures: Automata and interpretation
UNIF #4 (Aud. 8)
Invited talk
09:00  Dershowitz and Kirchner: Abstract canonical inference systems
09:00  Zuck, Pnueli, Fang, Goldberg, and Hu: Translation and run-time validation of optimized codeLFM #1 (Aud. 10)
09:00  López, Pimentel, Hodas, Polakow, and Stoilova: Isolating resource comsumption in linear-logic proof search
09:00  Ghilezan and Likavec: Reducibility: a ubiquitous method in lambda calculus with intersection types
09:30  Yong and Horwitz: Reducing the overhead of dynamic analysis09:30  Vanderwaart and Crary: A simplified account of the metatheory of linear LF09:30  Dezani-Ciancaglini, Frish, Giovanetti, and Motohama: The relevance of semantic subtyping
PAPM-PROBMIV #6: Security (Aud. 3)
09:50  Aldini and Gorrieri: Security analysis of a probabilistic non-repudiation protocol
Invited lecture
09:50  Terui: On the complexity of cut elimination in linear logic
10:00  Awodey and Bauer: Propositions as [types]10:00  Berwanger and Grädel: Fixed point formulae and solitaire games10:00  Ranise: A superposition decision procedure for the logic of equality with interpreted and uninterpreted functions10:00  Brörkens and Möller: Dynamic event generation for runtime checking using the JDI10:00  Stump and Dill: Producing proofs from an arithmetic decision procedure in elliptical LF10:00  Rocca: Intersection typed lambda calculus

R E F R E S H M E N T S

IMLA #2 (Aud. 2)
11:00  Hermida: A categorical outlook on relational modalities and simulations
PAPM-PROBMIV #7: Model checking (Aud. 3)
11:00  Huth: Possibilistic and probabilistic abstraction-based model checking
LL #4 (Aud. 4)
11:00  Hughes and van Glabbeek: MALL proof nets
FCS #6: Programming Language Security (Aud. 5)
11:00  Bauer, Ligatti, and Walker: More enforceable security policies
VERIFY #6: Specification and Verification (Aud. 6)
11:00  Herzog and Guttman: Eager formal methods for security management
CiAD #6 (Aud. 7)
Invited talk
11:00  Pichler: Algorithms and complexity of model representations
UNIF #5 (Aud. 8)
11:00  Bachmair and Scharff: Direct combination of completion and congruence closure
RV #2 (Aud. 9)
Invited talk
11:00  Peled: Tracing the executions of concurrent programs
LFM #2 (Aud. 10)
11:00  van Raamsdonk and Severi: Eliminating proofs from programs
ITRS #2 (A101)
11:00  Alessi and Lusin: Simple easy terms
11:30  Bellin: Towards a formal pragmatics: An intuitionistic theory of assertive and conjectural judgements with an extension of Gödel, McKinsey and Tarski's S4 translation.11:30  Mellies: Innocence in 2-dimensional games11:30  Liu and Smith: A component security infrastructure11:30  Armando, Bonacina, Ranise, Rusinowitch, and Sehgal: High-performance deduction for verification: a case study in the theory of arrays11:30  Marin and Middeldorp: New completeness results for lazy conditional narrowing11:30  Momigliano, Ambler, and Crole: A hybrid encoding of Howe's method for establishing congruence of bisimilarity11:30  Carlier: Polar type inference with intersection types and omega
11:40  Kwiatkowska, Norman, and Pacheco: Model checking CSL until formulae with random time bounds
12:00  Brunet: A modal logic for observation-based knowledge representation12:00  Slavnov: Geometrical semantics for linear logic (multiplicative fragment)12:00  Skalka and Smith: Static use-based object confinement12:00  Beckert, Keller, and Schmitt: Translating the object constraint language into first-order predicate logic12:00  Terán and Edmonds: Computational complexity of a constraint model-based proof of the envelope of tendencies in a MAS-based simulation model12:00  Korovin and Voronkov: The decidability of the first-order theory of the Knuth-Bendix orders in the case of unary signatures12:00  Karaorman and Abercrombie: jContractor: Bytecode instrumentation techniques for implementing design by contract in Java12:00  Scagnetto and Miculan: Ambient Calculus and its logic in the Calculus of Inductive Constructions12:00  Kfoury, Washburn, and Wells: Implementing compositional analysis using intersection types with expansion variables

L U N C H

IMLA #3 (Aud. 2)
Invited talk
14:00  Sambin: Open truth and closed falsity
PAPM-PROBMIV #8: Short presentations (Aud. 3)
14:00  Lassaigne and Peyronnet: Approximate verification of probabilistic systems
LL #5 (Aud. 4)
14:00  Coppola and della Rocca: Principal typing in elementary affine logic
FCS+VERIFY #7 (Aud. 6)
Panel
14:00  Cohen, Jeffrey, Martinelli, Massacci, Meadows, and Basin: The future of protocol verification
CiAD #7 (Aud. 7)
14:00  Discussion
UNIF #6 (Aud. 8)
Invited talk
14:00  Lynch: Decidability and complexity of e-unification for some classes of equational theories
RV #3 (Aud. 9)
14:00  Kim, Lee, Sammapun, Shin, and Sokolsky: Monitoring, checking, and steering of real-time systems
LFM #3 (Aud. 10)
14:00  Delahaye: A proof dedicated meta-language
ITRS #3 (A101)
Invited talk
14:00  Pfenning: Tri-directional type checking
14:20  Bournez: A generalization of equational proof theory?
14:30  Berdine, O'Hearn, and Thielecke: Extracting the range of CPS from affine typingInvited talk
14:30  Comon: How difficult is it to retrieve a secret?
14:30  Stoller: Testing concurrent Java programs using randomized scheduling14:30  Pientka: Memoization-based proof search in LF: An experimental evaluation of a prototype
14:40  Pierro and Wiklicky: Probabilistic abstract interpretation and statistical testing
15:00  Davoren, Coulthard, Moor, Gore, and Nerode: Topological semantics for intuitionistic modal logics, and spatial discretisation by A/D maps15:00  Bravetti: An integrated approach for the specification and analysis of stochastic real-time systems15:00  Roversi: A bridge between a proof-theoretical and a declarative system for polynomial functions15:00  Anantharaman, Narendran, and Rusinowitch: ACID-unification, rewrite reachability and set constraints15:00  Bhargavan and Gunter: Requirements for a practical network event recognition language15:00  Schürmann and Autexier: Towards proof planning for Mω+15:00  Leivant: Feasible functionals and intersection of ramified type
15:30  Closing Remarks

R E F R E S H M E N T S

IMLA #4 (Aud. 2)
16:00  Maietti and Ritter: Modal run-time analysis revisited
PAPM-PROBMIV #9: Refinement strategies (Aud. 3)
16:00  D'Argenio, Jeannet, Jensen, and Larsen: Reduction and refinement strategies for probabilistic analysis
LL #6 (Aud. 4)
15:50  Farwer and Misra: Object net modification using linear logic Petri nets
CiAD #8 (Aud. 7)
Invited talk
16:00  Voronkov: The Knuth-Bendix orderings
UNIF #7 (Aud. 8)
16:00  Baader and Tinelli: ACU-unification with a successor symbol
RV #4 (Aud. 9)
16:00  Finkbeiner, Sankaranarayanan, and Sipma: Collecting statistics over runtime executions

16:00-17:30: LFM #4: System Demonstrations (Aud. 10)

ITRS #4 (A101)
16:00  Courant: Strong normalization with singleton types
16:20  Bozzano and Delzanno: Protocol verification via a bottom-up evaluation strategy for linear logic programs
16:30  Discussion16:30  Nguyen: A constructive decision procedure for equalities modulo AC16:30  Kim, Kannan, Lee, Sokolsky, and Viswanathan: Computational analysis of run-time monitoring16:30  van Bakel: Strongly normalising cut-elimination with strict intersection types

16:40-16:50: PAPM-PROBMIV Closing and Farewell (Aud. 3)

Keynote address (Aud. 1)
Plenary talk
17:00  Henkel: Artificial intelligence: Disappointment or hope?
17:00  Cervesato: Solution count for multiset unification with trailing multiset variables Keynote address (Aud. 1)
Plenary talk
17:00  Henkel: Artificial intelligence: Disappointment or hope?
17:00  de'Liguoro: Subtyping in logical form
17:30  Business Meeting