CS Dept
Stanford University
Combination of Decision Procedures
Summer School 2004
| Home |
| Goals |
| Call for Participation |
| Program |
| Abstracts |
| Spill-Over Session (Thu, Aug 12) |
| Speakers |
| Registration |
| Logistics |
| Location |
| Directions |
| Contact Info |
| Sponsors: |
 |
| Intel Corporation |
| Acknowledgements |
| August 9-11, 2004 |
| Uemura room, International Building |
| SRI International |
| Menlo Park, CA 94025 |
| U.S.A. |
Goals
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.
Program
| 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 |
Speakers
| 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
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.
Logistics
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.
Transportation and parking
For those who are flying in, there are three major airports in the area:
- San Francisco International Airport (SFO)
- Mineta San José International Airport (SJC)
- Oakland International Airport (OAK)
Parking is free for visitors near the Building I at SRI (where the school will be held). See the Location page for more information.
Accomodation
The participants are expected to arrange for their own accomodation. Here are a few hotels and motels near SRI International, with many other possible options:| 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 |
Contact Information
| 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.
Sponsors
|
|
Intel Corporation |
If you would like to become a sponsor, please contact us at summerschool2004@verify.stanford.edu.