------- Blind-Carbon-Copy To: Undisclosed Recipients <[email protected]> Subject: Third Summer School on Formal Techniques, May 20-24, 2013 (call for participation) X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 Date: Tue, 16 Apr 2013 00:39:20 -0700 Message-ID: <19908.1366097960@ubi> From: Sam Owre <owre@ubi>
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. ------- End of Blind-Carbon-Copy ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
