
Announcing the winners of 2013
The three winners will each receive a gift from POPL, roughly, the
equivalent of an iPad mini.
Student Short Talk Session at POPL'13
Following prior years, POPL'13 will have two sessions devoted
entirely to short student talks, with a best talk award determined
by popular vote. All students attending POPL are strongly
encouraged to participate, and our goal is to allow as many
students as possible to present themselves and their work to the
community.
Suitable topics for short talks are descriptions of work in
progress, thesis projects, honours projects and relevant research
being or to be published elsewhere.
The best talk will be determined by popular vote and announced at
the end of POPL. Short presentations should fit in 10 minute slots
and we will have a few minutes after each slot for questions.
Submission instructions are found here:
We strive to give as many students as possible a chance to present
short talks at POPL'13. If we cannot accept all interested
participants due to space or time constraints, we will primarily
use seniority criteria rather than quality judgments to make
decision about participation, and favour students not already
presenting at POPL'13 or a colocated event over those who are.
Schedule
Session 1A (23/1 18:0019:00)
 Verification of Erlangstyle Concurrency, Emanuele D'Osualdo, University of Oxford, Department of Computer Science
[Show details]
This talk presents an approach for the fullyautomatic
program analysis and verification of Erlang modules. The
fragment of Erlang we consider includes the higherorder
functional constructs and all the key features of actor
concurrency, namely, dynamic and possibly unbounded
spawning of processes and asynchronous message
passing. We use a combination of static analysis and
infinitestate model checking to verify safety
properties specified by the user. Given an Erlang
program and a set of properties, our algorithm first
extracts an abstract (approximate but sound) model in
the form of an actor communicating system (ACS), and
then checks if the properties are satisfied using a
Petri net coverability checker, BFC. The prototype
implementation, called Soter and available at
mjolnir.cs.ox.ac.uk/soter, shows that in practice our
abstraction technique is accurate enough to verify an
interesting range of safety properties such as
mutualexclusion and boundedness of mailboxes.
View or download presentation ( PDF version)
 Constraintbased Static Analyses of Java Bytecode Programs, Durica Nikolic, University of Verona and MSR U Trento
[Show details]
We present the general idea of a parameterized formal framework for interprocedural static analyses of Java bytecode programs, based on abstract interpretation. The latter allows us to show, under hypotheses we characterize, the soundness of the analyses belonging to the framework. Our framework is capable of dealing with sideeffects and exceptional executions of invoked methods. Different instantiation of the parameters of our formal framework give rise to different static analyses. It is necessary to show, for each instantiation, that it satisfies the hypotheses mentioned above. This way, the general theory of the framework guarantees the soundness of the new analysis obtained from the instantiation. We introduce two static analyses formalized this way: Reachability Analysis of Program Variables and Definite Expression Aliasing Analysis, which have been also implemented in the static analyzer Julia and which improved the precision of its principal tools.
View or download presentation
 LargeScale SemanticsBased Code Analytics, Narcisa Andreea Milea, National University of Singapore, School of Computing
[Show details]
The volume of generated data in our world has been exploding. As costeffective solutions have emerged to handle the volume, velocity and variability of massive data, Big Data analytics has become widespread across industries. The exponential growth rate of repositories hosting source code and the increase in usage of external code in development and maintenance tasks also provide an opportunity and incentive to create novel Big code analytics solutions.
The focus of this work is a largescale semanticsbased code analytics solution that addresses the needs of developers and researchers in a uniform and scalable fashion. This raises a number of research questions regarding the semantic information extracted from code and the query language to express rich analyses. A number of works in the '90s focused on using program semantics to query code. Applying these techniques for large code bases, however, proved impractical either for the provider of the query engine, as often the code needed to be annotated with specifications or contracts, or the user, as the user had to specify too much. Current search engines (Koders, Krugle) ignore much of previous work and treat code as a bag of words which is queried using information retrieval techniques. This results in fast query times and a simple query language but supports only relatively simple questions. Finegrained information about structural relations between entities is not captured in these works, making it difficult to express complex analyses such as or finding code fragments that transform input type I to output type O.
Capturing finegrained structural data has its pros and cons. Specifically, it will allow for more varied analyses while requiring more storage space and access time. In order to address this challenge we will investigate new storage and indexing models and a multilevel tree and graph indexing scheme to support the analyses needed with high accuracy. The finegrained information we extract from code and use to answer a large number of queries is the structural information contained in Abstract Syntax Trees and Data Dependency Graphs. By also using coarse grained metadata such as textual information we enrich the graphs with semantic information thus obtaining multiple levels of detail data and supporting more analyses.
As preliminary experiments we have added support for handling code clone detection as an analysis in our framework. Clone detection has received considerable research interest due to applications in code refactoring, finding bugs or gaining insight into program design. In order to efficiently support this analysis our indexing model reduces subgraphs and subtrees to characteristic vectors and then to hashes. Preliminary results show good accuracy and scalability in answering clone queries.
To the best of our knowledge this is the first work that aims to
index finegrained structural information from ASTs and DDGs and
the first effort targeted towards big code bases with the aim of
unifying a large number of code analyses and queries.
View or download presentation
 ScanDal: Static Analyzer for Detecting Privacy Leaks, Yongho Yoon, Seoul National University
