Sandip Ray | 2 May 2011 18:27
Picon

CAV 2011 Call for Participation

[ Apologies if you receive more than one copy of this CFP.  Please 
  share it with students and colleagues who may be interested. ]

                   CALL FOR PARTICIPATION

 23rd International Conference on Computer Aided Verification (CAV 2011)
                Cliff Lodge, Snowbird, Utah, USA

HIGHLIGHTS OF CAV, JULY 16-20
. 35 regular papers, 20 tool papers, 4 invited talks, 4 tutorials
. Students may apply for NSF travel awards
. Four Invited Tutorials on July 16
. Details at  http://www.cs.utah.edu/cav2011

HIGHLIGHTS OF PRE-CAV WORKSHOPS, JULY 14-15
. NSV 2011:  The Fourth International Workshop on Numerical Software Verification 
. PDMC 2011: 10th International Workshop on Parallel and Distributed Methods in Verifications 
. EC2 2011:  The Fourth International Workshop on Exploiting Concurrency Efficiently and Correctly 
. FAC 2011:  Frontiers in Analog Circuit Synthesis and Verification 
. SMT 2011:  International Workshop on Satisfiability Modulo Theories, including SMT-COMP 
. SPIN 2011: 18th International SPIN Workshop on Model Checking of Software 
. FM-R 2011: Formal Methods for Robotics and Automation 
. PSY 2011:  Practical Synthesis for Concurrent Systems 

INVITED SPEAKERS
. Andy Chou, Coverity Inc., "Static Analysis Tools in Industry: Notes from the Front Line"
. Vigyan Singhal, Oski Technology Inc., "Deploying Formal in a Simulation World"
. Vikram Adve, Illinois, "Parallel Programming Should Be - and Can Be - Determinstic by Default
. Rolf Ernst, Univ of Braunschweig, "Analysis in Automotive Systems Design - a Rocky Ride to New Grounds"

(Continue reading)

Joe Hurd | 2 May 2011 19:44
Favicon
Gravatar

Call for Papers: Workshop on Automated Theory Engineering (Extended Deadline)

The scope of this workshop has a large overlap with interactive
theorem proving, and ITP systems are explicitly called out in the list
of topics. Apologies in advance if you receive multiple copies. -- Joe

=======================================================
Sorry for possible multiple copies of this announcement.
=======================================================

                   LAST CALL FOR PAPERS

                                 ATE-2011
                     CADE23 Workshop on
               Automated Theory Engineering
                           (31. July 2011)

             Extended Deadline: 6 May 2011
            http://www.nicta.com.au/ate2011/

GENERAL INFORMATION
 The first Workshop on Automated Theory Engineering will
 be held in July 2011 in Wroclaw. It is associated  with
 the 23th International Conference on Automated Deduction
 (CADE23).

SCOPE
 Theory engineering  means the development and mechanisation
 of mathematical axioms, definitions, theorems and inference
 procedures as needed to cover the essential concepts and
 analysis tasks of an application domain. It is essential for
 the  qualitative and quantitative modelling and  analysis of
(Continue reading)

Freek Wiedijk | 4 May 2011 15:20
Picon
Favicon

Call for Papers ACL2 2011


                          Call for Papers
 ACL2 2011: 10th International Workshop on the ACL2 Theorem Prover
                          and Its Applications
             3-4 November 2011, Austin, TX, USA
                 http://www.cs.ru.nl/~julien/acl2-11/

                            -----

Important dates
------------

Abstract submission: 13 June2011
Paper submission: 20 June 2011
Author notification: 25 July 2011
Final version: 02 September 2011

Scope of the workshop
------------------

