TPHOLs 2008 Emerging Trends Proceedings

August 18-21, Montreal, Canada

Proceedings

Papers

• Using Isabelle/HOL for Static Program Verification in JML4,
  Patrice Chalin, Perry R. James, George Karabotsos
• Theorem Proving based Framework for Verification of Group Key Protocols,
  Amjad Gawanmeh
• Probabilistic Analysis using Theorem Proving,
  Osman Hasan
• Checking the Satisfiability of XML-Specifications,
  Harald Hiss
• Reasoning with Powerdomains in Isabelle/HOLCF,
  Brian Huffman
• Shallow Dependency Pairs,
  Alexander Krauss
• A Reflexive Formalization of a SAT Solver in Coq,
  Stéphane Lescuyer, Sylvain Conchon
• Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle,
  Serguei Mokhov, Joey Paquet
• Verification of LISP Interpreters,
  Magnus O. Myreen
• Focus on Isabelle: From Specification to Verification,
  Maria Spichkova
• A Separation Logic Framework in HOL,
  Thomas Tuerk
• Implementing Secure Broadcast Ambients in Isabelle using Nominal Logic,
  Ayesha Yasmeen, Elsa Gunter

Authors

• Chalin, Patrice
• Conchon, Sylvain
• Gawanmeh, Amjad
• Gunter, Elsa
• Hasan, Osman
• Hiss, Harald
• Huffman, Brian
• James, Perry R.
• Karabotsos, George
• Krauss, Alexander
• Lescuyer, Stéphane
• Mokhov, Serguei
• Myreen, Magnus O.
• Paquet, Joey
• Spichkova, Maria
• Tuerk, Thomas
• Yasmeen, Ayesha