[Show details]
>
I'll present ScanDal, a static analyzer for detecting privacy
leaks in Android applications. We presented the previous version
of ScanDal at MoST, a workshop in conference IEEE Security &
Privacy. We improved the performance and precision of the
analyzer, and we adopted new activity lifecycle model. The number
of false alarms and analysis time both got decreased. I'll show
the progress and remaining works.
View or download presentation
 Efficient Verification of ProcessLocal Properties with Projections, Habib Saissi, Technische Universität Darmstadt
[Show details]
Verification of multiprocess programs remains a hard problem
where concurrency results in exponential growth of interleavings
to be verified. Thus improving verification efficiency naturally relates
to reducing the number of such interleavings. We achieve
this by decoupling across processes to verify processlocal properties.
Firstly, we characterize a nontrivial subset of all interleavings,
called projections, that preserve all reachable local states. Intuitively,
projections are sequences of processlocal transitions enhanced
with other interdependent transitions of other processes.
Secondly, we present an algorithm for the efficient exploration
of all projections. The proposed algorithm starts by optimistically
assuming that processes are independent from each other and it
launches processlocal exploration routines. In case a dependency
is discovered, the rest of the system is considered to reach new
local states. This procedure is repeated till no new dependencies
are found. Key to the achieved efficiency is that the algorithm utilizes
an asymmetric dependency relation. Finally, we show that our
reduction approach is fundamentally different from known partialorder
and symmetry reductions.
View or download presentation
Session 1B (23/1 18:0019:00)
 Synthesizing Binary Tree Operations from Specifications, Darya Kurilova, Carnegie Mellon University
[Show details]
As a part of my undergraduate program at the University
of Waterloo, I did a research project equivalent to an
undergraduate honours thesis. The project attempted to
bridge the gap between program specifications and the
implementation. The specific objective of the project
was to synthesize method implementations for a binary
tree data structure from its specifications. The
specification of a method is understood to include not
just pre and postconditions but also the invariants
and abstraction functions of the data structures on
which it operates. To generate the code, we applied SAT
solver based ``sketching'' techniques. In this talk, I
will present our approach and the results.
View or download presentation
 Synthesis of Randomized AccuracyAware Map/Fold Programs, Sasa Misailovic, MIT
[Show details]
Despite the fact that approximate computations have come to dominate
many areas of computer science, the field of program transformations has
focused almost exclusively on traditional semanticspreserving
transformations that do not attempt to exploit the opportunity,
available in many computations, to acceptably trade off accuracy for
benefits such as increased performance and reduced resource consumption.
We present a technique for synthesizing randomized map/fold computations
that trade accuracy for performance. Our technique takes as input (1) a
specification of an ideally accurate computation, consisting of as a set
of map tasks (which are continuous computations) and fold tasks, and (2)
a probabilistic specification of typical inputs of the computation. The
technique automatically synthesizes approximate implementations of map
and fold tasks (using polynomial interpolation and sampling) and
constructs expressions that characterize execution time and error
incurred by alternative implementations. The technique uses a
constrained optimizationbased approach to explore the space of
approximate computations that these transformations induce, and derives
an accuracy versus performance tradeoff curve that characterizes the
explored space. Each point on the curve corresponds to an approximate
randomized program configuration that realizes the probabilistic error
and time bounds associated with that point.
View or download presentation
 Synchronization Synthesis for SharedMemory Concurrent Programs, Roopsha Samanta, University of Texas at Austin
