Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high level of automation in the back-end. This paper presents AutoProof, a state-of-the-art auto-active verifier for object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features and a powerful methodology for framing and class invariants, which make it applicable in practice to idiomatic object-oriented patterns. The paper focuses on describing AutoProof's interface, design, and implementation features, and demonstrates AutoProof's performance on a rich collection of benchmark problems. The results attest AutoProof's competitiveness among tools in its league on cutting-edge functional verification of object-oriented programs.

We present the integration of the AutoFix automated program repair technique into the EiffelStudio Development Environment. AutoFix presents itself like a recommendation system capable of automatically finding bugs and suggesting fixes in the form of source-code patches. Its performance suggests usage scenarios where it runs in the background or during work interruptions, displaying fix suggestions as they become available. This is a contribution towards the vision of semantic Integrated Development Environments, which offer powerful automated functionality within interfaces familiar to developers. A screencast highlighting the main features of AutoFix can be found at: http://youtu.be/Ff2ULiyL-80.

AutoProof is an automatic verifier for functional properties of programs written in Eiffel. This paper illustrates some of AutoProof's capabilities when tackling the three challenges of the VerifyThis verification competition held at FM 2012, as well as on three other problems proposed in related events. AutoProof 's design focuses on making it practically applicable with reduced user effort. Tackling the challenges demonstrates to what extent this design goal is met in the current implementation: while some of AutoProof's current limitations prevent us from verifying the complete specification of the prefix sum and binary search tree algorithms, we can still prove some partial properties on interesting special cases, but with the advantage of requiring little or no specification.

In globally distributed software development, does it matter being agile rather than structured? To answer this question, this paper presents an extensive case study that compares agile (Scrum, XP, etc.) vs. structured (RUP, waterfall) processes to determine if the choice of process impacts aspects such as the overall success and economic savings of distributed projects, the motivation of the development teams, the amount of communication required during development, and the emergence of critical issues. The case study includes data from 66 projects developed in Europe, Asia, and the Americas. The results show no significant difference between the outcome of projects following agile processes and structured processes, suggesting that agile and structured processes can be equally effective for globally distributed development. The paper also discusses several qualitative aspects of distributed software development such as the advantages of nearshore vs. offshore, the preferred communication patterns, and the effects on project quality.

Contracts are a form of lightweight formal specification embedded in the program text. Being executable parts of the code, they encourage programmers to devote proper attention to specifications, and help maintain consistency between specification and implementation as the program evolves. The present study investigates how contracts are used in the practice of software development. Based on an extensive empirical analysis of 21 contract-equipped Eiffel, C#, and Java projects totaling more than 260 million lines of code over 7700 revisions, it explores, among other questions: 1 which kinds of contract elements preconditions, postconditions, class invariants are used more often; 2 how contracts evolve over time; 3 the relationship between implementation changes and contract changes; and 4 the role of inheritance in the process. It has found, among other results, that: the percentage of program elements that include contracts is above 33% for most projects and tends to be stable over time; there is no strong preference for a certain type of contract element; contracts are quite stable compared to implementations; and inheritance does not significantly affect qualitative trends of contract usage.

While most debugging techniques focus on patching implementations, there are bugs whose most appropriate corrections consist in fixing the specification to prevent invalid executions—such as to define the correct input domain of a function. In this paper, we present a fully automatic technique that fixes bugs by proposing changes to contracts (simple executable specification elements such as pre- and postconditions). The technique relies on dynamic analysis to understand the source of buggy behavior, to infer changes to the contracts that emend the bugs, and to validate the changes against general usage. We have implemented the technique in a tool called SpeciFix which works on programs written in Eiffel, and evaluated it on 44 bugs found in standard data-structure libraries. Manual analysis by human programmers found that SpeciFix suggested repairs that are deployable for 25

Collaborative software development requires programmers to coordinate their work and merge individual contributions into a consistent shared code base. Traditionally, coordination follows a series of update-modify-commit" cycles, where merge conflicts arise upon committing if individual modifications have diverged and must be explicitly reconciled. Researchers have been suggesting that providing timely awareness information about "who's changing what" may not only help deal with conflicts but, more generally, improve the effectiveness of collaboration. This paper investigates the impact of awareness information in the context of globally distributed software development. Based on an analysis of data from 105 student developers constituting 12 development teams located in different countries, we analyze, among other things: 1) the frequency of merge conflicts and insufficient awareness, 2) the impact of distribution on team awareness, 3) the perceived impact of conflicts and lack of awareness on productivity, motivation, and project punctuality. Our findings include: 1) lack of awareness occurs more frequently than merge conflicts, 2) information about remote team members is missing roughly as often as information about colocated ones, 3) insufficient awareness information affects more negatively programmer's performance than merge conflicts.

Modular and local reasoning about object-oriented programs has been widely studied for programing languages such as C# and Java. Once source programs have been proven, the next verification challenge is to ensure that the code produced by the compiler is correct. Since verifying a compiler can be extremely complex, this paper uses proof-transforming compilation , an alternative approach which automatically generates certificates , a bytecode proof, from proofs in the source language. The paper develops a bytecode logic using separation logic, and proof translation from proofs of object-oriented programs to bytecode. The translation also handles proofs for concurrent programs. The bytecode logic and the proof transformation are proven sound.

