Invited Talks †Beluga: programming with dependent types and higher-order data †Brigitte Pientka (McGill University, Canada) The logical framework LF provides an elegant foundation for specifying formal systems and proofs. In the past decade, LF technology has been highly successfully in verifying guarantees about the run-time behavior of mobile code and mechanizing meta-theory of programming languages. However, incorporating LF technology into functional programming to directly allow programmers to describe and reason about properties of programs from within the programming language itself has been a major challenge. In this talk, I will present Beluga, a dependently-typed functional programming environment which supports programming with data and proofs specified in the logical framework LF. I will first discuss some typical example programs written in Beluga, then describe the type-theoretic foundation based on contextual modal types, and finally highlight practical challenges regarding type reconstruction for dependently typed systems. Using Static Analysis to Detect Type Errors and Race Conditions in Erlang Programs †Kostis Sagonas (National Technical University of Athens, Greece) This invited talk will present the main techniques used in Dialyzer, a static analysis tool that automatically defects and reports to its user various kinds of software defects in large applications written in Erlang. As Erlang is a dynamically typed functional language, Dialyzer started as a tool to detect definite type errors using dataflow analysis and was subsequently extended with a component that statically detects discrepancies between success typings inferred by a constraint-based analysis and user-specified type contacts. Relatively recently, Dialyzer was enhanced with a precise and scalable analysis that automatically detects race conditions in concurrent programs and a component for finding violations in the use of Erlang behaviors. For more than five years now, Dialyzer has been part of the Erlang/OTP system and has been actively used by its community. We will discuss Dialyzer's design choices, report on interesting experiences from Dialyzer's uses, and distill the main lessons learned from using static analysis in large (open-source as well as commercial) code bases. Solving Constraint Satisfaction Problems with SAT Technology †Naoyuki Tamura (Kobe University, Japan) (Joint work with Tomoya Tanjo and Mutsunori Banbara) A Boolean Satisfiability Testing Problem (SAT) is a combinatorial problem to find a Boolean variable assignment which satisfies all given Boolean formulas. Recent performance improvement of SAT technologies makes SAT-based approaches applicable for solving large and practical combinatorial problems, such as planning, scheduling, hardware/software verification, and constraint satisfaction, Sugar is a SAT-based constraint solver based on a new encoding method called order encoding which was first used to encode job-shop scheduling problems by Crawford and Baker. In the order encoding, a comparison x<=a is encoded by a different Boolean variable for each integer variable x and integer value a. The Sugar solver shows a good performance for a wide variety of problems, and became the winner of the GLOBAL categories in 2008 and 2009 CSP solver competitions. The talk will provide an introduction to modern SAT solvers, SAT encodings, implementation techniques of the Sugar solver, and its performance evaluation. |