[Show details]
We present a framework that takes a concurrent program composed of
unsynchronized processes, along with a temporal specification of
their global concurrent behaviour, and automatically generates a
concurrent program with synchronization ensuring correct global
behaviour. Our methodology supports finitestate concurrent
programs composed of processes that may have local and shared
variables, may be straightline or branching programs, may be
ongoing or terminating, and may have programinitialized or
userinitialized variables. The specification language is an
extension of propositional Computation Tree Logic (CTL) that
enables easy specification of safety and liveness properties over
control and data variables.
View or download presentation
 Control ExplicitData Symbolic Model Checking, Petr Bauch, Masaryk University, Brno, Czech Republic
[Show details]
Modern computer programs challenge the verification community with
two distinct sources of nondeterminism. The dataflow component
(input variables) produces regular nondeterminism, which we can
capture using symbolic approaches, mainly by deciding
satisfiability of its logical representation. The controlflow
component (interleaving of parallel processes) produces
considerably less regular nondeterminism, and it seems that
explicit, enumerative approaches handle the controlflow component
more efficiently. However, complete verification  providing
evidence for correctness of every possible execution  requires
the verification procedure to handle efficiently both these types
of nondeterminism.
We combine the two approaches to formal verification, handling
data symbolically and control explicitly, in a process called
control explicitdata symbolic model checking. Explicit LTL
model checking forms the basis of the proposed procedure: the
execution transition system is traversed exhaustively, with every
execution inspected against the LTL behaviour
specification. Individual states of the transition system are
effectively sets of states, multistates containing one state for
every combination of input variable evaluations. Depending on what
firstorder theory is used to represent the multistates,
satisfiability of different properties of the multistates can be
decided.
Complete verification of parallel programs requires full Peano
arithmetic, which is undecidable for unbounded integers. Yet, a
decidable theory containing both addition and multiplication
exists; if the integers can be represented as bitvectors of fixed
size. The formulae in such a theory can be translated into
Propositional logic and decided using SAT solver, though the
translation may be exponential in size.
We hypothesise that the theory of bitvectors, together with
distributed explicit model checking, can support complete
verification of parallel software of substantial size: both
compared to present approaches and sufficient to realworld
application in specific domains. These domains include
safetycritical systems (where completeness is crucial) and unit
testing of parallel programs (where completeness might simplify
verification of difficult parts of the program). In order to
corroborate the hypothesis, we intend to build the proposed hybrid
model checker with the LLVM intermediate code as its input
language. Given that many languages can be translated into LLVM
(the most prominent among them being C++), if valid, our
hypothesis and the hybrid model checker will provide the industry
with a complete verification procedure that does not require
modelling the program.
As a first step, we have investigated the necessary changes on the
side of the model checker and what requirements must the symbolic
representation fulfil. Since, as mentioned above, the input
variables have to be bounded, the user should be allowed to
specify the bounds. Apart from the arithmetic operations and
assignments, the symbolic representation also has to support state
matching: decision whether two multistates represent the same
set. The reason is that state matching is required for accepting
cycle detection, the primary algorithm of LTL model
checking. Based on these requirements, we have implemented a
preliminary tools for hybrid model checking of Simulink diagrams
and reported a marked improvement compared to the purely explicit
approach.
View or download presentation
 Optimal and Heuristic Global Code Motion for Minimal Spilling, Gergö Barany, Vienna University of Technology
