Announcing the winners of 2013

Session I	Session II	Session III
Durica Nikolic University of Verona and MSR U Trento	Michael Carbin MIT	Sigurd Schneider Saarland University

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 co-located event over those who are.

Schedule

Session 1A (23/1 18:00-19:00)

1. Verification of Erlang-style Concurrency, Emanuele D'Osualdo, University of Oxford, Department of Computer Science
   [Show details]

   This talk presents an approach for the fully-automatic program analysis and verification of Erlang modules. The fragment of Erlang we consider includes the higher-order 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 infinite-state 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 mutual-exclusion and boundedness of mailboxes.

   View or download presentation (PDF version)

2. Constraint-based 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 side-effects 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

3. Large-Scale Semantics-Based 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 cost-effective solutions have emerged to handle the volume, velocity and variability of massive data, Big Data analytics has become wide-spread 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 large-scale semantics-based 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. Fine-grained 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 fine-grained 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 multi-level tree and graph indexing scheme to support the analyses needed with high accuracy. The fine-grained 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 fine-grained 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

4. 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

5. Efficient Verification of Process-Local Properties with Projections, Habib Saissi, Technische Universität Darmstadt
   [Show details]

   Verification of multi-process 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 process-local properties. Firstly, we characterize a non-trivial subset of all interleavings, called projections, that preserve all reachable local states. Intuitively, projections are sequences of process-local 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 process-local 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 partial-order and symmetry reductions.

   View or download presentation

Session 1B (23/1 18:00-19:00)

1. 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 post-conditions 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

2. Synthesis of Randomized Accuracy-Aware 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 semantics-preserving 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 optimization-based 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

3. Synchronization Synthesis for Shared-Memory 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 finite-state concurrent programs composed of processes that may have local and shared variables, may be straight-line or branching programs, may be ongoing or terminating, and may have program-initialized or user-initialized 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

4. Control Explicit---Data 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 data-flow component (input variables) produces regular nondeterminism, which we can capture using symbolic approaches, mainly by deciding satisfiability of its logical representation. The control-flow component (interleaving of parallel processes) produces considerably less regular nondeterminism, and it seems that explicit, enumerative approaches handle the control-flow 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 explicit---data 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, multi-states containing one state for every combination of input variable evaluations. Depending on what first-order theory is used to represent the multi-states, satisfiability of different properties of the multi-states 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 bit-vectors 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 bit-vectors, together with distributed explicit model checking, can support complete verification of parallel software of substantial size: both compared to present approaches and sufficient to real-world application in specific domains. These domains include safety-critical 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 multi-states 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

5. 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 well-studied 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:30-18:30)

1. 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 contract-oriented 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 multi-player 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

2. 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 proofs-as-programs 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

3. A Lattice-Based Approach to Deterministic Parallelism, Lindsey Kuper, Indiana University
   [Show details]

   Programs written using a deterministic-by-construction model of parallel computation always produce the same observable results, offering programmers the promise of freedom from subtle, hard-to-reproduce nondeterministic bugs. A common theme that emerges in the study of deterministic-by-construction 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 deterministic-by-construction parallel programming that generalizes existing single-assignment models. Our model allows multiple assignments that are monotonically increasing with respect to a user-specified 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

4. 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

5. 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 run-time 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 run-time instrumentation of the object-model and function-calling protocol with a performance comparable to a state-of-the-art interpreter, without having to modify the VM source code. Our approach consists in running a metacircular VM targeting the source language, based on a message-sending 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:30-18:30)

1. Towards Complete Specifications with an Error Calculus, Quang-Loc 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, must-error and may-error) 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 user-defined predicates and lemmas.We have implemented our calculus in an automated verification tool for pointer-based 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

2. Towards Noninterference in Composed Languages, Andreas Gampe, The University of Texas at San Antonio
   [Show details]

   As more personal information is entrusted to internet-connected 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 well-typed 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 security-complete, 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 non-trivial security-typed language is security-complete. We formally establish conditions sufficient for a security-typed language to be complete. Our reasoning is based on security-level separability and typability of computations at a single security level. While this allows us to show the conjecture for primitive-typed 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 security-typed languages that are imperative, functional and object-oriented, respectively.

   View or download presentation

3. 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 programs--they 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

4. Formal Reasoning on Component-Based Reconfigurable Applications, Nuno Gaspar, INRIA Sophia Antipolis Méditerranée
   [Show details]

   Component-based 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 in-house 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 non-functional concerns found in component-based applications.

   View or download presentation

5. A Specification Logic for Termination and Non-Termination Reasoning, Ton-Chanh Le, National University of Singapore
   [Show details]

   We propose a logical framework for specifying and proving assertions about program termination and non-termination. 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 non-terminating 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 vice-versa. With an experimental evaluation, we report on the usability and practicality of our approach for capturing both termination and non-termination reasoning for an existing verification system.

   View or download presentation

Session 3A (25/1 18:30-19:15)

1. Intuitionistic Type Theory and Equality, Francesco Mazzoli, Imperial College London
2. 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 Hom-set equivalence formulations of adjunction are equivalent.

   View or download presentation

3. Natural Proofs for Structure, Data, and Separation, Xiaokang Qiu, University of Illinois at Urbana-Champaign
   [Show details]

   We propose ``natural proofs'', for reasoning with programs that manipulate data-structures against complex specifications--- specifications that describe the structure of the heap, the data stored within it, and separation and framing of sub-structures. 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 first-order 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 data-structures are amenable to full functional correctness using the proposed natural proof method. These programs are drawn from a variety of sources including standard data-structures, the Schorr-Waite algorithm for garbage collection, a large number of low-level C routines from the Glib library, the OpenBSD library and the Linux kernel, and routines from a secure verified OS-browser 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

4. 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 first-order, 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 alpha-renaming, 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

5. 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 first-order predicate logic, but does extend to first-order 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 first-order logic into intuitionistic first-order 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:30-19:15)

1. Metamorphic Testing with WS-BPEL, María Azahara Camacho Magriñán, University of Cadiz
   [Show details]

   WS-BPEL 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 WS-BPEL source code with Metamorphic Testing.

   View or download presentation

2. TurtleBlocks, Erin Davis and Karishma Chadha, Wellesley College
   [Show details]

   At Wellesley College, we have created a blocks-based programming environment called TurtleBlocks where pieces of code fit together in jigsaw-like pieces. TurtleBlocks is a special blocks-based 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

3. 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 shared-memory 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 work-in-progress 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

4. Atomicity Refinement for Verified Compilation, Vincent Laporte, University of Rennes 1, France
   [Show details]

   We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory 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 high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of potentially racy code; the behavior of this code depends not only on the actions of other threads, but also on out-of-order 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 non-scalable exercise. To address this challenge, we define a refinement-based 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 low-level concurrent code used to implement managed services. We validate the effectiveness of our approach by demonstrating the verified compilation of the non-trivial 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.