posted by user: hawblitz || 7939 views || tracked by 16 users: [display]

CPP 2012 : The Second International Conference on Certified Programs and Proofs

FacebookTwitterLinkedInGoogle

Link: http://cpp12.kuis.kyoto-u.ac.jp/
 
When Dec 13, 2012 - Dec 15, 2012
Where Kyoto, Japan
Abstract Registration Due Jun 8, 2012
Submission Deadline Jun 15, 2012
Notification Due Aug 27, 2012
Final Version Due Sep 17, 2012
Categories    computer science   verification   formal methods   security
 

Call For Papers

The Second International Conference on
Certified Programs and Proofs (CPP 2012)
CALL FOR PAPERS

Kyoto, Japan
December 13-15 2012
http://cpp12.kuis.kyoto-u.ac.jp/

co-located with APLAS 2012
http://aplas12.kuis.kyoto-u.ac.jp/

CPP is a new international forum on theoretical and practical topics
in all areas, including computer science, mathematics, and education,
that consider certification as an essential paradigm for their work.
Certification here means formal, mechanized verification of some sort,
preferably with production of independently checkable certificates.
We invite submissions on topics that fit under this rubric.

The first CPP conference was held in Kenting, Taiwan during December
7-9, 2011. As with the first meeting, the proceedings will be
published in Springer-Verlag's Lecture Notes in Computer Science
series.

Suggested, but not exclusive, specific topics of interest for
submissions include: certified or certifying programming, compilation,
linking, OS kernels, runtime systems, and security monitors; program
logics, type systems, and semantics for certified code; certified
decision procedures, mathematical libraries, and mathematical
theorems; proof assistants and proof theory; new languages and tools
for certified programming; program analysis, program verification, and
proof-carrying code; certified secure protocols and transactions;
certificates for decision procedures, including linear algebra,
polynomial systems, SAT, SMT, and unification in algebras of interest;
certificates for semi-decision procedures, including equality,
first-order logic, and higher-order unification; certificates for
program termination; logics for certifying concurrent and distributed
programs; higher-order logics, logical systems, separation logics, and
logics for security; teaching mathematics and computer science
with proof assistants; and "Proof Pearls" (elegant, concise, and
instructive examples).


IMPORTANT DATES:

Authors are required to submit a paper title and a short abstract
before submitting the full paper. The submission should include when
necessary a url where to find the formal development assessing the
essential aspects of the work. All submissions will be electronic.
All deadlines are at midnight (GMT).

Abstract Deadline: Friday, June 8, 2012
Paper Submission Deadline: Friday, June 15, 2012
Author Notification: Monday, August 27, 2012
Camera Ready: Monday, September 17, 2012
Conference: December 13-15, 2012

PROGRAM CO-CHAIRS:
Chris Hawblitzel (Microsoft Research Redmond)
Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique)

GENERAL CHAIR:
Jacques Garrigue (Nagoya University)

PROGRAM COMMITTEE:
Stefan Berghofer (Technical University Munich)
Wei-Ngan Chin (National University of Singapore)
Adam Chlipala (MIT)
Mike Dodds (University of Cambridge)
Amy Felty (University of Ottawa)
Xinyu Feng (University of Science and Technology of China)
Herman Geuvers (Radboud University, Nijmegen)
Robert Harper (Carnegie Mellon University)
Chris Hawblitzel (Microsoft Research Redmond)
Gerwin Klein (NICTA)
Laura Kovacs (Vienna University of Technology)
Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique)
Rupak Majumdar (UCLA, Max Planck Institute for Software Systems)
Lawrence Paulson (University of Cambridge)
Frank Piessens (KU Leuven)
Randy Pollack (Harvard and Edinburgh University)
Bow-Yaw Wang (Academia Sinica)
Santiago Zanella Béguelin (IMDEA Software Institute)

ORGANIZING COMMITTEE:
Jacques Garrigue and Atsushi Igarashi
Email: cpp2012oc@math.nagoya-u.ac.jp

CPP STEERING COMMITTEE:
Andrew Appel (Princeton University)
Nikolaj Bjørner (Microsoft Research Redmond)
Georges Gonthier (Microsoft Research Cambridge)
John Harrison (Intel Corporation)
Jean-Pierre Jouannaud (co-Chair) (INRIA and Tsinghua University)
Gerwin Klein (NICTA)
Tobias Nipkow (Technische Universität München)
Zhong Shao (co-Chair) (Yale University)


SUBMISSION INSTRUCTIONS:

Papers should be submitted electronically online via the conference
submission web page at URL:

http://www.easychair.org/conferences/?conf=cpp2012

Acceptable formats are PostScript or PDF, viewable by Ghostview or
Acrobat Reader. Submissions should not exceed 16 pages in LNCS format,
including bibliography and figures. Submitted papers will be judged on
the basis of significance, relevance, correctness, originality, and
clarity. They should clearly identify what has been accomplished and
why it is significant. The proceedings of the symposium will be
published as a volume in Springer-Verlag’s Lecture Notes in Computer
Science series.

Each submission must be written in English and provide sufficient
detail to allow the program committee to assess the merits of the
paper. It should begin with a succinct statement of the issues, a
summary of the main results, and a brief explanation of their
significance and relevance to the conference, all phrased for the
non-specialist. Technical and formal developments directed to the
specialist should follow. Whenever appropriate, the submission should
come along with a formal development, using whatever prover, e.g.,
Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS,
Vampire, etc. References and comparisons with related work should be
included. Papers not conforming to the above requirements concerning
format and length may be rejected without further consideration.

The results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other published conferences
or workshops. The PC chairs should be informed of closely related work
submitted to a conference or journal in advance of submission.
Original formal proofs of known results in mathematics or computer
science are among the targets. One author of each accepted paper is
expected to present it at the conference.

Related Resources

TAP 2024   18th International Conference on Tests and Proofs
IEEE COINS 2024   IEEE COINS 2024 - London, UK - July 29-31 - Hybrid (In-Person & Virtual)
ZKDAPPS 2024   1st IEEE International Workshop on Programmable Zero-Knowledge Proofs for Decentralized Applications
ACM-Ei/Scopus-CCISS 2024   2024 International Conference on Computing, Information Science and System (CCISS 2024)
CTISC 2024   2024 6th International Conference on Advances in Computer Technology, Information Science and Communications (CTISC 2024) -EI Compendex
GreeNet Symposium - SGNC 2024   15th Symposium on Green Networking and Computing (SGNC 2024)
CVIV 2024   2024 6th International Conference on Advances in Computer Vision, Image and Virtualization (CVIV 2024) -EI Compendex
IEEE ICA 2022   The 6th IEEE International Conference on Agents
MLANN 2024   2024 2nd Asia Conference on Machine Learning, Algorithms and Neural Networks (MLANN 2024)
ACM ICMLT 2024   ACM--2024 9th International Conference on Machine Learning Technologies (ICMLT 2024)