[Show details]
The interaction of register allocation and instruction scheduling is a wellstudied problem: Certain ways of arranging instructions within basic blocks reduce overlaps of live ranges, leading to the insertion of less costly spill code. However, there is little previous research on the extension of this problem to global code motion, i.e., the motion of instructions between blocks. We present an algorithm that models global code motion as an optimization problem with the goal to minimize overlaps between live ranges in order to minimize spill code.
Our approach analyzes the program to identify the live range overlaps for all possible placements of instructions in basic blocks, and all orderings of instructions within blocks. Using this information, we formulate an optimization problem to determine code motions and partial local schedules that minimize the overall cost of live range overlaps. We evaluate solutions of this optimization problem using integer linear programming, where feasible, and a simple greedy heuristic.
We conclude that performing global code motion with the sole goal of avoiding spills rarely leads to performance improvements because code is placed too conservatively. On the other hand, purely local optimal instruction scheduling for minimal spilling is effective at improving performance when compared to a heuristic scheduler for minimal register use.
View or download presentation
Session 2A (25/1 17:3018:30)
 A Theory of Agreement and Protection, Tiziana Cimoli, University of Cagliari, Sardinia, Italy
[Show details]
Contracts specify the behavior of software components,
from the point of view of the interactions they may
participate in, and the goals they try to reach. When
components are untrusted, it might realistically happen
that they agree on a contract, and later on behave
dishonestly, by not keeping the promises made.
In a contractoriented application, participants advertise their
contracts to some contract brokers and then they wait until the
contract broker finds an agreement. Agreement is a property of
contracts which guarantees that each honest participant may reach
her objectives, or that, at least, she may blame some other
participant. Things goes smooth if everyone is honest, but in the
case where the contract broker is dishonest, it may create a
fraudulent session, making participants interact in the absence of
an agreement. In this way, the contract broker may allow an
accomplice to swindle an unaware participant. Note that the
accomplice may perform his scam while adhering to his contract,
and so he will not be liable for violations.
A crucial problem is how to devise contracts which protect
participants from malicious contract brokers, while at the same
time allowing honest brokers to find agreements. A good contract
should allow a participant to reach her goals when the other
participants are cooperative, and it should protect her against
malicious participants.
We propose a foundational model for contracts.
We specify the behaviour of participants as event structures, a
basic semantic model for interactive systems. We then provide a
formal definition for the two key notions intuitively introduced
above, i.e. agreement and protection. To do that, we borrow
techniques from game theory, by interpreting contracts as
multiplayer concurrent games.
A participant agrees on a contract if she has a strategy to reach
her objectives (or make another participant chargeable for a
violation), whatever the moves of her adversaries.
A participant is protected by a contract when she has a strategy
to defend herself in all possible contexts, even in those where
she has not reached an agreement.
A first result is that agreement and protection cannot coexist for
a broad class of objectives. That is, if we are given the
objectives of a set of participants, it is impossible to construct
a contract which protects them all, and at the same time admits an
agreement.
To overcome this negative result, we extend event structures with
a new notion of causality called circular causality. While in
classical event structures an action a which causally depends on
an action b can only be performed after b, in our extension we
also consider a relaxed version of causality, which allows a to
happen before b, under the (legally binding) promise that b will
be eventually performed.
The main result of our work is that, using this model for
contracts, it is possible for a wide class of objectives to
construct a set of contracts which protect their participants and
still admit an agreement.
View or download presentation
 Fairness in Reactive Programming, Andrew Cave, McGill University
[Show details]
Linear temporal logic is commonly used in model checking to
express properties such as the fairness of schedulers. In this
talk I illustrate work in progress to give a proofsasprograms
interpretation of a constructive variant of linear temporal logic,
and demonstrate how the type system can guarantee properties such
as fairness.
View or download presentation
 A LatticeBased Approach to Deterministic Parallelism, Lindsey Kuper, Indiana University
[Show details]
Programs written using a deterministicbyconstruction model of
parallel computation always produce the same observable results,
offering programmers the promise of freedom from subtle,
hardtoreproduce nondeterministic bugs. A common theme that emerges
in the study of deterministicbyconstruction systems, from venerable
models like Kahn process networks to modern ones like Intel's
Concurrent Collections system, is that the determinism of the model
hinges on some notion of monotonicity.
Taking monotonicity as a guiding principle, then, Ryan Newton and I
are developing a new model for deterministicbyconstruction parallel
programming that generalizes existing singleassignment models. Our
model allows multiple assignments that are monotonically increasing
with respect to a userspecified lattice. We maintain determinism by
allowing only monotonically increasing writes and ""threshold"" reads of
shared data. The resulting model is provably deterministic and is
expressive enough to subsume diverse existing deterministic parallel
models, while also providing a solid theoretical foundation for
exploring controlled nondeterminism.
View or download presentation
 An Overview of Java Semantics Implementation in K Framework, Denis Bogdanas, Alexandru Ioan Cuza University of Iasi
