June 30 |
||
All day:
Workshop on Implicit Computational Complexity A Tutorial Workshop on Realizability Semantics and Applications Workshop on Gröbner Bases and Rewriting Techniques |
Afternoon:
Plenary Invited Speakers Session 13:40 Dynamic Reachability
|
|
July 1 |
||
All day:
Workshop on Implicit Computational Complexity A Tutorial Workshop on Realizability Semantics and Applications Workshop on Finite
Model Theory and Applications
|
||
July 2 |
||
LICS |
RTA |
|
9:00-10:00 | INVITED TALK (chair: G. Longo)
Some enormous lower bounds H. Friedman (Ohio State Univ.) |
Session 1 (chair: M. Rusinowitch)
Solved forms for path ordering constraints
Jeopardy
|
10:00-10:30 | Session 1 (chair: M. Otto)
starts 10:05 Two-Variable Descriptions of Regularity
|
Strategic Pattern Matching
E. Visser (Pacific Software Res. Cntr) |
10:30-11:00 | COFFEE | COFFEE |
11:00-12:15 | Session 1 (chair: M. Otto)
The Two-Variable Guarded Fragment with Transitive Relations
Logics with Aggregate Operators
Guarded Fixed Point Logic
|
Session 2 (chair: A. Asperti)
On the strong normalization of natural deduction
Normalisation in weakly orthogonal rewriting
Strong normalization of proof-nets modulo
|
12:15 - 14:00 | LUNCH | LUNCH |
14:00-15:15 | Session 2 (chair: D. Sangiorgi)
Towards a theory of bisimulation for local names
Weak Bisimulation and Open Maps
Elementary Axioms for Categories of Classes
|
Session 3 (chair: K. Madlener)
starts at 14:15 INVITED TALK
|
15:15-15:45 | COFFEE | COFFEE |
15:45-17:45 | Session 3 (chair: M. Dezani)
Region analysis and the polymorphic lambda calculus
Pattern Matching as Cut Elimination
BREAK (16:35-16:55) Some Computational Properties of Intersection Types
Type Inference for Recursive Definitions
|
Session 4 (chair: C. Kirchner)
Undecidability of the exists-forall part of the
Solving one step rewriting formulae
A new result about the decidability of the
RTA BUSINESS MEETING (starts 17:30) |
July 3 |
||
LICS |
RTA |
|
9:00-10:00 | INVITED TALK (chair: M. Abadi)
Plausibility measures and default reasoning J. Halpern (Cornell Univ) |
Session 5 (chair: B. Gramlich)
A fully syntactic AC-RPO
|
10:00-10:30 | Session 4 (chair: M. Abadi)
starts 10:05 Subtyping Recursive Types in Kernel Fun
|
A characterisation of multiply recursive functions
H. Touzet (Univ. Lille) |
10:30-11:00 | COFFEE | COFFEE |
11:00-12:15 | Session 4 (chair: M. Abadi)
A Fragment Calculus - towards a model of
Proof techniques for Cryptographic Processes
On Hoare Logic and Kleene Algebra with Tests
|
Session 6 (chair: J. Hsiang)
Deciding the word problem in the union of
Normalization via rewrite closure
Test sets for the universal and existential closure
|
12:15-14:00 | LUNCH | LUNCH |
14:00-15:15 | Session 5 (Chair: T. Ehrhard)
Full Abstraction via Realisability
On Bunched Predicate Logic
Abstract Syntax and Variable Binding
|
Session 7 (chair: D. Kesner)
Starts at 14:15 INVITED TUTORIAL
|
15:15-15:45 | COFFEE | COFFEE |
15:45-17:45 | Session 6 (Chair: M. Okada)
Semantical analysis of higher-order abstract syntax
A New Approach to Abstract Syntax Involving Binders
BREAK (16:35-16:55) Paramodulation with Non-Monotonic Orderings
Full completeness of the multiplicative linear logic
18:00 LICS BUSINESS MEETING |
Session 8 (chair: H. Kirchner)
The Maude system
TOY: A Multiparadigm Declarative System
BREAK (16:25-16:35) UniMoK: A System for Combining Equational
LRR: A Laboratory for Rapid Term
|
July 4 |
||
LICS |
RTA |
|
9:00-10:00 | INVITED TALK (chair: W. Thomas)
Cartesian Closed Double Categories, their Lambda Notation and the Pi-Calculus U. Montanari (Univ. Pisa) |
Session 9 (chair: A. Voronkov)
Decidability for Left-Linear Growing TRS
Transforming Context-Sensitive Rewrite Systems
|
10:00-10:30 | Session 7 (chair: M. Grohe)
starts 10:05 Weak Bounded Arithmetic, the Diffie-Hellman
|
Context-sensitive AC-rewriting
M.C.F. Ferreira, A. Ribeiro (Univ. Nova de Lisboa) |
10:30-11:00 | COFFEE | COFFEE |
11:00-12:15 | Session 7 (chair: M. Grohe)
First-Order Logic vs. Fixed-Point Logic in
Entailment of Atomic Set Constraints is
A Superposition Decision Procedure for the
|
Session 10 (chair: R. Kennaway)
The calculus of algebraic constructions
HOL-lambdasigma
Session ends at 12:00 |
12:15-14:00 | LUNCH | LUNCH |
14:00-15:15 | Session 8 (chair: S. Weinstein)
Working with arms: complexity results on atomic
Logics with Counting, Auxiliary Relations, and
Counting and Addition cannot express
|
Session 11 (chair: P. Narendran)
starts 14:15 INVITED TALK
|
15:15-15:45 | COFFEE | COFFEE |
15:45 - 17:45 | Session 9 (chair: N. Shankar)
Parametric Quantitative Temporal Reasoning
Modular Temporal Logic
16:35 - 16:55 BREAK On the Verification of Broadcast Protocols
On the Expressive Power of CTL*
|
Session 12 (chair: F. Otto)
A rewrite system associated with quadratic
Fast rewriting of symmetric polynomials
On Implementation of Tree Synchronized
Session ends 17:15
|
19:30 | CONFERENCE DINNER | CONFERENCE DINNER |
JULY 5 |
||
LICS |
OTHER EVENTS |
|
9:00-10:00 | INVITED TALK (chair: A. Asperti)
Proving Security Protocols Correct
|
All day:
Workshop on Explicit
Substitutions
|
10:05-10:30 | Session 10 (Chair: E. Robinson)
Reasoning about common knowledge with
|
All day:
Workshop on Strategies in
Automated Deduction
|
10:30-11:00 | COFFEE | |
11:00-12:15 | Session 10 (Chair: E. Robinson)
Parikh's Theorem in Commutative Kleene Algebra
The Higher-order Recursive Path Ordering
Extensional Equality in Intensional Type Theory
|
All day:
5th International SPIN Workshop on
|
12:15-14:00 | LUNCH | |
14:00-15:15 | Session 11 (Chair: V. Danos)
A fully abstract game semantics for finite nondeterminism
Concurrent Games and Full Completeness
Non-deterministic Games and Program Analysis:
|
All day:
Workshop on Formal
Methods and Security Protocols
|
15:15-15:45 | COFFEE | |
15:45-16:35 | Session 12 (Chair: A. Asperti)
Correctness of Multiplicative Proof Nets is Linear
Linear types and non-size-increasing
|
Evening:
Using formal verification methods in an
Gerard Roucairol
|
16:35-17:00 | BREAK | |
17:00-18:00 | INVITED TALK (chair: G. Longo)
On the meaning of logical rules : ludics
END OF LICS |
|
July 6 |
||
CAV TUTORIAL DAY |
OTHER EVENTS |
|
9:00-10:00 | Chair: Doron Peled
Symbolic model checking
|
All day:
Workshop on Intuitionistic
Modal Logics and
|
10:00-10:30 | COFFEE | |
10:30-11:30 | Chair: Doron Peled
Hardware Verification
|
All day:
Workshop on Complexity-Theoretic
and
|
12:00-14:00 | LUNCH | |
14:00-15:00 | Chair: Nicolas Halbwachs
Specification and verification of timed systems
|
All day:
Workshop on Automation of Proof by Mathematical Induction |
15:00-15:30 | COFFEE | |
15:30-16:30 | Chair: Nicolas Halbwachs
Model checking of timed and hybrid systems
|
All day:
Workshop on Symbolic Model Checking |
All day:
Workshop on Run-Time Result Verification |
||
6:00-8:00 | Panel on:
"Current trends in research funding in the use of logic and formal methods in computer science" Moderator: Alan Bundy
|
|
July 7 |
||
|
CAV |
CADE |
9:00-10:00 | Chair: David Dill
INVITED PAPER
|
Session 1 Chair: Pat Lincoln
A dynamic programming approach to
Tractable Transformations from Modal
|
10:00-10:30 | COFFEE | COFFEE |
10:30-12:30 | Regular session: Processor verification
Chair: Bob Kurshan Proof of Correctness of a Processor with Reorder
Verifying Safety Properties of a PowerPC(TM)
Model Checking the IBM Gigahertz Processor: An
Validation of Pipelined Processor Designs using
|
Session 2 Chair: H. Comon
INVITED TALK
A PSPACE Algorithm for Graded Modal Logic
Session ends at 12:00 |
12:30-14:00 | LUNCH | LUNCH |
14:00-15:30 | Regular session: Protocols verification and testing
Chair: Tom Henzinger Automated verification of a parametric real-time
Test generation derived from model-checking
Latency Insensitive Protocols
|
Session 3 Chair: F. Baader
Solvability of Context Equations with
Complexity of the higher order matching
Solving equational problems efficiently
|
15:30-16:00 | COFFEE | COFFEE |
16:00-17:30 | Regular session: Infinite state space
Chair: Yaron Wolfsthal Handling Global Conditions in Parametrized
Verification of Infinite-State Systems by Combining
Experience with Predicate Abstraction
|
Session 4 Chair: John Slaney
VSDITLU: a verifiable symbolic definite
A Framework for the Flexible Integration of a Class of
Presenting Proofs in a Human-Oriented Way
|
17:30-19:00 | System Demonstrations | |
July 8 |
||
|
CAV |
CADE |
9:00-10:00 | Joint CADE/CAV session
Chair: Fabio Somenzi INVITED TALK
|
Joint session with CAV |
10:00-10:30 | COFFEE | COFFEE |
10:30-12:30 | Regular session: Theory of verification
Chair: Prasad Sistla Model Checking of Safety Properties
A Complete Finite Prefix for Process Algebra
The Mathematical Foundation of Symbolic
Assume-Guarantee Refinement Between
|
Session 5 Chair: Alexander Leitsch
On the Universal Theory of Varieties of Distributive
Maslov's Class K Revisited
Prefixed Resolution - A Resolution Method for
Session ends at 12:00 |
12:30-14:00 | LUNCH | LUNCH |
14:00-15:30 | Regular session: Linear Temporal Logic
Chair: Doron Peled Efficient Decision Prcedures for Model
Stutter-invariant Languages, omega-automata, and
Improved Automata Generation for Linear Time
|
Session 6 System Descriptions
Chair: William McCune Session starts 13:45 Twelf - A Meta-Logical Framework for Deductive Systems
INKA 5.0 - A Logic Voyager
CutRes 1.0: Cut Elimination by Resolution
MathWeb, an Agent-Based Communication Layer for
Using OBDDs for the validation of Skolem
Fault-Tolerant Distributed Theorem Proving
Waldmeister - Improvements in Performance and Ease of Use
|
15:30-16:00 | COFFEE | COFFEE |
16:00-17:30 | Tool presentations
Chair: Ahmed Bouajjani A Toolbox for the Analysis of Discrete
TIPPtool: Compositional Specification and Analysis
Java Bytecode Verification by Model-Checking
NuSMV: a new Symbolic Model Verifier
PIL/SETHEO: A Tool for the Automatic Analysis of
Session ends 17:15 |
Session 7 Chair: Frank Pfenning
Formal Metatheory using Implicit Syntax, and an
A formalization of Static Analyses in System F
On explicit reflection in theorem proving and
18:30-20:30 CADE BUSINESS MEETING
|
17:30-19:00 | Tool demonstrations | |
July 9 |
||
CAV |
CADE |
|
9:00-10:00 | Chair: Gerard Berry
INVITED TALK
|
Session 8 System Descriptions
Chair: David Plaisted Kimba, A Model Generator for Many-Valued
A Compiler and Abstract Machine Based
Vampire
E 0.3
|
10:00-10:30 | COFFEE | COFFEE |
10:30-12:00 | Regular session: Modeling of systems
Chair: Limor Fix On the Representation of Probabilities over
Model Checking Partial State Spaces with 3-Valued
Elementary Microarchitecture Algebra
Verifying sequential consistency on shared memory
|
Session 9 Chair: Andrei Voronkov
INVITED TALK
Towards an Automatic Analysis of Security Protocols in
|
12:00-14:00 | LUNCH | LUNCH |
14:00-15:30 | Regular session: Symbolic model checking
Chair: Ed Clarke Stepwise CTL Model Checking of State/Event Systems Jørn Lind-Nielsen, Henrik Reif Andersen (TU Denmark) Optimizing Symbolic Model Checking for
Efficient Timed Reachability Analysis using Clock
|
Session 10 Chair: Reinhold Letz
A Confluent Connection Calculus
Abstraction-Based Relevancy Testing for
A Breadth-First Strategy for Mating Search
|
15:30-16:00 | COFFEE | COFFEE |
16:00-17:30 | Regular session: Theorem proving.
Chair: Mandayam Srivas Mechanizing Proofs of Computation Equivalence
Linking Theorem Proving and Model-Checking with
Automatic verification of combinational and
|
Session 11 Reports from the Competition
Chairs: Dieter Hutter and Geoff Sutcliffe |
17:30-19:00 | Tool demonstrations | |
10:00-18:00 | PARALLEL EVENT
CASC-16 Competition of Automated Theorem
|
|
19:30 | CONFERENCE DINNER | CONFERENCE DINNER |
July 10 |
||
CAV |
CADE |
|
9:00-10:00 | Chair: Bengt Jonsson
INVITED TALK
|
Session 12 System Descriptions
Chair: Tanel Tammet SPASS Version 1.0.0
KK: a theorem prover for K
An ML Editor Based on Proofs-as-Programs
MCS: Model-based Conjecture Searching
|
10:00-10:30 | COFFEE | COFFEE |
10:30-12:00 | Regular session: Automata theoretic methods.
Chair: Ching-Tsun Chou Efficient Analysis of Cyclic Definitions
A theory of restrictions for logics and automata
Model Checking using Automatic Test-Pattern Generation
Automatic Verification of Abstract State Machines
|
Session 13 Chair: Gilles Dowek
INVITED TALK
Extensional Higher-Order Paramodulation and
Automatic Generation of Proof Search
END OF CADE |
12:00-14:00 | LUNCH | |
14:00-15:30 | Regular session: Abstraction
Chair: Alan Hu Abstract and Model Check while you Prove
Deciding Equality Formulas by
Exploiting Positive Equality in a Logic of
|
|
15:30-16:00 | COFFEE | |
16:00-17:30 | Tool demonstrations
END OF CAV |
|
July 11 |
||
All Day:
Workshop CALCULEMUS:
Systems for Integrated
Workshop on Formal
Methods for Industrial
|
||
July 12 |
||
All Day:
Workshop CALCULEMUS:
Systems for Integrated
Workshop on Formal
Methods for Industrial
|