Ciclo de actividades en Lenguajes de Programación y Análisis de Programas

David Van Horn y David Darais
12 Enero, 2016 - 15:00
Auditorio Ramón Picarte
PLEIAD - É. Tanter


Extendemos la invitación para asistir este 12, 13 y 14 de enero, al ciclo de actividades en Lenguajes de Programación y Análisis de Programas , según se detalla a continuación: 

Organiza: PLEIAD - É. Tanter
David Van Horn is professor at the University of Maryland. He works toward making the construction of reusable, trusted software components possible and effective. His research has spanned program analysis; semantics; verification and model-checking; security; logic; complexity; and algorithms.
David Darais is a PhD student at the University of Maryland, where he studies program analysis metatheory and formally verified programming. Most recently he has developed (with David Van Horn) Constructive Galois Connections and Mechanically Verified Calculational Abstract Interpretation, which solves the open problem of embedding Galois connections in a proof assistant.
Charla: Soft Contract Verification
David Van Horn
sala Auditorio Picarte (3er piso norte)
Martes 12 de Enero 

Abstract: Behavioural software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes significant overhead and delays discovery of faulty components to run-time. 

To overcome these issues, we present soft contract verification, which aims to statically prove either complete or partial contract correctness of components, written in an untyped, higher-order language with first-class contracts. Our approach uses higher-order symbolic execution, leveraging contracts as a source of symbolic values including unknown behavioral values, and employs an updatable heap of contract invariants to reason about flow-sensitive facts. We prove the symbolic execution soundly approximates the dynamic semantics and that verified programs can't be blamed. 

The approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of an off-the-shelf solver to decide problems without heavy encodings. The approach is competitive with a wide range of existing tools---including type systems, flow analyzers, and model checkers---on their own benchmarks.


Charla: Abstracting Gradual Typing: Mechanization in Agda
David Darais
Sala reunión Fundadores (3er piso norte)
Miercoles 13 de Enero

Abstract: Abstracting Gradual Typing (AGT) is an approach to systematically design gradual versions of static typing disciplines, by considering gradual types as an abstract representation of possible static types. Gradual typing is then a possible-typing analysis in presence of type imprecision. This talk presents work in progress in mechanizing the AGT approach in the Agda proof assistant. The crux of the mechanization addresses the issue of constructively dealing with the Galois connection that is at the heart of AGT.

Tutorial: Abstracting Abstract Machines in Redex

David Van Horn
Sala BP 319 (3er piso poniente)
Jueves 14 de Enero 
Part 1: 11:00-12:30
Part 2: 14:30-16:00

Abstract: This tutorial provides a brief introduction to the Redex programming language for semantic modeling. It does so by developing several semantic models of a simple programming language and then showing how to construct a program analyzer for this language using the “Abstracting Abstract Machines” method (Van Horn and Might, ICFP 2010).

So this tutorial aims to accomplish two goals:
• to introduce semantic engineers (programming language researchers, language designers and implementors, analysis and tool builders, etc.) to the Redex programming language;
• to demonstrate the method of building abstract interpreters known as AAM.

This tutorial serves either purpose. If you want to learn Redex, this tutorial will build a bunch of standard semantic systems: reduction relations, type judgments, evaluators, machines, and finally a program analyzer. If you want an explicit and approachable introduction to the AAM method, this tutorial will walk you through a detailed construction.