[Show details]
The project Java semantics in K Framework aims to provide a complete executable semantics of Java language. Once completed, it will be used for reasoning about programs. At the moment of writing, Java 1.4 semantics is almost complete. The only unimplemented feature is inner classes. The presentation will be composed of three parts. Part 1 will provide some statistics about the project  the size of the code, number of rules, how it was developed and tested, and the overview of the K cells. The second part will describe the four basic steps of execution  three preprocessing steps and one actual execution step. It will also discuss the difference between the semantics approach and the classical compilation/execution paradigm. The third part will present some peculiarities of Java and how they were implemented in the semantics. In the end the presentation will highlight the projected applications.
View or download presentation
 Harnessing Performance for Flexibility in Instrumenting a Virtual Machine for JavaScript through Metacircularity, Erick Lavoie, Université de Montréal
[Show details]
Recent research and development on Virtual Machines (VMs), especially for the JavaScript (JS) language, has focused on performance at the expense of flexibility. Notably, it has hindered our understanding of the runtime behavior of programs by making instrumentation of existing VMs laborious. Past approaches required manual instrumentation of production interpreters, preventing the acquisition of longitudinal data because of the high cost associated with maintaining a modified VM over time.
In this presentation, we will show how it is possible to provide a flexible runtime instrumentation of the objectmodel and functioncalling protocol with a performance comparable to a stateoftheart interpreter, without having to modify the VM source code. Our approach consists in running a metacircular VM targeting the source language, based on a messagesending object model, on top of another fast VM. An overview of the implementation will be given and performance numbers will be presented.
View or download presentation
Session 2B (25/1 17:3018:30)
 Towards Complete Specifications with an Error Calculus, QuangLoc Le, National University of Singapore
[Show details]
We present an error calculus to support a novel specification
mechanism for sound and/or complete safety properties that are to
be given by users. With such specfications, our calculus can form
a foundation for both proving program safety and/or discovering
real bugs. The basis of our calculus is an algebra with a lattice
domain of four abstract statuses (namely unreachability, validity,
musterror and mayerror) on possible program states and four
operators for this domain to calculate suitable program status.We
show how proof search and error localization can be supported by
our calculus. Our calculus can also be extended to separation
logic with support for userdefined predicates and lemmas.We have
implemented our calculus in an automated verification tool for
pointerbased programs. Initial experiments have confirmed that it
can achieve the dual objectives, namely of safety proving and bugs
finding, with modest overheads.
View or download presentation
 Towards Noninterference in Composed Languages, Andreas Gampe, The University of Texas at San Antonio
[Show details]
As more personal information is entrusted to internetconnected software, ensuring that that software protects its users' privacy has become an increasingly pressing challenge. One mechanism that can be used to protect privacy is to require that software be certified with a secure type system. Protecting privacy with type systems, however, has only been studied for programs written entirely in a single language, whereas software is frequently implemented using multiple languages specialized for different tasks. A prominent example are embedded querying languages like SQL for relational databases and Javascript for NoSQL data sources.
We present an approach that facilitates reasoning over composed languages.
We outline sufficient requirements for the component languages, such that a generic theorem can lift privacy guarantees of the component languages to welltyped programs composed from parts in the various languages.
This significantly lowers the burden necessary to certify that such composite programs respect their users' privacy.
Our approach relies on computability.
We define security completeness, a form of completeness with respect to secure computations.
If a language is securitycomplete, we can then use a simulation argument to lift noninterference from components to the composed language.
Our apprach is based on the conjecture that any nontrivial securitytyped language is securitycomplete.
We formally establish conditions sufficient for a securitytyped language to be complete.
Our reasoning is based on securitylevel separability and typability of computations at a single security level.
While this allows us to show the conjecture for primitivetyped computations, it turns out that with more complex datatypes, the conjecture only holds with additonal constraints on the computation.
We demonstrate the applicability of the results with a case study of the work of Volpano et.al., FlowML and work of Banerjee & Naumann, three seminal securitytyped languages that are imperative, functional and objectoriented, respectively.
View or download presentation
 Reasoning about Relaxed Programs, Michael Carbin, MIT
