Skip to content

Workshop Programme

for period 8 - 12 May 2006

Constraints and Verification

8 - 12 May 2006


Monday 8 May
08:30-10:00 Registration
10:00-11:00 Manna, Z (Stanford University)
  From verification conditions to constraints Sem 1
11:00-11:30 Coffee
11:30-12:00 Bradley, A (Stanford University)
  Solving verification constraint problems with constraint programming Sem 1
12:30-13:30 Lunch at Churchill College
14:00-15:00 Cousot, P (ENS-DI)
  Program verification by parametric abstraction and semi-definite programming Sem 1
15:00-15:30 Tea
15:30-16:00 Fisler, K (Worcester Polytechnic Institute)
  Parameterized interfaces for open system verification of product lines Sem 1
16:00-16:30 Sankaranarayanan, S (NEC Labs America)
  Polyhedral analysis of systems software Sem 1
16:30-17:00 Cook, B (Microsoft Research Cambridge)
  Proving termination of programs Sem 1
17:30-18:30 Wine and Beer Reception
Tuesday 9 May
09:00-10:00 Clarke, E (Carnegie Mellon University)
  Bounded and unbounded model checking with SAT Sem 1
10:00-10:30 Kroening, D (ETH Zentrum)
  Model checking C++ programs that use the STL Sem 1
10:30-11:00 Namjoshi, K (Bell Labs)
  Incremental model checking Sem 1
11:00-11:30 Coffee
11:30-12:00 Marques-Silva, J (University of Southampton)
  Towards more efficient SAT-based model checking Sem 1
12:00-12:30 Lisitsa, A (Liverpool)
  Uniform + supercompilation = verification Sem 1
12:30-13:30 Lunch at Churchill College
14:00-15:00 Cardelli, L (Microsoft Research)
  Artifical Biochemistry Sem 1
15:00-15:30 Tea
15:30-16:00 Dechter, R (University of California)
  Generalizing BDD trees using minimal and/or graphs Sem 1
16:00-16:30 Junker, U (ILOG)
  Return of the JTMS: Preferences orchestrate conflict learning and solution synthesis Sem 1
16:30-17:00 Gupta, A (NEC Labs America)
  Enhancing software model checking with static program analysis Sem 1
17:00-17:30 Leconte, M (ILOG SA)
  State of the art in constraint programming solvers Sem 1
Wednesday 10 May
09:00-10:00 Hanna, Z (Intel Corp)
  Logic verification challenges in system level design at Intel Sem 1
10:00-10:30 Havlicek, J (Freescale Inc)
  Constraints in hardware verification: some industrial perspectives Sem 1
10:30-11:00 Lugiez, D (CMI)
  Symbolic constraint solving for cryptographic protocols Sem 1
11:00-11:30 Coffee
11:30-12:00 Grumberg, OG (Technion)
  Automatic refinement and vacuity detection for symbolic trajectory evaluation Sem 1
12:30-13:30 Lunch at Churchill College
15:00-18:00 Cambridge Walking Tour
Thursday 11 May
09:00-10:00 Kwiatkowska, MZ (University of Birmingham)
  Linear constraints in probabilistic model checking Sem 1
10:00-10:30 Jurdzinski, M (University of Warwick)
  Time average games Sem 1
10:30-11:00 Maler, O (Verimag)
  Controller synthesis with adversaries Sem 1
11:00-11:30 Coffee
11:30-12:00 Abdullah, P (Uppsala University)
  Language inclusion for timed automata Sem 1
12:30-13:30 Lunch at Churchill College
14:00-15:00 McMillan, K (Cadence Berkeley Labs)
  Consequence generation, interpolants and invariant discovery Sem 1
15:00-15:30 Tea
15:30-16:30 Naveh, Y (IBM research Lab in Haifa)
  Constraint satisfaction for random stimuli generation Sem 1
16:30-17:00 Qadeer, S (Microsoft Research)
  Verifying properties of well-founded linked lists Sem 1
17:00-17:30 Bouajjani, A (Paris 7)
  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)
Friday 12 May
09:00-10:00 Wolper, P (Universite de Liege)
  On the use of automata for representing arithmetic constraints Sem 1
10:00-10:30 Mitchell, D (Simon Fraser University)
  Modelling with FO(ID); Solving with SAT Sem 1
10:30-11:00 Cotton, S (Verimag)
  Satisfiability modulo theory chains with DPLL(T) Sem 1
11:00-11:30 Coffee
11:30-12:00 Sakallah, K (University of Michigan)
  A progressive approach to solving satisfiability modulo theories (SMT) Sem 1
12:30-13:30 Lunch at Churchill College
14:00-15:00 Giunchiglia, E (DIST - Universita di Genova)
  State of the art in QBF reasoning, with emphasis on applications in FV Sem 1
15:00-15:30 Tea
15:30-16:30 Amir, E (University of Illinois)
  Compact propositional encodings of first-order theories Sem 1

Back to top ∧