Journal of Automated Reasoning (JAR), Volume 41

Volume 41, Number 1, July 2008

• Xavier Leroy, Sandrine Blazy:
  Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. 1-31
  Electronic Edition (link) BibTeX
• Amine Chaieb, Tobias Nipkow:
  Proof Synthesis and Reflection for Linear Arithmetic. 33-59
  Electronic Edition (link) BibTeX
• Magdalena Ortiz, Diego Calvanese, Thomas Eiter:
  Data Complexity of Query Answering in Expressive Description Logics via Tableaux. 61-98
  Electronic Edition (link) BibTeX

Volume 41, Number 2, August 2008

• Volker Haarslev, Ralf Möller:
  On the Scalability of Description Logic Instance Retrieval. 99-142
  Electronic Edition (link) BibTeX
• André Platzer:
  Differential Dynamic Logic for Hybrid Systems. 143-189
  Electronic Edition (link) BibTeX

Volume 41, Numbers 3-4, November 2008

• Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow:
  Preface. 191-192
  Electronic Edition (link) BibTeX
• Hasan Amjad:
  Data Compression for Proof Replay. 193-218
  Electronic Edition (link) BibTeX
• Achim D. Brucker, Burkhart Wolff:
  An Extensible Encoding of Object-oriented Data Models in hol. 219-249
  Electronic Edition (link) BibTeX
• Alastair F. Donaldson, Alice Miller:
  Automatic Symmetry Detection for Promela. 251-293
  Electronic Edition (link) BibTeX
• Osman Hasan, Sofiène Tahar:
  Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. 295-323
  Electronic Edition (link) BibTeX
• Roberto Gorrieri, Fabio Martinelli, Marinella Petrocchi:
  Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks. 325-364
  Electronic Edition (link) BibTeX
• Nick Moffat, Michael Goldsmith:
  Assumption-Commitment Support for CSP Model Checking. 365-398
  Electronic Edition (link) BibTeX