In chronological order
A great variety of static analyses that compute safety properties of single- thread programs have now been developed. I will present a systematic method to extend a class of such static analyses, so that they handle programs with multiple POSIX-style threads. Starting from a pragmatic operational semantics, the final algorithm is then derived by abstract interpretation. It analyses each thread in turn, propagating interferences between threads, in addition to other semantic information. The combinatorial explosion, ensued from the explicit consideration of all interleavings, is thus avoided. The worst case complexity is only increased by a factor n compared to the single-thread case, where n is the number of instructions in the program. This method is implemented in Penjili, an EADS tool, demonstrating the practicality of the approach.
Programming skill is crucial for all Computer Science students which can only be mastered through intensive exercise practice. Apart from traditional face-to-face manner of teaching programming, which suffers certain disadvantages when dealing with large-sized classes, Web-based tutoring systems that can play the role of teacher are increasingly considered. With the recent advancement of Internet, such systems can liberate the learners from the restriction of time and venues for practice, as well as significantly reducing the cost of manpower.
To make those ideas feasible and practical, we propose a framework for automatic verification of programming works submitted from students. In our framework, we employ some formal methods for software verification, e.g. theorem proving and model checking, thus avoiding the risk of execution of actual code from student, which may sometimes be harmful. In particular, by the means of model checking, we are able to render the learners with some useful features such as invariant-free checking of loop-based programs or generation of counter-examples associated with error-flows. Our framework has been implemented and employed in our Faculty in the course of Programming Methodologies, and the initial results are somehow promising.
~~ IMPORTANT: this talk will take place in BC410 ~~
We consider a scenario where large data frames are broken into a few packets and transmitted over the network. Our focus is on a bottleneck router: the model assumes that in each time step, a set of packets (a burst) arrives, from which only one packet can be served, and all other packets are lost. A data frame is considered useful only if none of its constituent packets is lost, and otherwise it is worthless. We abstract the problem as a new type of online set packing, present a randomized distributed algorithm and a matching lower bound on the competitive ratio for any randomized online algorithm. Our bounds are expressed in terms of the maximal burst size and the maximal number of packets per frame. We also present refined bounds that depend on the uniformity of these parameters.
Joint work with Emek, Halldorsson, Mansour and Rawitz
Algebraic Petri Nets (APN: Petri Nets + Algebraic Abstract Data Types) are powerful tools to model concurrent systems. Because of their high expressive power, allowing end-users to model complex systems in a compact way, state space explosion is a big issue when verifying properties on APN models. Symbolic Model Checking (SMC) and particularly Decision Diagrams (DD) based model checking is a proven technique to handle the state space explosion for simpler formalisms such as P/T Petri nets. This presentation shows how to use Binary Decision Diagrams' (BDD) evolutions (Data Decision Diagrams, Set Decision Diagrams, SigmaDD, to tackle the state space explosion problem in the APN world. The main contribution of this work is the notion of the Algebraic Cluster and partial net unfolding that tackles the concurrency induced by token multiplicity. These algorithms have been implemented in a tool that is freely accessible on http://alpina.unige.ch, a short demo will be made.
Abstract: Over the last few years Microsoft Research has been working on bringing simple and pragmatic program specification, aka Code Contracts, to programming languages targeting the Microsoft .NET platform. Contracts document programming assumptions in a machine discoverable form.
Contracts are targeted at the general developer, not the verification enthusiast. It is thus important to use a single form of specifications that meets three simultaneous goals:
Our specification approach is language-agnostic in that we use idiomatic code written in the developer's source language to express preconditions, postconditions, and object invariants.
Abstract: Closures, first-class citizen procedures that are able to capture their lexical environment, increase the expressiveness of object-oriented languages such as C#, Scala, and various dynamic languages. However, closures make program specification and verification more difficult. For instance, a verification methodology must allow specifications to describe the behavior of one method relatively to the specification of another method passed as argument, and it must allow specifications to describe the behavior of a closure without exposing its captured state. This paper presents a modular specification and verification methodology for closures. Our solution is based on first-order logic and, thus, well suited for automatic verification with SMT solvers. We have verified a series of interesting examples that cover the main applications of closures such as delegation patterns and even the creation of custom control flow.
Abstract: The theory of Well Structured Transition Systems provides the good structure for computing a finite basis of the set of predecessors of the upward closure of a finite set of states. We address here the dual problem which is to compute a finite representation of the set of successors of the downward closure of a finite set of states (called the cover). This last problem is, a priori, more difficult because in general, the cover has no finite basis. It is possible to complete any well-ordered set to obtain a cpo in which every downward closed set has a finite representation. We then define the framework of Complete Well Structured Transition Systems and we propose a simple and a conceptual procedure for computing the covering set. This procedure terminates more often than the generalized Karp-Miller tree procedure when applied on extended Petri nets and lossy channel systems.
Abstract: We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests.
In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. Our algorithms are based on new quantifier elimination and symbolic manipulation techniques.
Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation.
The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming.
An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by reference. Moreover, the problematic interplay between destructive reads–often used to implement unique references–and temporary aliasing through ``borrowed'' references is exacerbated in a concurrent setting, increasing the potential for unpredictable run-time errors.
This paper introduces a new approach to uniqueness. The idea is to use capabilities for enforcing both at-most-once consumption of unique references, and a flexible notion of uniqueness. The main novelty of our approach is a model of uniqueness and borrowing based on simple, unstructured capabilities. The advantages are: first, it provides simple foundations for uniqueness and borrowing. Second, it can be formalized using a relatively simple type system, for which we provide a complete soundness proof. Third, it avoids common problems involving borrowing and destructive reads, since unique references subsume borrowed references.
We have implemented our type system as an extension to Scala. Practical experience suggests that our system allows type checking real-world actor-based concurrent programs with only a small number of additional type annotations.
Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w1*w2*… wk* for some words w1,…,wk. Bounded languages have nice structural and decidability properties.
We show two applications of bounded languages in model checking: first, to underapproximate the reachable state space of multithreaded procedural programs and second, to underapproximate the reachable state space of counter machines. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.
We also show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L' which is a subset of L and has the same Parikh image as L.
(Joint work with Pierre Ganty and Benjamin Monmege)
Applications that process complex inputs often react in different ways to changes in different regions of the input. Small changes to forgiving regions induce correspondingly small changes in the behavior and output. Small changes to critical regions, on the other hand, can induce disproportionally large changes in the behavior or output. Identifying the critical and forgiving regions in the input and the corresponding critical and forgiving regions of code is directly relevant to many software engineering tasks.
In this talk, I will present a system, Snap, for automatically grouping related input bytes into fields and classifying each field and corresponding regions of code as critical or forgiving. Given an application and one or more inputs, Snap uses targeted input fuzzing in combination with dynamic execution and influence tracing to classify regions of input fields and code as critical or forgiving. Our experimental evaluation shows that Snap makes classifications with close to perfect precision (99%) and very good recall (between 99% and 73%, depending on the application).
Constraint solvers play a central role in the construction of reliable and secure software, regardless of whether such software is based on formal methods, program analysis, testing or synthesis. In this talk, I will present two solvers namely, STP and HAMPI. STP extends SAT solvers with the theory of bit-vectors and arrays, and has enabled a new testing technique known as Concolic Testing. STP-enabled Concolic testers have been used to find hundreds of previously unknown bugs in Unix utilities, OS kernels, media players, and commercial software, some with approximately a million lines of code. HAMPI is designed for the analysis of string-manipulating programs and incorporates a rich theory of equality over bounded string variables, bounded regular expressions, and context-free grammars. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis. I will discuss techniques that make these solvers scale to large formulas obtained from real-world applications, and some related theoretical results.
Dr. Vijay Ganesh is a Research Scientist at MIT since 2007. He completed his PhD in computer science from Stanford University in 2007, and Bachelor of Technology from College of Engineering, Trivandrum, India. His primary research interests are constraint solvers and their applications to software reliability, computer security and biology. His STP solver was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006, and his paper on HAMPI won the ACM Distinguished Paper Award in 2009.