Organizers
Motivation
Topics
Program
Abstracts
Registration
Location
RISC, Castle of Hagenberg,
Austria
at ACA 2008
Important Dates
Early registration deadline:July, 7, 2008
The session will take place
on July 29 and 30, 2008
Contact
For further informations please send an e-mail toViorica Sofronie-Stokkermans
Program (Tuesday, July 29th)
11:30-12:00 Session 1: Combining deduction and symbolic computation
| 11:30-12:00 | Bruno Buchberger Automated Algorithm Synthesis in Theorema |
12:00-13:30 Lunch
13:30-14:30 Plenary Invited Talk
14:30-15:00 Coffee Break
15:00-16:30 Session 2: Constraint solving, QE and applications
16:30-17:00 Coffee Break
17:00-18:30 Session 3: Groebner bases and applications
| 17:00-17:30 | Masaaki Kanno Sum of Roots: a Review. |
| 17:30-18:00 | Naoyuki Shinohara
Parametric Polynomial Spectral Factorization by Comprehensive Groebner System |
| 18:00-18:30 | Yuki Watanabe (joint work with Naofumi Homma, Takafumi Aoki, and Tatsuo Higuchi) Formal Verification of VLSI Circuits Using Groebner Bases |
Program (Wednesday, July 30th)
9:00-10:30 Session 4: Constraint solving and quantifier elimination
10:30-11:00 Coffee Break
11:00-12:00 Session 5: Combining deduction and symbolic computation
| 11:00-11:30 | Ashish Tiwari Deductive Components of Analyzers for Dynamical Systems |
| 11:30-12:00 | Stefan Ratschan
The Role of Constraint Solving in the Verification of Hybrid Systems |
12:00-13:30 Lunch Break
13:30-14:30 Session 6: Linear arithmetic and resolution in verification
| 13:30-14:00 | Armin Biere (joint work with Toni Jussila) Linear Algebra, Boolean Rings and Resolution? |
| 14:00-14:30 | Evgeny Kruglov (joint work with Ernst Althaus and Christoph Weidenbach) Superposition Modulo Linear Arithmetic |
14:30-15:00 Coffee Break
15:00-16:30 Session 7: Combining symbolic computation and deduction for verification
| 15:00-15:30 | Tino Teige (joint work with Andreas Eggers, Martin Fränzle, Christian Herde, Holger Hermanns, Stefan Ratschan, and Tobias Schubert) Constraint-based Modeling and Verification of Hybrid Systems |
| 15:30-16:00 | Uwe Waldmann (joint work with Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, and Boris Wirtz) State Set Representations for Model Checking of Hybrid Systems with Large Discrete State Space |
| 16:00-16:30 | Viorica Sofronie-Stokkermans (joint work with Carsten Ihlemann and Swen Jacobs) Combining deduction in complex theories with quantifier elimination for the verification of parametric systems |
16:30-17:00 Coffee Break
17:00-17:50 Session 8: Combining symbolic computation and deduction
| 17:00-17:30 | Tudor Jebelean (joint work with Adrian Craciun, Madalina Hodorog and Robert Vajda) Systematic Exploration of Mathematical Theories |
| 17:30-17:50 | Session organizers Concluding remarks |