[Show details]
Approximate program transformations such as loop perforation, multiple selectable implementations, approximate function memoization, and approximate data types produce programs that can execute at a variety of points in an underlying performance versus accuracy tradeoff space. Namely, these transformed programs trade accuracy of their results for increased performance by dynamically and nondeterministically modifying their execution.
We call such transformed programs relaxed programsthey have been extended with additional nondeterminism to relax their semantics and enable greater flexibility in their execution.
In this talk I will discuss our work in developing programming language constructs and a verification system to support to developing and verifying relaxed programs. Our work focuses on enabling developers to reason about the acceptability properties of their programs, which are the key correctness properties that enable them to have a wide range of acceptable behaviors. These properties include for example integrity properties, such as memory safety, and also accuracy properties which characterize bounds on the acceptable differences between the outputs of the original program and its relaxed variants.
We have used the Coq proof assistant to design and formalize a set
of proof rules for verifying acceptability properties of relaxed
programs written in a simple imperative language. And our
experience using the rules suggests that our design enables
developers to reduce the effort required to verify a relaxed
program by reusing the verification effort (or assumptions) done
for the original program.
View or download presentation
 Formal Reasoning on ComponentBased Reconfigurable Applications, Nuno Gaspar, INRIA Sophia Antipolis Méditerranée
[Show details]
Componentbased Engineering aims at providing a modular means to
specify a wide range of applications. The idea is to promote a
clean separation of concerns, and thus reusability, in order to
ease the burden of software development and maintenance. To this
end, the Grid Component Model (GCM), our inhouse component model,
provides all the means to define, compose and dynamically
reconfigure such applications.
In this talk we present our ongoing work towards a framework for
the specification and verification of GCM applications mechanized
in the Coq Proof Assistant. Our goal is to provide an unified
environment for the formal reasoning of the typical functional and
nonfunctional concerns found in componentbased applications.
View or download presentation
 A Specification Logic for Termination and NonTermination Reasoning, TonChanh Le, National University of Singapore
[Show details]
We propose a logical framework for specifying and proving
assertions about program termination and nontermination. Although
program termination has been well studied, it is usually added as
an external component to a specification logic. In this talk, we
propose to integrate termination requirements directly into our
logic, as temporal resource constraints for each execution of
every method. Semantically, each temporal constraint is an
abstraction of the computing resource that is required for program
execution. Terminating computation requires only finitely bounded
computing resource, while nonterminating computation requires
infinite computing resource. With a novel logical entailment with
frame inference for assertions of those temporal constraints, the
Hoare logic can be extended to verify both partial correctness and
(non) termination in a unified system. As an integrated logic,
our approach can leverage on richer specification logics to help
conduct more intricate termination reasoning for programs with
both heap manipulation and multiple terminating phases. We expect
our termination reasoning to benefit from any future improvements
to our logics, and viceversa. With an experimental evaluation, we
report on the usability and practicality of our approach for
capturing both termination and nontermination reasoning for an
existing verification system.
View or download presentation
Session 3A (25/1 18:3019:15)
 Intuitionistic Type Theory and Equality, Francesco Mazzoli, Imperial College London
 Building Database Management on Top of Category Theory in Coq, Jason Gross, MIT
[Show details]
The category of categories is isomorphic to the category of
relational databases. The language of category theory promises to
provide a structured way to talk about migrating data between
databases. Additionally, formulating database management in a
proof assistant allows guarantees about the properties and
correctness of database operations to be stated and proven. Using
the Coq proof assistant, I have formalized from scratch most of
the category theory necessary to implement data migration. The
constructions include categories, functors, natural
transformations, natural equivalences, opposite categories,
functor categories, adjoint pairs, limits and colimits (defined in
general, constructed in the category of sets), comma categories,
universal morphisms, the category of small categories, the
underlying graph of a category, coend, discrete categories,
subcategories, and product and sum categories. Proven properties
include that the diagonal (or ``constant diagram'') functor is
right adjoint to the colimit functor and left adjoint to the limit
functor, and that the unit, counit, and Homset equivalence
formulations of adjunction are equivalent.
View or download presentation
 Natural Proofs for Structure, Data, and Separation, Xiaokang Qiu, University of Illinois at UrbanaChampaign
