[TYPES/announce] ACL2'14 Call for Participation

[Freek Verbeek]

       *** CALL FOR PARTICIPATION ***


                               ACL2 2014
          International Workshop on the ACL2 Theorem Prover
                         and its Applications

               July 12-13, 2014 in Vienna, Austria

                          *http://vsl2014.at/acl2/
<http://vsl2014.at/acl2/>*

                              CALL FOR PARTICIPATION

IMPORTANT DATES

  ACL2 workshop  12-13 July 2014   Early registration  8th June 2014
WORKSHOP SCOPE

The online registration for ACL2'14 has now been open for a few days,
see *http://vsl2014.at/registration/
<http://vsl2014.at/registration/>*
The early registration period ends June 8. The registration policy can be
found at *http://vsl2014.at/floc-ws/guide/
<http://vsl2014.at/floc-ws/guide/>*

ACL2 2014 is the major technical forum for users of the ACL2 theorem
proving system to present research related to the ACL2 theorem prover
and its applications. ACL2 2014 is the eleventh in the series of ACL2
workshops, which occur approximately every 18 months. ACL2 is an
industrial-strength automated reasoning system, the latest in the
Boyer-Moore family of theorem provers. The 2005 ACM Software System
Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2
and the other theorem provers in the Boyer-Moore family.

ACL2 2014 is a two-day workshop to be held in Vienna, Austria.
The workshop will feature technical papers and includes two invited talks:

Mike Gordon,"Linking ACL2 and HOL: past achievements and future prospects”

Magnus Myreen, "Machine-code verification: experience of tackling
medium-sized case studies using 'decompilation into logic’”

Furthermore, the workshop features rump sessions discussing ongoing
research. Topics include but are not limited to the
following:

    * software or hardware verification with ACL2,
    * formalizations of mathematics in ACL2,
    * new libraries, tools, and interfaces for ACL2,
    * novel uses of ACL2,
    * experiences with ACL2 in the classroom,
    * reports of and proposals for improvements of ACL2,
    * comparisons with other theorem provers,
    * comparisons with other programming or specification languages,
    * challenge problems and their solutions,
    * foundational issues related to ACL2, and
    * implementations connecting ACL2 with other systems.

The workshop will also feature ``rump sessions'', in which
participants can describe ongoing research related to ACL2. Proposals
for rump session presentations, including a title and short abstract,
will be accepted until the workshop.

ORGANIZATION

    Chairs

        * Freek Verbeek, Open University of The Netherlands
        * Julien Schmaltz, Eindhoven University of Technology, The
Netherlands

    Program Committee

        * John Cowles University of Wyoming
        * Warren Hunt University of Texas at Austin
        * Matt Kaufmann University of Texas at Austin
        * Panagiotis Manolios Northeastern University
        * Magnus O. Myreen University of Cambridge
        * Lee Pike Galois, Inc.
        * David Rager Oracle, Inc.
        * Sandip Ray Intel Corporation
        * Jose Luis Ruiz Reina University of Seville
        * David Russinoff Intel Corporation
        * Julien Schmaltz University of Technology, Eindhoven
        * Eric Smith Kestrel Institute
        * Sol Swords Centaur Technology, Inc.
        * Laurent Théry INRIA
        * Freek Verbeek Open University of The Netherlands
        * Makarius Wenzel Université Paris-Sud
        * Freek Wiedijk Radboud University Nijmegen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140604/c5dd3664/attachment.html>