Skip to content

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
Tuesday 09 May
09:00-10:00 Clarke, E (Carnegie Mellon University) LAA
  Bounded and unbounded model checking with SAT Sem 1
10:00-10:30 Kroening, D (ETH Zentrum) LAA
  Model checking C++ programs that use the STL Sem 1
10:30-11:00 Namjoshi, K (Bell Labs) LAA
  Incremental model checking Sem 1
11:00-11:30 Coffee LAA
11:30-12:00 Marques-Silva, J (University of Southampton) LAA
  Towards more efficient SAT-based model checking Sem 1
12:00-12:30 Lisitsa, A (Liverpool) LAA
  Uniform + supercompilation = verification Sem 1
12:30-13:30 Lunch at Churchill College LAA
14:00-15:00 Cardelli, L (Microsoft Research) LAA
  Artifical Biochemistry Sem 1
15:00-15:30 Tea LAA
15:30-16:00 Dechter, R (University of California) LAA
  Generalizing BDD trees using minimal and/or graphs Sem 1
16:00-16:30 Junker, U (ILOG) LAA
  Return of the JTMS: Preferences orchestrate conflict learning and solution synthesis Sem 1
16:30-17:00 Gupta, A (NEC Labs America) LAA
  Enhancing software model checking with static program analysis Sem 1
17:00-17:30 Leconte, M (ILOG SA) LAA
  State of the art in constraint programming solvers Sem 1
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

Back to top ∧