Workshop Programme
for period 8-12 May
Constraints and Verification
8-12 May
Timetable
| Monday 08 May | ||
| 08:30-10:00 | Registration | LAA |
| 10:00-11:00 | Manna, Z (Stanford University) | LAA |
| From verification conditions to constraints | Sem 1 | |
| 11:00-11:30 | Coffee | LAA |
| 11:30-12:00 | Bradley, A (Stanford University) | LAA |
| Solving verification constraint problems with constraint programming | Sem 1 | |
| 12:30-13:30 | Lunch at Churchill College | LAA |
| 14:00-15:00 | Cousot, P (ENS-DI) | LAA |
| Program verification by parametric abstraction and semi-definite programming | Sem 1 | |
| 15:00-15:30 | Tea | LAA |
| 15:30-16:00 | Fisler, K (Worcester Polytechnic Institute) | LAA |
| Parameterized interfaces for open system verification of product lines | Sem 1 | |
| 16:00-16:30 | Sankaranarayanan, S (NEC Labs America) | LAA |
| Polyhedral analysis of systems software | Sem 1 | |
| 16:30-17:00 | Cook, B (Microsoft Research Cambridge) | LAA |
| Proving termination of programs | Sem 1 | |
| 17:30-18:30 | Wine and Beer Reception | LAA |
| Wednesday 10 May | ||
| 09:00-10:00 | Hanna, Z (Intel Corp) | LAA |
| Logic verification challenges in system level design at Intel | Sem 1 | |
| 10:00-10:30 | Havlicek, J (Freescale Inc) | LAA |
| Constraints in hardware verification: some industrial perspectives | Sem 1 | |
| 10:30-11:00 | Lugiez, D (CMI) | LAA |
| Symbolic constraint solving for cryptographic protocols | Sem 1 | |
| 11:00-11:30 | Coffee | LAA |
| 11:30-12:00 | Grumberg, OG (Technion) | LAA |
| Automatic refinement and vacuity detection for symbolic trajectory evaluation | Sem 1 | |
| 12:30-13:30 | Lunch at Churchill College | LAA |
| 15:00-18:00 | Cambridge Walking Tour | LAA |
| Thursday 11 May | ||
| 09:00-10:00 | Kwiatkowska, MZ (University of Birmingham) | LAA |
| Linear constraints in probabilistic model checking | Sem 1 | |
| 10:00-10:30 | Jurdzinski, M (University of Warwick) | LAA |
| Time average games | Sem 1 | |
| 10:30-11:00 | Maler, O (Verimag) | LAA |
| Controller synthesis with adversaries | Sem 1 | |
| 11:00-11:30 | Coffee | LAA |
| 11:30-12:00 | Abdullah, P (Uppsala University ) | LAA |
| Language inclusion for timed automata | Sem 1 | |
| 12:30-13:30 | Lunch at Churchill College | LAA |
| 14:00-15:00 | McMillan, K (Cadence Berkeley Labs) | LAA |
| Consequence generation, interpolants and invariant discovery | Sem 1 | |
| 15:00-15:30 | Tea | LAA |
| 15:30-16:30 | Naveh, Y (IBM research Lab in Haifa) | LAA |
| Constraint satisfaction for random stimuli generation | Sem 1 | |
| 16:30-17:00 | Qadeer, S (Microsoft Research) | LAA |
| Verifying properties of well-founded linked lists | Sem 1 | |
| 17:00-17:30 | Bouajjani, A (Paris 7) | LAA |
| Reasoning about dynamic networks of counter systems | Sem 1 | |
| 20:00-18:00 | Conference Dinner in Dining Hall at Robinson College (Cash bar open from 19:30) | LAA |
| Friday 12 May | ||
| 09:00-10:00 | Wolper, P (Universite de Liege) | LAA |
| On the use of automata for representing arithmetic constraints | Sem 1 | |
| 10:00-10:30 | Mitchell, D (Simon Fraser University) | LAA |
| Modelling with FO(ID); Solving with SAT | Sem 1 | |
| 10:30-11:00 | Cotton, S (Verimag) | LAA |
| Satisfiability modulo theory chains with DPLL(T) | Sem 1 | |
| 11:00-11:30 | Coffee | LAA |
| 11:30-12:00 | Sakallah, K (University of Michigan) | LAA |
| A progressive approach to solving satisfiability modulo theories (SMT) | Sem 1 | |
| 12:30-13:30 | Lunch at Churchill College | LAA |
| 14:00-15:00 | Giunchiglia, E (DIST - Universita di Genova) | LAA |
| State of the art in QBF reasoning, with emphasis on applications in FV | Sem 1 | |
| 15:00-15:30 | Tea | LAA |
| 15:30-16:30 | Amir, E (University of Illinois) | LAA |
| Compact propositional encodings of first-order theories | Sem 1 | |
| Other Seminars |
|
Seminars in the University National and International Scientific Research Meetings |