Volume 125, Number 1, March 2005

Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004)

• 
  Alessandro Armando, Luca Viganò: Preface. 1-
• 
  Simon N. Foley: Believing the Integrity of a System: (Invited Talk). 3-12
• 
  Mike Bond, Jolyon Clulow: Extending Security Protocol Analysis: New Challenges. 13-24
• 
  Hao Chen, John A. Clark, Jeremy L. Jacob: Synthesising Efficient and Effective Security Protocols. 25-41
• 
  Christopher Lynch, Catherine Meadows: On the Relative Soundness of the Free Algebra Model for Public Key Encryption. 43-54
• 
  Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: Deciding the Security of Protocols with Commuting Public Key Encryption. 55-66
• 
  Carlos Caleiro, Luca Viganò, David A. Basin: Metareasoning about Security Protocols using Distributed Temporal Logic. 67-89
• 
  Alessandro Armando, Luca Compagna: An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. 91-108
• 
  Laurent Mazaré: Satisfiability of Dolev-Yao Constraints. 109-124
• 
  Graham Steel, Alan Bundy: Attacking Group Multicast Key Management Protocols Using Coral. 125-144
• 
  Paul Hankes Drielsma, Sebastian Mödersheim: The ASW Protocol Revisited: A Unified View. 145-161

Volume 125, Number 2, March 2005

Proceedings of the 5th International Workshop on Strategies in Automated Deduction (Strategies 2004)

• 
  Maria Paola Bonacina, Thierry Boy de la Tour: Preface. 1-3
• 
  Bernhard Gramlich: Strategic Issues, Problems and Challenges in Inductive Theorem Proving. 5-43
• 
  Sayan Mitra, Myla Archer: PVS Strategies for Proving Abstraction Properties of Automata. 45-65
• 
  Andreas Meier, Erica Melis: Failure Reasoning in Multiple-Strategy Proof Planning. 67-90
• 
  Thierry Boy de la Tour, Prakash Countcham: An Isomorph-Free SEM-Like Enumeration of Models. 91-113
• 
  Tatjana Lutovac, James Harland: Issues in the Analysis of Proof-Search Strategies in Sequential Presentations of Logics. 115-147
• 
  Aaron Stump, Carsten Schürmann: Logical Semantics for the Rewriting Calculus. 149-164

Volume 125, Number 3, July 2005

• 
  Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli: Preface. 1-2
• 
  Clark Barrett, Jacob Donham: Combining SAT Methods with Non-Clausal Decision Heuristics. 3-12
• 
  Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill: A Practical Approach to Partial Functions in CVC Lite. 13-23
• 
  Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Massimo Idini, Marco Maratea: TSAT++: an Open Platform for Satisfiability Modulo Theories. 25-36
• 
  Pascal Fontaine, E. Pascal Gribomont: Combining Non-stably Infinite, Non-first Order Theories. 37-51
• 
  Robert Klapper, Aaron Stump: Validated Proof-Producing Decision Procedures. 53-68
• 
  Leonardo Mendonça de Moura, Harald Rueß, Natarajan Shankar: Justifying Equality. 69-85
• 
  Simon Colton, Alison Pease: The TM System for Repairing Non-Theorems. 87-101
• 
  Tjark Weber: Bounded Model Generation for Isabelle/HOL. 103-116
• 
  Didier Galmiche, Daniel Méry: Resource Graphs and Countermodels in Resource Logics. 117-135
• 
  Dominique Larchey-Wendling: Gödel-Dummett Counter-models through Matrix Computation. 137-148
• 
  Jian Zhang, Zhuo Huang: Reducing Symmetries to Generate Easier SAT Instances. 149-164