[Show details]
We propose ``natural proofs'', for reasoning with programs that manipulate datastructures against complex specifications specifications that describe the structure of the heap, the data stored within it, and separation and framing of substructures. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, that provide sound but incomplete procedures, and that capture common reasoning tactics in program verification. We develop a dialect of separation logic over heaps, called Dryad, with recursive definitions that avoids explicit quantification. We develop ways to reason with heaplets using classical logic over the theory of sets, and develop natural proofs for reasoning using proof tactics involving disciplined unfoldings and formula abstractions. Natural proofs are encoded into decidable theories of firstorder logic so as to be discharged using SMT solvers.
We also implement the technique and show that a large class of more than 100 correct programs that manipulate datastructures are amenable to full functional correctness using the proposed natural proof method. These programs are drawn from a variety of sources including standard datastructures, the SchorrWaite algorithm for garbage collection, a large number of lowlevel C routines from the Glib library, the OpenBSD library and the Linux kernel, and routines from a secure verified OSbrowser project. Our work is the first that we know of that can handle such a wide range of full functional verification properties of heaps automatically, given pre/post and loop invariant annotations. We believe that this work paves the way for the deductive verification technology to be used by programmers who do not (and need not) understand the internals of the underlying logic solvers, significantly increasing their applicability in building reliable systems.
View or download presentation
 Semantics of an Intermediate Language for Program Transformation, Sigurd Schneider, Universität des Saarlandes, Saarbrücken, Germany
[Show details]
We present a language with two different semantic interpretations: An imperative interpretation allows to concisely encode control flow graphs as they occur in every compiler. A functional interpretation reveals a common firstorder, functional language where function application is restricted to tail calls. We call a program invariant if the two interpretations coincide and give sufficient and decidable criteria to identify invariant programs. Since we can switch interpretations on invariant programs, many transformations that occur in compilers can be naturally reflected to the functional setting, and correctness criteria for transformations can be analyzed in the functional setting, too. For example, register allocation becomes essentially alpharenaming, and an allocation is correct if it respects alpha equivalence.
Of particular importance is the transformation to the invariant fragment, which comes in two flavors: One preserves the imperative semantics and the other preserves the functional semantics. If the imperative semantics is preserved, the transformation corresponds to construction of static single assignment (SSA) form. SSA form is a restriction on intermediate languages used in modern compilers like Java HotSpot VM, LLVM, and libFirm, because it provides referential transparency for a large class of expressions. The functional setting has the advantage that program equivalence is a congruence, hence justifying referential transparency in the imperative setting. The other transformation to the invariant fragment preserves the functional semantics and corresponds to register allocation.
The research builds on the observation by Appel and Kelsey that SSA programs are essentially functional programs. Based on this idea, we develop a framework to explain and analyze the correctness of program transformations that occur in realistic compilers and are traditionally formulated in an imperative setting. The work is formalized using the Coq proof assistant.
View or download presentation
 Glivenko and Kuroda for Simple Type Theory, Christine Rizkallah, Max Planck Institute for Informatics Saarland University
[Show details]
Glivenko's theorem states that an arbitrary propositional formula
is classically provable if and only if its double negation is
intuitionistically provable. The result does not extend to full
firstorder predicate logic, but does extend to firstorder
predicate logic without the universal quantifier. A recent paper
by Zdanowski shows that Glivenko's theorem also holds for second
order propositional logic without the universal quantifier. We
prove that Glivenko's theorem extends to some versions of simple
type theory without the universal quantifier. Moreover we prove
that Kuroda's negative translation, which is known to embed
classical firstorder logic into intuitionistic firstorder logic,
extends to the same versions of simple type theory. We also prove
that the Glivenko property fails for simple type theory once a
weak form of functional extensionality is included.
View or download presentation
Session 3B (25/1 18:3019:15)
 Metamorphic Testing with WSBPEL, María Azahara Camacho Magriñán, University of Cadiz
