Sunday July 28th

All assigned slots
See also the by-session program

CAV #5: Symbolic Model Checking I (Aud. 1)
08:45  Introduction and Welcome
09:00  Barner, Geist, and Gringauze: Symbolic localization reduction with reconstruction layering and backtrackingCADE #5: SAT (Aud. 3)
09:00  Goldberg: Testing satisfiability of CNF formulas by computing a stable set of points

09:00-09:30: NLULP Welcome (Aud. 10)

09:30  Bryant, Lahiri, and Seshia: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions09:30  de la Tour: A note on symmetry heuristics in SEMNLULP #1: Invited talk (Aud. 10)
09:30  Bos: Generating speech recognition grammars with compositional semantics from unification grammars
10:00  Barner and Grumberg: Combining symmetry reduction and under-approximation for symbolic model checking10:00  Audemard, Bertoli, Cimatti, Kornilowicz, and Sebastiani: A SAT based approach for solving formulas over boolean and linear mathematical propositions


CAV #6: Abstraction and Refinement (Aud. 1)
11:00  Pnueli, Xu, and Zuck: Liveness with (0,1,infinity)-counter abstraction
CADE #6: Model generation (Aud. 3)
11:00  Ahrendt: Deductive search for errors in free data type specifications using model generation
NLULP #2: Formalisms (Aud. 10)
11:00  Daniels and Meurers: Improving the efficiency of parsing with discontinuous constituents
11:30  Chatterjee, Sivaraj, and Gopalakrishnan: Shared memory consistency protocol verification against weak memory models: refinement via model-checking11:30  Audemard and Benhamou: Reasoning by symmetry and function ordering in finite model generationCLPSE #1: Invited Talk (Aud. 8)
11:30  Bossche: Logic programming for software engineering
11:30  Erk and Kruijff: A constraint-programming approach to parsing with resource-sensitive categorial grammar
12:00  Godefroid and Jagadeesan: Automatic abstraction using generalized model checking12:00  Gramlich and Pichler: Algorithmic aspects of herbrand models represented by ground atoms with ground equations12:00  Fox, Lappin, and Pollard: First-order, Curry-typed logic for natural language semantics


CAV #7: Compositional Verification I (Aud. 1)
14:00  Baumgartner, Kuehlmann, and Abraham: Property checking via structural analysis
CADE #7 (Aud. 3)
Invited talk
14:00  Jackson: Simple logic, complex systems
CLPSE #2: Software Components (Aud. 8)
14:00  Dong, Alencar, and Cowan: Modeling and analysis of design component contracts in logic programming
NLULP #3: Semantics (Aud. 10)
14:00  Gawronska: Employing cognitive notions in multilingual summarization of news reports
14:30  Rajamani and Rehof: Conformance checking for models of asynchronous message passing software14:30  Lau and Ornaghi: A priori reasoning for component-based software development14:30  Amoia, Gardent, and Thater: Using set constraints to generate distinguishing descriptions
15:00  Flanagan, Qadeer, and Seshia: A modular checker for multithreaded programs15:00  Georgieva, Hustadt, and Schmidt: A new clausal class decidable by hyperresolution15:00  Gupta: A language-based approach to software engineering: Domain specific languages meet software components15:00  ten Cate and chieh Shan: Question answering: From partitions to Prolog


CAV #8: Timing Analysis (Aud. 1)
16:00  Yoneda, Kitai, and Myers: Automatic derivation of timing constraints by failure analysis
CADE #8: CASC (Aud. 3)
16:00  Weidenbach, Brahm, Hillenbrand, Keen, Theobalt, and Topic: SPASS version 2.0
CLPSE #3: Software Design and Analysis (Aud. 8)
16:00  Ferrer, Lorenzo, Ramos, Carsí, and Perez: Modeling dynamic aspects in architectures and multiagent systems
NLULP #4: Interpretation as deduction (Aud. 10)
16:00  Christiansen: Abductive language interpretation as bottom-up deduction
16:15  Schulz and Sutcliffe: System description: GrAnDe 1.0
16:30  Strichman, Seshia, and Bryant: Reducing linear inequalities to propositional formulas16:30  Colton: System description: The HR program for theorem generation16:30  Pelin, Pelin, Orlovsky, Miron, and Grinev: On the problem of creation of Prolog operating system

16:30-17:30: NLULP #5: Panel: the future of NLP and LP (Aud. 10)

16:45  Whalen, Schumann, and Fischer: AutoBayes/CC - combining program synthesis with automatic code certification - system description
17:00  Younes and Simmons: Probabilistic verification of descrete event systems using acceptance samplingCADE Herbrand award (Aud. 3)
17:00  Award ceremony
17:00  Pelin, Pelin, and Pelin: The problem of knowledge structurization and use during training and consultation
17:10  Stickel: Title TBA
CADE CASC (continued) (Aud. 3)
18:00  CASC results and discussion

19:30-22:00: CADE Conference dinner (Restaurant Luftkastellet)

20:00-22:00: NLULP NLULP Dinner (Restaurant TBA)