The following is a list of workshops and tutorials to take place during CADE. See also schedule. Notice that some of the tutorials will take place during the main conference, not the first two workshop days.

• Workshop: Constraints in Formal Verification (CFV'05). Organizers: J. Marques-Silva, M. Velev.
• Workshop: Empirically Successful Classical AR (ESCAR). Organizers: G. Sutcliffe, S. Schulz, B. Fischer.
• Workshop: Non-Theorems, Non-Validity, Non-Provability (DISPROVING). Organizers: W. Ahrendt, P. Baumgartner, H. de Nivelle.
• Tutorial: Integrating Object-Oriented Design and Deductive Verification of Software (VERIFICATION OO) . Organizers: W. Ahrendt, B. Beckert, R. Hähnle, P. H. Schmitt.
• Tutorial: An Automatic Security Protocol Verifier based on Resolution Theorem Proving by B. Blanchet.
• Tutorial: Beyond SAT: QSAT, and SAT-based Decision Procedures by E. Giunchiglia.
• CASC. Organizers: G. Sutcliffe, C. Suttner.
• TPTP Tea Party. Organizers: G. Sutcliffe, J. Urban.

An Automatic Security Protocol Verifier based on Resolution Theorem Proving

We present a technique for the verification of cryptographic protocols, based on an abstract representation of the protocol by a set of Horn clauses, and on a resolution algorithm on these clauses. This technique allows a flexible encoding of many cryptographic primitives. It can verify a wide range of security properties of the protocols, such as secrecy, authenticity, and limited cases of process equivalences, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol, in parallel or not.

Beyond SAT: QSAT, and SAT-based Decision Procedures

The tutorial will start with a brief introduction to Propositional Satisfiability and then will concentrate on DLL-based decision procedures for Quantified Boolean Formulas (QBFs), separation logic and (time permitting) modal logic. For the QBFs satisfiability problem, the tutorial will focus on two topics: (1) the development of efficient solvers targeted to solving instances coming from real world applications, and (2) the empirical evaluation of QBF solvers and benchmarks. As for the other decision procedures, we will first give the main ideas underlying the SAT-based approach, and then focus on separation and modal logics.