Call for Submissions to Workshops
			
		  Affiliated with
     The 20th International Conference on
	    Computer Aided Verification
		     CAV 2008
	http://www.princeton.edu/cav2008
.............................................................
Note: Not all workshops have open submissions.

FAC '08: 2nd Workshop on Formal Verification of Analog Circuits
---------------------------------------------------------------
*** Submission deadline: April 1st, 2008 ***
http://www.em.informatik.uni-frankfurt.de/FAC08.html
Organizers: Lars Hedrich and Oded Maler 

While formal verification has become part of the design process of
digital circuits, its application to analog and mixed-signal design is
still in its infancy. This is mainly due to the fact that the
mathematical models for such circuits are very different from the
discrete, finite-state transition systems that underlie verification of
digital systems. Such models are based on continuous dynamical systems
governed by differential equations and their verification calls for
different techniques, like those developed in the analysis of hybrid
systems. This workshop intends to bring together practitioners in
circuit design and in EDA tools together with researchers in
verification of discrete and hybrid systems in order to understand the
problems faced by designers of analog circuits and to see what support
can be provided by existing and new verification techniques.


AFM08: Automated Formal Methods
-------------------------------
http://fm.csl.sri.com/AFM08/
Organizers: Bruno Dutertre, Sam Owre, John Rushby, N. Shankar, Ashish
Tiwari

AFM functions both as a user's meeting for the SRI tools PVS, SAL, and
Yices, and as a general workshop for those interested in
state-of-the-art automation for formal methods.  The workshop will
include short tutorials on effective use of PVS, SAL, and Yices, as well
as contributed papers that report on applications, case studies, and
experiments, as well as fresh ideas for enhancing the scale and range of
automated formal methods.


BPR 2008: 1st International Workshop on Bit-Precise Reasoning
-------------------------------------------------------------
http://www.cs.ubc.ca/~babic/index_bpr.htm
Organizers: Domagoj Babic, Amit Goel

Bit-Precise Reasoning (BPR) is increasingly being used for the analysis
of hardware and software systems. The aim of the workshop is to bring
together researchers working on BPR with users of BPR. Relevant topics
include, but are not limited to: applications of BPR and case studies,
new decision procedures for bit-vector arithmetic, combinations with
other theories, theoretical results, novel implementation techniques, as
well as benchmarks and evaluation methodology.


(EC)^2: Exploiting Concurrency Efficiently and Correctly
--------------------------------------------------------
http://www.cs.utah.edu/ec2/
Rajeev Alur, Ganesh Gopalakrishnan, Vineet Kahlon, Stephen Siegel

(EC)^2 will bring together formal methods researchers with experts in
multicore architectures, programming languages, and concurrency
libraries. The two day-workshop will feature six invited talks and the
opportunity for participants to present position papers on issues such
as transactional memory, programming constructs for concurrency,
formalization of concurrency libraries, verification, and hardware
support for correctness. See the workshop website for submission
instructions and further details.


HAV 2008: Heap Analysis and Verification
----------------------------------------
http://research.microsoft.com/~jjb/HAV2008/index.html
Organizers: Josh Berdine, Mooly Sagiv

The Heap Analysis and Verification (HAV) 2008 workshop aims to bring
together researchers to exchange the latest, and develop new, ideas in
all aspects of formal analysis and verification for heap-manipulating
software.


NSV 2008: First International Workshop on Numerical Abstractions for
Software Verification
------------------------------------------------------------------------
----
http://theory.stanford.edu/~srirams/nsv/index.html
Organizers: Franjo Ivancic, Sriram Sankaranarayanan and Chao Wang

This workshop will focus on various issues related to the handling of
numerical operations in software verification. The workshop brings
together eight invited speakers who will present various techniques for
numerical reasoning in software, and their application to important
software verification problems for embedded systems such as safety,
termination, timing analysis and so on.


SMT 2008: Sixth International Workshop on Satisfiability Modulo Theories
------------------------------------------------------------------------
http://research.microsoft.com/conferences/SMT08/
Organizers: Clark Barrett, Leonardo de Moura

Determining the satisfiability of first-order formulas modulo background
theories, known as the Satisfiability Modulo Theories (SMT) problem, has
proved to be very useful in verification, compiler optimization,
scheduling, and other areas. The aim of the SMT workshop is to bring
together researchers working on SMT and users of SMT techniques.