| August 9-11, 2004 |
| Uemura room, International Building |
| SRI International |
| Menlo Park, CA 94025 |
| U.S.A. |
The summer school aims at providing a focused in-depth overview of the latest research done in combination of decision procedures, with a strong preference towards practical applications and tools. The target audience includes academic and industry researchers in formal methods, graduate students in logic, computer science, and engineering, and anyone interested in combination of decision procedures.
| Time | Mon, Aug 9 | Tue, Aug 10 | Wed, Aug 11 | Thu, Aug 12 |
|---|---|---|---|---|
| 9:00-9:15 | Breakfast | Breakfast | Breakfast | Spill-Over Session |
| 9:15-10:30 | Cesare Tinelli | Vijay Ganesh | Ashish Tiwari | |
| 10:30-10:45 | Break | Break | Break | |
| 10:45-12:00 | Sava Krstic | Sava Krstic | Harald Ruess | |
| 12:00-1:15 | Lunch | Lunch | Lunch | |
| 1:15-2:30 | Rajeev Joshi | Sergey Berezin | Clark Barrett | |
| 2:30-2:45 | Break | Break | Break | |
| 2:45-4:00 | Cesare Tinelli | Vijay Ganesh | Ashish Tiwari | |
| 4:00-4:15 | Break | Break | Break | |
| 4:15-5:30 | Leonardo De Moura | Sanjit Seshia and Shuvendu Lahiri | Harald Ruess | |
| 5:30-5:45 |
| Cesare Tinelli | University of Iowa | Nelson-Oppen combinations, latest advances including non-disjoint signatures, deterministic and non-deterministic algorithms, fusion methods. |
| Clark Barrett | New York University | CVC Lite + HOL light; Non-clausal decision heuristic; Partial functions. |
| Ashish Tiwari | SRI International | Decision procedure for congruence closure, extensions, combinations with other decision procedures, polynomial rings, Grobner basis, quantifier elimination. |
| Sergey Berezin | Stanford University | CVC Lite: An Efficient Theorem Prover Based on Combination of Decision Procedures |
| Leonardo De Moura | SRI International | ICS tool |
| Sanjit Seshia and Shuvendu Lahiri | CMU | UCLID: Deciding Combinations of Theories via Eager Translation to SAT |
| Rajeev Joshi | JPL | Verifun: A Theorem Prover Using Lazy Proof Explication |
| Sava Krstic | Intel | Strategies for combining decision procedures, generalizing Nelson-Oppen and Shostak methods. |
| Harald Ruess | SRI International | Modularity and Refinement of Inference Systems for Equality |
| Vijay Ganesh | Stanford University | Combination results for many-sorted theories with overlapping signatures |
| Marco Maratea | University of Genova, Italy | TSAT++ theorem prover |
| Byron Cook | Microsoft Research | Zapato/ZAP theorem provers |
| Sumit Gulwani | UC Berkeley | Randomized join algorithms for linear arithmetic and uninterpreted functions |
Registration is done by email: summerschool2004@verify.stanford.edu.
Please send your name and affiliation. If you have any dietary restrictions or other special needs, please let us know. A small registration fee (about $60 USD, to cover food services and conference room) will be accepted at the registration desk in cash (sorry, no credit cards).
Student registration is free, thanks to our sponsors.
The summer school will be held in the heart of the Silicon Valley at SRI International, one of the most well-known research institutes in the United States.
SRI International is located near downtown Menlo Park with plenty of restaurants, speciality stores, and other sights of interest. Stanford University is within 10 min of driving distance. Other nearby attractions include San Francisco, Santa Cruz mountains and the Pacific ocean, which are easily reached within 1 hour.
See Location and Directions page for more information.
For those who are flying in, there are three major airports in the area:
Parking is free for visitors near the Building I at SRI (where the school will be held). See the Location page for more information.
| Menlo Park | ||
| Miles from SRI | Name and Address | Telephone |
|---|---|---|
| 0.6 | Menlo Park Inn, 1315 El Camino Real, Menlo Park, CA 94025 | +1 (650) 326-7530, +1 (800) 327-1315 |
| 1.2 | Mermaid Inn Motel, 727 El Camino Real, Menlo Park, CA 94025 | +1 (650) 323-9481 |
| Palo Alto | ||
| Miles from SRI | Name and Address | Telephone |
| 1.0 | Sheraton Palo Alto Hotel, 625 El Camino Real, Palo Alto, CA 94301 | +1 (650) 328-2800 |
| 4.8 | Motel 6, 4301 El Camino Real, Palo Alto, CA 94306 | +1 (650) 949-0833 |
| Vijay Ganesh, | Stanford University, | Hardware Verification Group |
| Sergey Berezin, | Stanford University | Hardware Verification Group |
| Henny Sipma, | Stanford University, | CS-Theory Group |
For more information about the school, please contact us at summerschool2004@verify.stanford.edu.
 |
Intel Corporation |
If you would like to become a sponsor, please contact us at summerschool2004@verify.stanford.edu.