skip to content
 

Timetable (LAAW05)

Constraints and Verification

Monday 8th May 2006 to Friday 12th May 2006

Monday 8th May 2006
08:30 to 10:00 Registration
10:00 to 11:00 Z Manna (Stanford University)
From verification conditions to constraints
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 Solving verification constraint problems with constraint programming INI 1
12:30 to 13:30 Lunch at Churchill College
14:00 to 15:00 Program verification by parametric abstraction and semi-definite programming INI 1
15:00 to 15:30 Tea
15:30 to 16:00 Parameterized interfaces for open system verification of product lines INI 1
16:00 to 16:30 Polyhedral analysis of systems software INI 1
16:30 to 17:00 Proving termination of programs INI 1
17:30 to 18:30 Wine and Beer Reception
Tuesday 9th May 2006
09:00 to 10:00 Bounded and unbounded model checking with SAT INI 1
10:00 to 10:30 D Kroening ([ETH Zentrum])
Model checking C++ programs that use the STL
INI 1
10:30 to 11:00 K Namjoshi ([Bell Labs])
Incremental model checking
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 J Marques-Silva (University of Southampton)
Towards more efficient SAT-based model checking
INI 1
12:00 to 12:30 Uniform + supercompilation = verification INI 1
12:30 to 13:30 Lunch at Churchill College
14:00 to 15:00 Artifical Biochemistry INI 1
15:00 to 15:30 Tea
15:30 to 16:00 Generalizing BDD trees using minimal and/or graphs INI 1
16:00 to 16:30 Return of the JTMS: Preferences orchestrate conflict learning and solution synthesis INI 1
16:30 to 17:00 Enhancing software model checking with static program analysis INI 1
17:00 to 17:30 M Leconte ([ILOG SA])
State of the art in constraint programming solvers
INI 1
Wednesday 10th May 2006
09:00 to 10:00 Logic verification challenges in system level design at Intel INI 1
10:00 to 10:30 Constraints in hardware verification: some industrial perspectives INI 1
10:30 to 11:00 D Lugiez ([CMI])
Symbolic constraint solving for cryptographic protocols
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 Automatic refinement and vacuity detection for symbolic trajectory evaluation INI 1
12:30 to 13:30 Lunch at Churchill College
15:00 to 18:00 Cambridge Walking Tour
Thursday 11th May 2006
09:00 to 10:00 Linear constraints in probabilistic model checking INI 1
10:00 to 10:30 Time average games INI 1
10:30 to 11:00 O Maler (Verimag)
Controller synthesis with adversaries
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 P Abdullah ([Uppsala University])
Language inclusion for timed automata
INI 1
12:30 to 13:30 Lunch at Churchill College
14:00 to 15:00 Consequence generation, interpolants and invariant discovery INI 1
15:00 to 15:30 Tea
15:30 to 16:30 Y Naveh ([IBM Research Lab in Haifa])
Constraint satisfaction for random stimuli generation
INI 1
16:30 to 17:00 Verifying properties of well-founded linked lists INI 1
17:00 to 17:30 Reasoning about dynamic networks of counter systems INI 1
20:00 to 18:00 Conference Dinner in Dining Hall at Robinson College (Cash bar open from 19:30)
Friday 12th May 2006
09:00 to 10:00 On the use of automata for representing arithmetic constraints INI 1
10:00 to 10:30 Modelling with FO(ID); Solving with SAT INI 1
10:30 to 11:00 S Cotton (Verimag)
Satisfiability modulo theory chains with DPLL(T)
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 A progressive approach to solving satisfiability modulo theories (SMT) INI 1
12:30 to 13:30 Lunch at Churchill College
14:00 to 15:00 E Giunchiglia ([DIST - Universita di Genova])
State of the art in QBF reasoning, with emphasis on applications in FV
INI 1
15:00 to 15:30 Tea
15:30 to 16:30 Compact propositional encodings of first-order theories INI 1
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons