From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id B38657EE7A for ; Thu, 28 Mar 2013 17:59:58 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=pra; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=mailfrom; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@brightmail-internal4.sri.com) identity=helo; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="postmaster@brightmail-internal4.sri.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArMBAKx2VFGAElSFnGdsb2JhbABDDoMsv3IWDgEBAQEBCAsJCRQKHoIhBgEBbUUlD0+IJgy/FRWNNhYGhHgDiHiKKo82h2RfgUs X-IPAS-Result: ArMBAKx2VFGAElSFnGdsb2JhbABDDoMsv3IWDgEBAQEBCAsJCRQKHoIhBgEBbUUlD0+IJgy/FRWNNhYGhHgDiHiKKo82h2RfgUs X-IronPort-AV: E=Sophos;i="4.87,927,1363129200"; d="scan'208";a="10897015" Received: from brightmail-internal4.sri.com ([128.18.84.133]) by mail2-smtp-roc.national.inria.fr with ESMTP; 28 Mar 2013 17:59:56 +0100 X-AuditID: 80125485-b7fe46d000006efa-b5-5154770a1f9c Received: from mx0.csl.sri.com (mx0.csl.sri.com [130.107.1.30]) (using TLS with cipher AES256-SHA (AES256-SHA/256 bits)) (Client did not present a certificate) by brightmail-internal4.sri.com (SRI Internal SMTP Gateway) with SMTP id 01.F3.28410.A0774515; Thu, 28 Mar 2013 09:59:54 -0700 (PDT) Received: from ubi (ubi.csl.sri.com [130.107.15.8]) by mx0.csl.sri.com (8.14.3/8.14.2) with ESMTP id r2SGxnwR042363 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Thu, 28 Mar 2013 09:59:49 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.72) (envelope-from ) id 1ULGB3-0002XQ-00; Thu, 28 Mar 2013 09:59:49 -0700 To: acl2@utlists.utexas.edu, afsec@afsec.asr.cnrs.fr, amast@cs.utwente.nl, calculemus-ig@mathweb.org, caml-list@inria.fr, comlab@comlab.ox.ac.uk, concurrency@listserver.tue.nl, coq-club@pauillac.inria.fr, event@in.tu-clausthal.de, events@fmeurope.org, fmcad@utlists.utexas.edu, gdr-im@gdr-im.fr, hol-info@lists.sourceforge.net, lics@research.bell-labs.com, lprolog@cs.umn.edu, matita@cs.unibo.it, mizar-forum@mizar.uwb.edu.pl, prog-lang@diku.dk, pvs@csl.sri.com, qpq-general@qpq.org, sal@csl.sri.com, strqds@laas.fr, theorem-provers@ai.mit.edu, theory-logic@cs.cmu.edu, theorynt@listserv.nodak.edu, yices@csl.sri.com X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 Date: Thu, 28 Mar 2013 09:59:48 -0700 Message-ID: <9759.1364489988@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA+NgFmpmkeLIzCtJLcpLzFFi42JpymaU0+UqDwk0+PRZ1+LojpWMFnPWnGC1 uHE+z6Jh60FGi087NrBYfNi0j9Xi14VzrBbPZ65gtlj95QaTRf/NJ0Blfx8yW/Sf+sxu8eri bBaL7kMeFl/fTmO3+HLczWLF01/MFt2/ZS02v13BbvF12XxWi113lrFb7P5zEqj74ysmB3GP H11XWDw6TpR43Jxg57HgiI/HqYYFbB5T7jYxe/x4vZ7VY82E74wef3dGePybvIjFo2uysMek F4dYPGb+2MHosXvBZyaPKa8msnnc2dPCEiAWxWWTkpqTWZZapG+XwJXR2PSNsWCNRcWy3vIG xvv6XYycHBICJhIHpu9lg7DFJC7cWw9kc3EICaxikuicMZ8RwvnHKHHi71NmCGcGo8TijkVg GRGBQ6wSL1r2sIP0Cws4SUz6tJIdYpauxMdFM8FsFgFVic0TvzGC2LwCihKzz8wDs9mA7OZb C5knMHIvYGRYxSiTVJSZnlGSm5iZowuLEBO94qJMveT83E2MwKhpEApp3cG4Yo/hIUYBDkYl Ht4ZESGBQqyJZcWVuYcYJTiYlUR4m+KAQrwpiZVVqUX58UWlOanFhxilOViUxHm/mfP7Cwmk J5akZqemFqQWwWSZODilGhj1/z+T/yTF8mK3UHig4MzaSu9jPxX3Mx5gC0x9coRPUvvIQWGX t5fPaF465T2n/Aj3Ziu3D4ul9k2uOj6v8um5pRVSn8Sab/4/UX7kieXfm7+uqiXNkn1dskj+ YJi2wcTUmTLLcly4rmk4dayRiPnEdLKW5dDMtV1PHs2ddVnM6uy6Y7G7+bzYlFiKMxINtZiL ihMBDsZT/JYCAAA= Subject: [Caml-list] Third Summer School on Formal Techniques, May 20-24, 2013 Third Summer School on Formal Techniques May 20 - May 24, 2013 Menlo College, Atherton, CA http://fm.csl.sri.com/SSFT13 Follows VSTTE May 17-19 in the same location: https://sites.google.com/site/vstte2013/ Formal verification techniques such as model checking, satisfiability, and static analysis have matured rapidly in recent years. This school, the third in the series, will focus on the principles and practice of formal verification, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in using verification technology in their own research in computing as well as engineering, biology, and mathematics. Students at the school will have the opportunity to experiment with the tools and techniques presented in the lectures. The first Summer Formal school (SSFT11; http://fm.csl.sri.com/SSFT11) was held in May 2011 and the second (SSFT12; http://fm.csl.sri.com/SSFT12) was held in May 2012. We have NSF support for the travel and accommodation for students from US universities, but welcome applications from graduate students at non-US universities as well. Non-US students will have to cover their travel and lodging expenses (around $500). The deadline for applications is April 30. Non-US students requiring US visas are requested to apply early (by April 15). Interested students can submit their application at http://fm.csl.sri.com/SSFT13 The lectures at the school include: ================================================================== Title: Decision Methods for Arithmetic Lecturer: Leonardo de Moura, Microsoft Research Abstract: Decision methods for arithmetic are extensively used in the formal verification and analysis of software and cyber-physical systems, computer algebra, and formalized mathematics. In these talks, we will cover several decision methods for fragments of arithmetic such as the elementary theories of algebra and geometry over the Real and Complex numbers. We will also describe the general techniques used in the design of these procedures: saturation, model-based methods, abstract/refine loop, infinitesimals, etc. We assume only a basic grounding in first-order logic. ================================================================== Title: Advanced Theorem Proving Techniques in PVS with Applications Lecturer: Cesar Munoz, NASA Langley Research Center Hampton, VA 23681-2199, USA Abstract: The Prototype Verification System (PVS) [http://pvs.csl.sri.com] is an interactive environment for the specification and verification of systems. PVS provides a strongly typed specification language, which is based on Higher-Order Logic. The type system of PVS supports: sub-typing, dependent-types, abstract data types, parametric types, records, unions, and tuples. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This seminar will provide a gentle introduction to advanced PVS features, including types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. ================================================================== Title: Static and Dynamic Verification of Concurrent Programs Lecturer: Aarti Gupta, NEC Labs Abstract: The need to harness the computing power of modern multi-core platforms has driven a resurgence of interest in concurrent programs. However, it is very challenging to develop correct concurrent programs, and in practice programs often exhibit bugs related to subtle synchronization effects. These lectures will describe various static and dynamic techniques underlying automatic verification and debugging of concurrent programs. The emphasis will be on main ideas to reason about synchronizations and interleavings between interacting threads or processes. On the static side, we first review some theoretical results on model checking based on interacting pushdown system (PDS) models. Decidability results here limit the patterns of synchronization allowed. Next, we consider the practice of model checking concurrent programs, where the main challenge is in managing the explosion in interleavings. We consider both explicit and symbolic state space exploration, where various techniques are inspired by successful verification of finite state systems on one hand, and sequential programs on the other. Due to scalability limitations of static verification, there has been increased interest in dynamic techniques for systematically exploring (parts of) concurrent programs. We discuss preemptive context bounding techniques that control the scheduler to dynamically explore other interleavings. We also consider predictive analysis techniques, where a trace-based model derived from dynamic executions is used to predict concurrency bugs. ================================================================== Title: Program verification and synthesis as Horn-like constraint solving Lecturer: Andrey Rybalchenko, TU Munich Abstract: First, we review how proving reachability and termination properties of transition systems, procedural programs, multi-threaded programs, and higher- order functional programs can be reduced to constraint solving for Horn-like constraints. This step will cover properties over program variables of scalar and array data types. Second, we show how universal and existential temporal properties can be proved using contraint-based setting equipped with existential quantification. Third, we present a reduction from reactive program synthesis to existentially quantified Horn-like constraints. Finally, we discuss adequate solving algorithms and tools. The material would cover/export syntax and semantics of Horn clauses over theory literals, basics of temporal proof rules for reasoning about programs, basics of CTL and synthesis together with deductive proof rules, bottom-up inference/ resolution of Horn clauses, Skolemization, abstraction, interpolation. ================================================================== Title: Verified Programming with VCC Speaker: Ernie Cohen Abstract: In the last few years it has become practical to write real-world code and prove that it meets its specifications. This course provides an introduction to the joys of verified programming using VCC, a deductive verifier for concurrent C code. ================================================================== Title: Speaking Logic Speaker: Natarajan Shankar, SRI International Abstract: Formal logic has become the lingua franca of computing. It is used for specifying digital systems, annotating programs with assertions, defining the semantics of programming languages, and proving or refuting claims about software or hardware systems. Familiarity with the language and methods of logic is a foundation for research into formal aspects of computing. This course covers the basics of logic focusing on the use of logic as a medium for formalization and proof.