*Invited Talks [#pde747cc]

**Brigitte Pientka (McGill University, Canada) [#x170a045]
''Beluga: programming with dependent types and higher-order data''
**Beluga: programming with dependent types and higher-order data [#g9b1735c]
''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.

**Kostis Sagonas (National Technical University of Athens, Greece) [#k9ba0d48]
''Using Static Analysis to Detect Type Errors and Race Conditions in Erlang Programs''
**Using Static Analysis to Detect Type Errors and Race Conditions in Erlang Programs [#a1282741]
''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.

**Naoyuki Tamura (Kobe University, Japan) [#vf16a29c]
''Solving Constraint Satisfaction Problems with SAT Technology''
**Solving Constraint Satisfaction Problems with SAT Technology [#h36d3351]
''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.

Front page   Diff Backup Reload   List of pages Search Recent changes   Help   RSS of recent changes