[Show details]
WSBPEL 2.0 is a standard language allows us to develop processes
between Web Services. These type of services have a great impact
because of the increasing number of transactions through
Internet. The importance of transactions are very high, so this
implies to pay attention to the software we use to make it
possible.
Traditional testing techniques advise us of the faults and other
errors, but due of the concurrency, compensation handling and
dynamic services of transactions, these type of testing techniques
are not enough.
Metamorphic Testing present a solution to these problems using
Metamorphic Relations. Studies have shown that this technique
improves the quality of the source code and software.
A case study is ``MetaSearch'' defined in OASIS. MetaSearch
consists of a search done by a user/client in Google search and
MSN search, and when the search is complete, returns the response
of both, but only the number required by the user.
This talk presents this case study and shows how detect an
internal fault of the WSBPEL source code with Metamorphic
Testing.
View or download presentation
 TurtleBlocks, Erin Davis and Karishma Chadha, Wellesley College
[Show details]
At Wellesley College, we have created a blocksbased programming environment called TurtleBlocks where pieces of code fit together in jigsawlike pieces. TurtleBlocks is a special blocksbased language because of how it treats local variables and scoping. For instance, copying and pasting blocks preserves the scope of the variable references contained in those blocks. If you rename the variable in its declaration, then all references to that variable change names as well.
View or download presentation
 TransCML: Consensus Made Easy, Carlo Spaccasassi, Trinity College Dublin, Ireland and Microsoft Research Cambridge, UK
[Show details]
Many of the difficulties in concurrent programming come from the absence of good language abstractions to address widely common and recurrent problems, such as mutual exclusion and process consensus. Transactional Memory is a now popular abstraction to implement mutual exclusion in concurrent sharedmemory systems. TM implementations allow the programmer to assume that no memory access violations occur at runtime, greatly reducing code complexity. TM achieves this by effectively isolating processes from each other. For this reason TM it is not a suitable abstraction for implementing consensus where processes need to communicate.
Recently proposed abstractions for streamlining consensus in concurrent programming also take a transactional form. However, these are transactions allowed to communicate with their environment rather than being isolated from it. TransCCS is a calculus that extends Milner's CCS with such an abstraction called Communicating Transactions, and has a simple behavioural theory capturing the notions of safety and liveness. However, it is primarily a specification language and it does not address the practical challenges in developing a programming language geared towards real concurrent and distributed systems.
In this talk, we present a number of illustrative scenarios that motivate the need for novel programming abstractions to implement consensus in concurrent systems. We also present the challenges and our workinprogress in developing TransCML, a functional programming language that adds Communicating Transactions to Concurrent ML. The ultimate goal of this work is to develop a language with an intuitive semantics, simple reasoning techniques and an efficient runtime system, and in which programmers can simply specify the local conditions for consensus, without spelling out how it can be achieved.
View or download presentation
 Atomicity Refinement for Verified Compilation, Vincent Laporte, University of Rennes 1, France
[Show details]
We consider the verified compilation of highlevel managed languages like Java
or C# whose intermediate representations provide support for sharedmemory
synchronization and automatic (concurrent) memory management. Our development
is framed in the context of the Total Store Order (TSO) relaxed memory model
underlying Intel x86 multiprocessors. Ensuring the correctness of compilers for
managed languages in such environments is challenging because highlevel
actions are translated into sequences of nonatomic actions with
compilerinjected snippets of potentially racy code; the behavior of this code
depends not only on the actions of other threads, but also on outoforder
reorderings performed by the processor. A naïve correctness proof of the
compiler would require reasoning over all possible thread interleavings that
can arise during execution, an impractical and nonscalable exercise. To
address this challenge, we define a refinementbased proof methodology that
precisely relates concurrent code expressed at different abstraction levels,
cognizant throughout of the relaxed memory semantics of the underlying
processor. Our technique allows the compiler writer to reason compositionally
about the atomicity of lowlevel concurrent code used to implement managed
services. We validate the effectiveness of our approach by demonstrating the
verified compilation of the nontrivial components comprising a realistic
concurrent garbage collector, including racy write barriers and memory
allocators.
View or download presentation
Sponsors
Other Student Activities
You should sign up for the complimentary TutorialFest, and look into PMWL, the Programming Languages Mentoring Workshop.
