TOPICS

• Specification and verification of hardware: microprocessors, memory systems, buses, pipelines, etc; formal semantics of hardware design languages; synthesis; formal design flows.
• Specification and verification of software: program verification, refinement, and synthesis for functional, declarative and imperative languages; formal semantics of programming languages; proof carrying code.
• Industrial application of theorem provers.
• Advances in theorem prover technology: proof automation and decision procedures, induction, combination of deductive and algorithmic approaches, incorporation of theorem provers into larger systems, combination of theorem provers with other provers and tools.
• Other topics, including: security algorithms, properties, and policies; specification and requirements analysis of systems; user interfaces for theorem provers; development and extension of higher order logics; formalization of mathematical theories.
• Proof Pearls: concise and elegant presentations of interesting examples.

SUBMISSIONS

	Mature Work	Emerging Trends
Submission deadline	20 Feb 2004	31 May 2004
Acceptance notification	16 Apr 2004	18 June 2004
Camera-ready copy due	14 May 2004	16 July 2004

Submissions under Mature Work will be fully refereed, and the accepted papers will be published in a volume of Springer's Lecture Notes in Computer Science series, which will be available at the conference. Authors of accepted papers are expected to present their work at the conference.

Submissions under Emerging Trends will not be formally refereed, but their content and relevance will be reviewed. Those submissions accepted will be published in a University of Utah technical report, which will be available at the conference. Authors of accepted papers are expected to present a brief outline of their work at the conference and to prepare a poster for display at the conference venue. Unless otherwise requested, submissions rejected under Mature Work will also be considered for inclusion under Emerging Trends.

Papers should be no more than 16 pages in length and should be written using LaTeX2e and the LNCS style file. Submissions should be emailed directly to the organizers using the email address . This email address can also be used for any inquiries concerning the conference.

PROGRAM COMMITTEE

TPHOLs / tphols2004@cs.utah.edu