The importance of planning and management skills in software development is very difficult to convey in software engineering courses. We present the synopsis of an assignment whose purpose is to demonstrate the significance of such skills, including effective communication, team coordination and collaboration, and overall project planning. The assignment is organized in the context of a distributed software engineering course carried out in collaboration with 12 universities in South America, Europe and Africa. The assignment is a globally distributed contest issued before most development activities related to the course's software project are performed, aiming at favoring the collaboration between students prior to project development. The contest does not involve any programming, and is not related to the project development activities. Instead, it consists of making teams in different countries compete in collaboratively solving a set of very simple tasks. The complexity of the activity is in team collaboration and coordination, and their lack is evident when the tasks are not correctly solved, or not solved in time. Despite the simplicity of the as-signment, students have found it useful in helping them understand the significance of management and planning challenges in distributed software development. Moreover, the assignment helped in team building, by creating a better team atmosphere and contributing in identifying team members better suited for management.

This paper describes AutoFix, an automatic debugging technique that can fix faults in general-purpose software. To provide high-quality fix suggestions and to enable automation of the whole debugging process, AutoFix relies on the presence of simple specification elements in the form of contracts (such as pre- and postconditions). Using contracts enhances the precision of dynamic analysis techniques for fault detection and localization, and for validating fixes. The only required user input to the AutoFix supporting tool is then a faulty program annotated with contracts; the tool produces a collection of validated fixes for the fault ranked according to an estimate of their suitability. In an extensive experimental evaluation, we applied AutoFix to over 200 faults in four code bases of different maturity and quality (of implementation and of contracts). AutoFix successfully fixed 42 percent of the faults, producing, in the majority of cases, corrections of quality comparable to those competent programmers would write; the used computational resources were modest, with an average time per fix below 20 minutes on commodity hardware. These figures compare favorably to the state of the art in automated program fixing, and demonstrate that the AutoFix approach is successfully applicable to reduce the debugging burden in real-world scenarios.

Debugging - the process of finding and correcting programming mistakes - faces too the challenges of distributed and collaborative development. The debugging tools commonly used by programmers are integrated into traditional development environments such as Eclipse or Visual Studio, and hence do not offer specific features for collaboration or remote shared usage. In this paper, we describe CDB, a debugging technique and integrated tool specifically designed to support effective collaboration among developers during shared debugging sessions. We also discuss the design and results of an empirical study aimed at identifying features that can ameliorate the effectiveness of collaborative debugging processes, and at evaluating the usefulness of our CDB collaborative debugging approach. The study suggests that CDB's collaboration features are often perceived as important for effective debugging, and can improve the overall debugging experience in collaborative settings.

JavaScript ranks among the most popular programming languages for the web, yet its highly dynamic type system and occasionally unintuitive semantics make programming particularly error-prone. This paper presents Javanni, a verifier for JavaScript programs that can statically detect many common programming errors. Javanni checks the absence of standard type-related errors (such as accessing undefined fields) without requiring user-written annotations, and it can also verify full functional-correctness specifications. Several experiments with JavaScript applications reported in the paper demonstrate that Javanni is flexibly usable on programs with non-trivial specifications. Javanni is available online within the CloudStudio web integrated environment.

Even when implemented in a purely procedural programming language, properly designed programs possess elements of good design that are expressible through object-oriented constructs and concepts. For example, placing structured types and the procedures operating on them together in the same module achieves a weak form of encapsulation that reduces inter-module coupling. This paper presents a novel technique, and a supporting tool AutoOO, that extracts such implicit design elements from C applications and uses them to build reengineered object-oriented programs. The technique is completely automatic: users only provide a source C program, and the tool produces an object-oriented application written in Eiffel with the same input/output behavior as the source. An extensive evaluation on 10 open-source programs (including the editor vim and the math library libgsl) demonstrates that our technique works on applications of significant size and builds reengineered programs exhibiting elements of good object-oriented design, such as low coupling and high cohesion of classes, and proper encapsulation. The reengineered programs also leverage advanced features such as inheritance, contracts, and exceptions to achieve a better usability and a clearer design. The tool AutoOO is freely available for download.

As software development becomes an increasingly collaborative effort, traditional development tools have to be extended to support seamless collaboration while minimizing the chances of conflicts. This paper describes Cloud Studio, a collaboration framework that integrates a fine-grained software configuration management model and a real-time awareness system. Cloud Studio's configuration management operates transparently by automatically sharing the changes of developers working on the same project, the real-time awareness system allows for dynamic views on the project selectively including or excluding other developers' changes. With this tight integration, conflicts are prevented in many cases, while leaving individual developers free to experiment without blocking others. The paper also describes a freely available prototype web-based implementation of Cloud Studio and a case study that demonstrates the usability of the approach for collaborative software development.

The simple and often imprecise specifications that programmers may write are a significant limit to a wider application of rigorous program verification techniques. Part of the reason why non-specialists find writing good specification hard is that, when verification fails, they receive little guidance as to what the causes might be, such as implementation errors or inaccurate specifications. To address these limitations, this paper presents two-step verification , a technique that combines implicit specifications, inlining, and loop unrolling to provide improved user feedback when verification fails. Two-step verification performs two independent verification attempts for each program element: one using standard modular reasoning, and another one after inlining and unrolling; comparing the outcomes of the two steps suggests which elements should be improved. Two-step verification is implemented in AutoProof, our static verifier for Eiffel programs integrated in EVE the Eiffel Verification Environment and available online.

TOPI (http://se.inf.ethz.ch/events/topi2013/) is a workshop started in 2011 to address research questions involving plug-ins: software components designed and written to execute within an extensible platform. Most such software components are tools meant to be used within a development environment for constructing software. Other environments are middle-ware platforms and web browsers. Research on plug-ins encompasses the characteristics that differentiate them from other types of software, their interactions with each other, and the platforms they extend.

The LASER school is intended for professionals from the industry (engineers and managers) as well as university researchers, including PhD students. Participants learn about the most important softwar