ACL2 2011 is a major forum for the users of the ACL2 theorem proving
system to present research related to the ACL2 theorem prover and its
applications. ACL2 2011 is the tenth in the series of workshops, occurring
at approximately 18-month intervals. ACL2 is a state-of-the-art automated
reasoning system, the latest in the Boyer-Moore family of theorem provers,
for which its authors received the 2005 ACM Software Systems Award.
ACL2 2011 is planned as a two-day workshop to be held in Austin, TX, USA,
on 3-4 November 2011. ACL2 2011 is affiliated with FMCAD 2011, the
eleventh International Conference on Formal Methods in Computer Aided
Design (http://www.cs.utexas.edu/users/ragerdl/fmcad11/). In addition to paper
(Continue reading)

Freek Wiedijk | 4 May 2011 15:13
Picon
Favicon

Call for bids ITP 2012

It is time to begin the process of selecting a host for ITP 2012, the
International Conference on Interactive Theorem Proving.

Following tradition from TPHOLs, the hosts of the previous conference
(ITP 2011) are running the process. There are two phases: solicitation
of bids and voting. This message concerns the first phase. A
long-standing TPHOLs convention is that the conference should be held in
a continent different from the location of the previous meeting, and
therefore no bids to host ITP 2012 in Europe will be accepted. Based on
ITP and TPHOLs history, ITP 2012 will likely be held in July, August or
September.

Bids should be sent to itp2011 <at> easychair.org and should include at least
the following information:

- name and email address of a contact person
- names of other people involved
- address of website for the bid
- approximate dates of the conference
- structure (e.g., k workshop days and n days of presentations followed
  by excursion...)
- advantages of the proposed venue

An example of a previous winning bid is here:

http://itp2011.cs.ru.nl/ITP2011/Bid_ITP11.html

Deadline for all bids is Monday, 30 May 2011. Shortly after that, the
bids will be made public and the voting phase will take place.  The
people eligible to vote are those who are seriously thinking of
(Continue reading)

Tom Ridge | 6 May 2011 15:48

Opportunities to study for a PhD in Computer Science

Dear All,

The University of Leicester has 7 PhD studentships available in
computer science (broadly theoretical computer science) including
automated theorem proving and related topics.

The studentships include one sponsored by Microsoft Research.

Further details can be found eg on my website:

http://www.cs.le.ac.uk/~tr61/

If you know of anyone who would be interested, please encourage them
to apply. The closing date is May 15th.

Thanks

Tom

------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
Havelund, Klaus (318M | 6 May 2011 05:16
Picon
Picon
Favicon

[fm-announcements] RV 2011 - call for papers + tutorial and tool demo proposals


International Conference on Runtime Verification (RV 2011)
September 27 - 30, 2011
San Francisco, California, USA
at the Historic Fairmont Hotel

http://rv2011.eecs.berkeley.edu/

Runtime verification (RV) is concerned with monitoring and
analysis of software or hardware system executions. The field is
often referred to under different names, such as runtime
verification, runtime monitoring, runtime checking, runtime
reflection, runtime analysis, dynamic analysis, runtime symbolic
analysis, trace analysis, log file analysis, etc. RV can be used
for many purposes, such as security or safety policy monitoring,
debugging, testing, verification, validation, profiling, fault
protection, behavior modification (e.g., recovery), etc. A
running system can be abstractly regarded as a generator of
execution traces, i.e., sequences of relevant states or
events. Traces can be processed in various ways, e.g., checked
against formal specifications, analyzed with special algorithms,
visualized, etc. Topics of interest include, but are not limited
to:

* program instrumentation techniques
* specification languages for writing monitors
* dynamic program slicing
* record-and-replay
* trace simplification for debugging
* extraction of monitors from specifications
* APIs for writing monitors
* programming language constructs for monitoring
* model-based monitoring and reconfiguration
* the use of aspect oriented programming for dynamic analysis
* algorithmic solutions to minimize runtime monitoring impact
* combination of static and dynamic analysis
* full program verification based on runtime verification
* intrusion detection, security policies, policy enforcement
* log file analysis
* model-based test oracles
* observation-based debugging techniques
* fault detection and recovery
* model-based integrated health management and diagnosis
* program steering and adaptation
* dynamic concurrency analysis
* dynamic specification mining
* metrics and statistical information gathered during runtime
* program execution visualization
* data structure repair for error recovery
* parallel algorithms for efficient monitoring
* monitoring for effective fault localization and program repair

The RV series of events started in 2001, as an annual workshop.
The RV'01 to RV'05 proceedings were published in ENTCS. Since
2006, the RV proceedings have been published in LNCS. In year
2010, RV became an international conference. Links to past RV
events can be found at the permanent URL:

   http://runtime-verification.org


INVITED SPEAKERS

Dawson Engler, Stanford University
   Title: "Making finite verification of raw C code easier than writing a
test case"

Cormac Flanagan, University of California, Santa Cruz
   Title: "Efficient and Precise Dynamic Detection of Destructive Races"

Wolfgang Grieskamp, Google
   Title: "Utilizing Protocol Contracts for Verifying Services in the
Cloud"

Sharad Malik, Princeton University
   Title: "Runtime Verification: A Computer Architecture Perspective"

Vern Paxson, University of California, Berkeley
   Title: "Approaches and Challenges for Detecting Network Attacks in Real-Time"

Steven P. Reiss, Brown University
   Title: "What is My Program Doing? Program Dynamics in Programmer's Terms"


PAPER SUBMISSION

RV will have two research paper categories: regular and short
papers. Papers in both categories will be reviewed by the
conference Program Committee.

* Regular papers (up to 15 pages) should present original
unpublished results. Applications of runtime verification are
particularly welcome. A Best Paper Award (USD 300) will be
offered.

* Short papers (up to 5 pages) may present novel but not
necessarily thoroughly worked out ideas, for example emerging
runtime verification techniques and applications, or techniques
and applications that establish relationships between runtime
verification and other domains. Accepted short papers will be
presented in special short talk (5-10 minutes) and poster
sessions.

In addition to short and regular papers, proposals for tutorials
and tool demonstrations are welcome. Proposals should be up to 2
pages long.

* Tutorial proposals on any of the topics above, as well as on
topics at the boundary between RV and other domains, are
welcome. Accepted tutorials will be allocated up to 15 pages
in the conference proceedings. Tutorial presentations will be
at least 2 hours.

* Tool demonstration proposals should briefly introduce the
problem solved by the tool and give the outline of the
demonstration. Tool papers will be allocated 5 pages in the
conference proceedings. A Best Tool Award (USD 200) will be
offered. Submitted tutorial and tool demonstration proposals
will be evaluated by the corresponding chairs, with the help of
selected reviewers.

All accepted papers, including tutorial and tool papers, will
appear in the LNCS proceedings. Submitted papers must use the
LNCS style. At least one author of each accepted paper must
attend RV'11 to present the paper. Papers must be submitted
electronically using the EasyChair system. A link to the
electronic submission page will be made available on the RV'11
web page.


IMPORTANT DATES

June 5, 2011 - Submission of regular and short papers
June 12, 2011 - Submission of tutorial and tool demonstration proposals
July 24, 2011 - Notification for regular, short, and tool papers
August 21, 2011 - Submission of camera-ready versions of accepted papers
September 27-30, 2011 - RV 2011 Conference and tutorials


ORGANIZERS

Programme committee chairs:
Sarfraz Khurshid (University of Texas at Austin, USA)
Koushik Sen (University of California at Berkeley, USA)

Local organization chairs:
Jacob Burnim (University of California at Berkeley, USA)
Nicholas Jalbert (University of California at Berkeley, USA)


PROGRAM COMMITTEE

Howard Barringer (University of Manchester, UK)
Eric Bodden (Technical University Darmstadt, Germany)
Rance Cleaveland (University of Maryland, USA)
Mads Dam (Kungliga Tekniska högskolan, Sweden)
Brian Demsky (University of California at Irvine, USA)
Bernd Finkbeiner (Saarland University, Germany)
Cormac Flanagan (University of California at Santa Cruz, USA)
Patrice Godefroid (Microsoft Research Redmond, USA)
Jean Goubault-Larrecq (ENS Cachan, France)
Susanne Graf (Verimag, France)
Radu Grosu (State University of New York at Stony Brook, USA)
Lars Grunske (University of Kaiserslautern, Germany)
Aarti Gupta (NEC Laboratories America, USA)
Rajiv Gupta (University of California at Riverside, USA)
Klaus Havelund (NASA/JPL, USA)
Mats Heimdahl (University of Minnesota, USA)
Gerard Holzmann (NASA/JPL, USA)
Sarfraz Khurshid (University of Texas at Austin, USA) (co-chair)
Viktor Kuncak (École Polytechnique Fédérale De Lausanne, Switzerland)
Kim Larsen (Aalborg University, Denmark)
Martin Leucker (University of Luebeck, Germany)
Rupak Majumdar (Max Planck Institute Germany and University of California
at Los Angeles USA)
Greg Morrisett (Harvard University, USA)
Mayur Naik (Intel Berkeley Labs, USA)
Brian Nielsen (Aalborg University, Denmark)
Klaus Ostermann (University of Marburg, Germany)
Corina Pasareanu (NASA Ames, USA)
Wim De Pauw (IBM T. J. Watson, USA)
Doron Peled (Bar Ilan University, Israel)
Suzette Person (NASA Langley, USA)
Gilles Pokam (Intel, Santa Clara, USA)
Shaz Qadeer (Microsoft Research Redmond, USA)
Derek Rayside (University of Waterloo, Canada)
Grigore Rosu (University of Illinois at Urbana-Champaign, USA)
Wolfram Schulte (Microsoft Research Redmond, USA)
Manu Sridharan (IBM T. J. Watson, USA)
Koushik Sen (University of California, Berkeley, USA) (co-chair)
Peter Sestoft (IT University of Copenhagen, Denmark)
Scott Smolka (State University of New York at Stony Brook, USA)
Oleg Sokolsky (University of Pennsylvania, USA)
Mana Taghdiri (Karlsruhe Institute of Technology, Germany)
Serdar Tasiran (Koc University, Turkey)
Nikolai Tillmann (Microsoft Research Redmond, USA)
Shmuel Ur (Shmuel Ur Innovation, Israel)
Willem Visser (University of Stellenbosch, South Africa)
Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA)
Xiangyu Zhang (Purdue University, USA)


RV STEERING COMMITTEE

Howard Barringer (University of Manchester, UK)
Klaus Havelund (NASA/JPL, USA)
Gerard Holzmann (NASA/JPL, USA)
Insup Lee (University of Pennsylvania, USA)
Grigore Rosu (University of Illinois at Urbana-Champaign, USA)
Oleg Sokolsky (University of Pennsylvania, USA)

=====================================


------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Nadia Polikarpova | 6 May 2011 15:21
Picon

LASER summer school: Last call for participation

LASER Summer School on Software Engineering

Tools for Practical Software Verification
September 4-10, 2011 - Elba Island, Italy

http://laser.inf.ethz.ch/2011/

Application deadline: May 15th, 2011

Goals
---------

The LASER summer school, organized by the ETH Chair of Software 
Engineering, brings together the concepts and practice of software 
engineering in the idyllic setting of the Elba Island off the coast of 
Tuscany, easily reachable by air, car, bus or train.

The LASER school is intended for professionals from the industry 
(engineers and managers) as well as university researchers, including 
PhD students. Participants learn about the most important software 
technology advances from the pioneers in the field. The school's focus 
is applied, although theory is welcome to establish solid foundations. 
The format of the school favors extensive interaction between 
participants and speakers.

Topic and speakers
---------------------------

LASER 2011 is devoted to software verification tools. There have been 
great advances in the field of software verification in recent years. 
Today verification tools are being increasingly used not only by 
researchers, but by programming practitioners. The summer school will 
focus on several of the most prominent and practical of such tools from 
different areas of software verification (such as formal proofs, testing 
and model checking). During the school the participants will not only 
learn the principles behind the tools, but also get hands-on experience, 
trying the tools on real programs.

The speakers are among the most respected experts in the field:

- Edmund Clarke, Carnegie Mellon (involved in the development of SMV and 
CBMC model checkers);
- Patrick Cousot, Ecole normale superieure (ASTREE and THESEE static 
analysis tools);
- Patrice Godefroid, Microsoft Research (VeriSoft model checker, DART 
and SAGE testing tools);
- Rustan Leino, Microsoft Research (Boogie, Spec#, Dafny and Chalice 
program verifiers);
- Bertrand Meyer, ETH Zurich, organizer (AutoTest tool, Eiffel 
Verification Environment);
- Cesar Munoz, NASA Langley Research Center (PVS specification and 
verification system);
- Christine Paulin-Mohring, Universite Paris-Sud (Coq proof assistant);
- Andrei Voronkov, University of Manchester (Vampire theorem prover).

How to apply?
-------------------

Use the online registration form available on the LASER website 
http://laser.inf.ethz.ch/2011. Registration is open until May 15th, 
2011. The number of participants is strictly limited to ensure quality 
interaction with the lecturers and the rest of the audience. For more 
information, visit our website or contact the organizers: se-laser at 
lists.inf.ethz.ch

Venue
---------

The school takes place at the magnificent Hotel del Golfo 
(http://www.hoteldelgolfo.it/) in Golfo di Procchio, Elba. Along with an 
intensive scientific program, participants will have time to enjoy the 
natural and cultural riches of this history-laden jewel of the 
Mediterranean.

------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
Florian Rabe | 6 May 2011 14:06
Picon
Favicon

Call for Papers: 3rd Workshop on Modules and Libraries for Proof Assistants (affiliated with ITP 2011)

                      Third International Workshop on
	      Modules and Libraries for Proof Assistants
			      (MLPA'11)
	   http://kwarc.info/frabe/events/mlpa-11/index.html

		       Affiliated with ITP
             Nijmegen, The Netherlands, August 22-27, 2011

			   CALL FOR PAPERS

-----------------------------------------------------------------------

Submission deadline:    20 June 2011
Author Notification:     1 July 2011
Final Version:          11 July 2011
Workshop day:           26 August 2011

-----------------------------------------------------------------------

MLPA'11 is the third International Workshop on Modules and Libraries
for Proof Assistants. Previous meetings were held at CADE 2009 and at
FLoC 2010.

MLPA aims at bringing together researchers and practitioners with
background and experience in module systems from different logic-based
systems, such as theorem provers, proof assistants, and programming
languages. It will provide a fertile venue for the exchange of ideas and
experiences and has the potential to impact the way we organize proofs
and programs in the future.

We want to foster discussion of state-of-the-art results and techniques,
from theory and practice of module systems. This includes but is not limited
to:

* The design of module systems for programming languages and proof
  systems.

* System descriptions of existing module systems, for example ML
  modules, type classes, Coq's, Isabelle's, or Agda's module system.

* The implementation of formal digital libraries.

* Case studies regarding information retrieval, sharing, and
  management of change.

* Experience reports of industrial practitioners, using e.g., HOL,
  PVS, or other proof assistants.

Program Committee:

  * Gerwin Klein, NICTA
  * Dale Miller, INRIA
  * Brigitte Pientka, McGill University
  * Florian Rabe, Jacobs University Bremen (chair)
  * Claudio Sacerdoti Coen, University of Bologna
  * Carsten Schürmann, IT University of Copenhagen (chair)

Submission Categories:

* Category A: Detailed accounts of novel research - up to 15 pages.

* Category B: Abstracts and short descriptions of current work and
  proposed directions - up to 5 pages.

* Category C: System descriptions presenting an implemented tool and
  its features - up to 5 pages.

Shorter papers are welcome. Submission is electronic via easychair.
The submission site is
https://www.easychair.org/conferences/?conf=mlpa11

Proceedings are published informally and will be available to the
participants at the workshop. Formal post-proceedings will be
considered depending on the number and quality of submissions.

Authors of accepted papers are expected to present their work at
the workshop. System descriptions should be accompanied with a demo.

Organizers:

Florian Rabe                        Carsten Schuermann
f.rabe at jacobs-university.de      carsten at itu.dk
Jacobs University                   IT University of Copenhagen
Bremen, Germany		      	    Copenhagen, Denmark

------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
David L. Rager | 7 May 2011 20:18
Picon

Formal Methods in Computer Aided Design 2011 -- Final CFP


*************************************************************************** 
                             FMCAD 2011                                  
                FORMAL METHODS IN COMPUTER-AIDED DESIGN                  
                        FINAL CALL FOR PAPERS                           
*************************************************************************** 

FINAL CALL FOR PAPERS 
International Conference on Formal Methods in Computer-Aided Design 
http://www.fmcad.org

University of Texas at Austin, Texas, USA 
October 30 - November 2, 2011 

IMPORTANT DATES 

Abstract Submission: May 11 

Paper Submission: May 18 

Author Notification: July 15 

Final Version: August 5 

Conference: October 30 - November 2 

CONFERENCE SCOPE 

FMCAD 2011 is the eleventh in a series of conferences on the theory
and application of formal methods in hardware and system design and
verification. FMCAD provides a leading international forum to
researchers and practitioners in academia and industry for presenting
and discussing novel methods, technologies, theoretical results, and
tools for formal reasoning about computing systems, as well as open
challenges therein.

FMCAD is privileged to host invited presentations and tutorials from a
number of outstanding academic and industrial speakers:

 - Aaron Bradley, Assistant Professor at CU Boulder
 - Aarti Gupta, senior researcher at NEC
 - John Hughes, Professor at Chalmers University of Technology and CEO
   of QuviQ
 - J Moore, winner of the ACM System Award (2005), member of National
   Academy of Engineering, and ACM Fellow
 - Vigyan Singhal, President and CEO of Oski Technology Inc
 - Ivan Sutherland, Turing Award winner (1988)

ASSOCIATED WORKSHOPS AND COMPETITION

The following workshops are co-located with this year's conference:

 - The 10th International Workshop on the ACL2 Theorem Prover and Its
   Applications (http://www.cs.ru.nl/~julien/acl2-11/)

 - The Design and Implementation of Formal Tools and Systems workshop
   (http://www.nec-labs.com/research/system/systems_SAV-website/DIFTS11)

We are also proud to host this year's Hardware Model Checking
Competition (http://fmv.jku.at/hwmcc11).

TOPICS OF INTEREST 

Advances in model checking, theorem proving, equivalence checking,
abstraction and reduction techniques, compositional methods, automatic
decision procedures at the bit and word-level, probabilistic methods,
and combinations of deductive methods and decision procedures.

Topics related to the application of formal and semi-formal methods to
functional and non-functional specification and validation of hardware
and software. This includes timing and power modeling, and
verification of computing systems on all levels of abstraction.

System-level design and verification, especially for embedded systems,
HW/SW co-design and verification, and transaction-level verification.

Modeling and specification languages, formal semantics of known
languages or their subsets, model-based design, design derivation and
transformation, and correct-by-construction methods.

Experience with the application of formal and semi-formal methods to
industrial-scale designs. Tools that represent FV enablement, new
features, or a substantial improvement in the automation of FV
methods.

Application of formal methods in new areas. 

SUBMISSIONS 

Submissions must be made electronically in PDF format via EasyChair.
More details will be provided on the FMCAD web site. The proceedings
will be available online in the ACM Digital Library, at IEEE Xplore,
and as a free download from the FMCAD web site. Two categories of
papers can be submitted: regular papers (8 pages), containing original
research that has not been previously published, nor concurrently
submitted for publication; and short papers (4 pages), containing
emerging results or original ideas that can be described succinctly.

Regular and short papers must use the IEEE Transactions format on
letter-size paper with a 10-point font size, see
http://www.ieee.org/portal/pages/pubs/transactions/stylesheets.html.
Submissions must contain original research that has not been
previously published, nor concurrently submitted for publication. Any
partial overlap with any published or concurrently submitted paper
must be clearly indicated. If experimental results are reported,
authors are strongly encouraged to provide adequate access to their
data so that results can be independently verified.

A small number of accepted papers will be considered for a
distinguished paper award.

GENERAL CHAIRS 

Per Bjesse, Synopsys Inc., Hillsboro, USA 
Anna Slobodova, Centaur Technology, Austin, USA 

LOCAL ARRANGEMENTS 

David Rager, University of Texas at Austin, USA 

STEERING COMMITTEE 

Jason Baumgartner, IBM, USA 
Aarti Gupta, NEC Labs America, USA 
Warren Hunt, University of Texas at Austin, USA 
Panagiotis Manolios, Northeastern University, USA 
Mary Sheeran, Chalmers University of Technology, Sweden 

PROGRAM COMMITTEE 

Barbara Jobstmann (TUTORIALS CHAIR), VERIMAG, France 
Viktor Kuncak (PUBLICATION CHAIR), EPFL, Switzerland 
Nina Amla, NSF, USA 
Jason Baumgartner, IBM, USA 
Armin Biere, Johannes Kepler University, Austria 
Roderick Bloem, Graz University of Technology, Austria 
Gianpiero Cabodi, Politecnico di Torino, Italy 
Alessandro Cimatti, FBK-IRST, Italy 
Koen Claessen, Chalmers University of Technology, Sweden 
Rolf Drechsler, University of Bremen, Germany 
Bruno Dutertre, SRI, USA 
Ganesh Gopalakrishnan, University of Utah, USA 
Aarti Gupta, NEC Labs America, USA 
Alan Hu, University of British Columbia, Canada 
Rick Huang, National Taiwan University, Taiwan 
Kevin Jones, City University London, UK
Gerwin Klein, NICTA, Sydney, Australia 
Daniel Kroening, University of Oxford, UK 
Thomas Kropf, Robert Bosch GmbH, Germany 
Oded Maler, VERIMAG, France 
Panagiotis Manolios, Northeastern University, USA 
Ken McMillan, Microsoft Research, Seattle, USA 
Tom Melham, University of Oxford, UK 
Doron Peled, Bar Ilan University, Israel
Lee Pike, Galois, USA 
Kavita Ravi, Cadence, USA 
Sandip Ray, University of Texas at Austin, USA 
Julien Schmaltz, Open University of the Netherlands, The Netherlands 
Peter-Michael Seidel, AMD, USA
Natasha Sharygina, University of Lugano, Switzerland 
Satnam Singh, Microsoft Research, UK 
Sofiene Tahar, Concordia University, Montreal, Canada 
Murali Talupur, Intel, USA 
Helmut Veith, Vienna University of Technology, Austria
Karen Yorav, IBM, Israel 

------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
hao deng | 13 May 2011 09:11
Picon

hol-light , is this a bug of BETA_CONV

Hi, there:
    I'm a new user of hol-light and I find the following thing strange :

# BETA_CONV `(\x. ?y. x = a /\ y = b) y`;;
Warning: inventing type variables
val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b)

the ?y is not renamed in the substitution , is this a bug ?
or am I wrong at some where?

Thanks in advance.

------------------------------------------------------------------------------
Achieve unprecedented app performance and reliability
What every C/C++ and Fortran developer should know.
Learn how Intel has extended the reach of its next-generation tools
to help boost performance applications - inlcuding clusters.
http://p.sf.net/sfu/intel-dev2devmay

Gmane