# Publications by Carlo A. Furia

## Currently submitted and work in progress

(Ask me if you're interested in drafts of these papers.)

• AutoProof: Auto-active Functional Verification of Object-oriented Programs.
Julian Tschannen, Carlo A. Furia, Martin Nordio, and Nadia Polikarpova.
(See AutoProof's page and gallery of verified benchmarks.)
• A Comparative Study of Programming Languages in Rosetta Code.
Sebastian Nanz and Carlo A. Furia.
(See the technical report version.)
• Automating Full Functional Verification of Programs with Loops.
Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller.
(See the DynaMate project page and the technical report write-up.)

## Details

Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller.
DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification.
In Proceedings of the 10th Haifa Verification Conference (HVC).
Lecture Notes in Computer Science, 8855:48–53, Springer, November 2014 (Tool paper).

Abstract
DynaMate is a tool that automatically infers loop invariants and uses them to prove Java programs correct with respect to a given JML functional specification. DynaMate improves the flexibility of loop invariant inference by integrating static (proving) and dynamic (testing) techniques with the goal of combining their complementary strengths. In an experimental evaluation involving 26 Java methods of java.util annotated with JML pre- and postconditions, it automatically discharged over 97% of all proof obligations, resulting in automatic complete correctness proofs of 23 out of the 26 methods.

• The paper in PDF format (updated and improved text) and its DOI.
• DynaMate's techniques and its experimental evaluation are described in a technical report.
• DynaMate's project page.
@InProceedings{GFMFZ-HVC14-DynaMate,
author = {Juan P. Galeotti and Carlo A. Furia and Eva May and Gordon Fraser and Andreas Zeller},
title = {{D}yna{M}ate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification},
booktitle = {Proceedings of the 10th Haifa Verification Conference (HVC)},
year = {2014},
editor = {Eran Yahav},
series = {Lecture Notes in Computer Science},
pages = {48--53},
volume = {8855},
month = {November},
publisher = {Springer},
note = {Tool paper},
acceptancerate = {49\%}
}


Carlo A. Furia and Paola Spoletini.
Bounded Variability of Metric Temporal Logic.
In Proceedings of the 21st International Symposium on Temporal Representation and Reasoning (TIME'14).
Pgg. 155–163, IEEE Computer Society, September 2014.

Abstract
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability—where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability?
In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.

@InProceedings{FS-TIME14,
author = {Carlo A. Furia and Paola Spoletini},
title = {Bounded Variability of Metric Temporal Logic},
booktitle = {Proceedings of the 21st International Symposium on Temporal Representation and Reasoning (TIME'14)},
pages = {155--163},
editor    = {Amedeo Cesta and Carlo Combi and Francois Laroussinie},
year = {2014},
month = {September},
publisher = {IEEE Computer Society},
acceptancerate = {53\%}
}


Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, and Andreas Zeller.
Automated Fixing of Programs with Contracts.
IEEE Transactions on Software Engineering, 40(5):427–449.
IEEE Computer Society, May 2014.

Abstract
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% 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.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• An extended version with appendix is available as technical report.
• This journal paper combines and extends the previous publications [ISSTA'10] and [ASE'11] on AutoFix. In particular, it describes the latest AutoFix implementation and includes a detailed experimental evaluation.
• The AutoFix project page.
@Article{PFNWMZ-TSE14,
author = {Yu Pei and Carlo A. Furia and Martin Nordio and Yi Wei and Bertrand Meyer and Andreas Zeller},
title = {Automated Fixing of Programs with Contracts},
journal = {IEEE Transactions on Software Engineering},
volume = {40},
number = {5},
pages = {427--449},
month = {May},
year = {2014}
}


H.-Christian Estler, Martin Nordio, Carlo A. Furia, and Bertrand Meyer.
Awareness and Merge Conflicts in Distributed Software Development.
In Proceedings of the 9th International Conference on Global Software Engineering (ICGSE).
Pgg. 26–35, IEEE Computer Society, August 2014.

Abstract
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 co-located ones; 3) insufficient awareness information affects more negatively programmer's performance than merge conflicts.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• This paper won the best paper award at ICGSE 2014.
@InProceedings{ENFM-ICGSE14,
author = {H.-Christian Estler and Martin Nordio and Carlo A. Furia and Bertrand Meyer},
title = {Awareness and Merge Conflicts in Distributed Software Development},
booktitle = {Proceedings of the 9th International Conference on Global Software Engineering (ICGSE)},
editor    = {Yuanfang Cai and Jude Fernandez and Wenyun Zhao},
pages = {26--35},
year = {2014},
month = {August},
publisher = {IEEE Computer Society},
acceptancerate = {36\%},
note = {Best paper award}
}


Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer.
Flexible Invariants Through Semantic Collaboration.
In Proceedings of the 19th International Symposium on Formal Methods (FM).
Lecture Notes in Computer Science, 8442:514–530, Springer, May 2014.

Abstract
Modular reasoning about class invariants is challenging in the presence of collaborating objects that need to maintain global consistency. This paper presents semantic collaboration: a novel methodology to specify and reason about class invariants of sequential object-oriented programs, which models dependencies between collaborating objects by semantic means. Combined with a simple ownership mechanism and useful default schemes, semantic collaboration achieves the flexibility necessary to reason about complicated inter-object dependencies but requires limited annotation burden when applied to standard specification patterns. The methodology is implemented in AutoProof, our program verifier for the Eiffel programming language (but it is applicable to any language supporting some form of representation invariants). An evaluation on several challenge problems proposed in the literature demonstrates that it can handle a variety of idiomatic collaboration patterns, and is more widely applicable than the existing invariant methodologies.

• The paper in PDF format (updated and improved text) and its DOI.
• An extended version is available as technical report.
• Supplementary material and online examples are available on the SC project page.
@InProceedings{PTFM-FM14-SemiCola,
author = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia and Bertrand Meyer},
title = {Flexible Invariants Through Semantic Collaboration},
booktitle = {Proceedings of the 19th International Symposium on Formal Methods (FM)},
year = {2014},
editor = {Cliff B. Jones and Pekka Pihlajasaari and Jun Sun},
series = {Lecture Notes in Computer Science},
pages = {514--530},
volume = {8442},
month = {May},
publisher = {Springer},
acceptancerate = {28\%}
}


H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, and Bertrand Meyer.
Contracts in Practice.
In Proceedings of the 19th International Symposium on Formal Methods (FM).
Lecture Notes in Computer Science, 8442:230–246, Springer, May 2014.

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

@InProceedings{EFNPM-FM14-Coat,
author = {H.-Christian Estler and Carlo A. Furia and Martin Nordio and Marco Piccioni and Bertrand Meyer},
title = {Contracts in Practice},
booktitle = {Proceedings of the 19th International Symposium on Formal Methods (FM)},
year = {2014},
editor = {Cliff B. Jones and Pekka Pihlajasaari and Jun Sun},
series = {Lecture Notes in Computer Science},
pages = {230--246},
volume = {8442},
month = {May},
publisher = {Springer},
acceptancerate = {28\%}
}


Yu Pei, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Automatic Program Repair by Fixing Contracts.
In Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE).
Lecture Notes in Computer Science, 8411:246–260, Springer, April 2014.

Abstract
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% of the faults; in most cases, these contract repairs were preferred over fixes for the same bugs that change the implementation.

• The paper in PDF format (updated, improved, and extended text with appendix) and its DOI.
• The SpeciFix project page.
@InProceedings{PFNM-FASE14,
author = {Yu Pei and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Automatic Program Repair by Fixing Contracts},
booktitle = {Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE)},
year = {2014},
editor = {Stefania Gnesi and Arend Rensink},
series = {Lecture Notes in Computer Science},
pages = {246--260},
volume = {8411},
month = {April},
publisher = {Springer},
acceptancerate = {23\%}
}


Julian Tschannen, Carlo A. Furia, and Martin Nordio.
AutoProof Meets Some Verification Challenges.
International Journal on Software Tools for Technology Transfer.
Springer, February 2014.

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

@Article{TFN-STTT14,
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio},
title = {{A}uto{P}roof Meets Some Verification Challenges},
journal = {International Journal on Software Tools for Technology Transfer},
year = {2014},
pages = {1--11},
month = {February},
publisher = {Springer},
note = {Special section on the VerifyThis 2012 Verification Competition.}
}


Carlo A. Furia, Bertrand Meyer, and Sergey Velder.
Loop Invariants: Analysis, Classification, and Examples.
ACM Computing Surveys, 46(3), Article 34, January 2014.

Abstract
Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a "loop invariant". Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs.
We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns, and presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on "domain theory". It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.

@Article{FMV-CSUR14,
author = {Carlo A. Furia and Bertrand Meyer and Sergey Velder},
title = {Loop Invariants: Analysis, Classification, and Examples},
journal = {ACM Computing Surveys},
volume = {46},
number = {3},
year = {2014},
pages = {Article 34},
publisher = {ACM},
month = {January},
}


Hans-Christian Estler, Martin Nordio, Carlo A. Furia, Bertrand Meyer, and Johannes Schneider.
Agile vs. Structured Distributed Software Development: A Case Study.
Empirical Software Engineering, 19(5):1197–1224.
Springer, October 2014.

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

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• This paper is an extended version of the conference paper with the same title; it was invited to a special issue of the Empirical Software Engineering journal with the best papers from ICGSE 2012.
@Article{ENFMS-ESE13,
author = {Hans-Christian Estler and Martin Nordio and Carlo A. Furia and Bertrand Meyer and Johannes Schneider},
title = {Agile vs.\ structured distributed software development: A case study},
journal = {Empirical Software Engineering},
year = {2014},
volume = {19},
number = {5},
pages = {1197--1224},
month = {October},
publisher = {Springer},
note = {Online since August 2013}
}


Nadia Polikarpova, Carlo A. Furia, and Scott West.
To Run What No One Has Run Before: Executing an Intermediate Verification Language.
In Proceedings of the 4th International Conference on Runtime Verification (RV).
Lecture Notes in Computer Science, 8174:251–268, Springer, September 2013.

Abstract
When program verification fails, it is often hard to understand what went wrong in the absence of concrete executions that expose parts of the implementation or specification responsible for the failure. Automatic generation of such tests would require "executing" the complex specifications typically used for verification (with unbounded quantification and other expressive constructs), something beyond the capabilities of standard testing tools.
This paper presents a technique to automatically generate executions of programs annotated with complex specifications, and its implementation for the Boogie intermediate verification language. Our approach combines symbolic execution and SMT constraint solving to generate small tests that are easy to read and understand. The evaluation on several program verification examples demonstrates that our test case generation technique can help understand failed verification attempts in conditions where traditional testing is not applicable, thus making formal verification techniques easier to use in practice.

@InProceedings{PFW-RV13,
author = {Nadia Polikarpova and Carlo A. Furia and Scott West},
title = {To Run What No One Has Run Before: Executing an Intermediate Verification Language},
booktitle = {Proceedings of the 4th International Conference on Runtime Verification (RV)},
year = {2013},
editor = {Axel Legay and Saddek Bensalem},
series = {Lecture Notes in Computer Science},
pages = {251--268},
volume = {8174},
month = {September},
publisher = {Springer},
acceptancerate = {41\%}
}


Marco Piccioni, Carlo A. Furia, and Bertrand Meyer.
An Empirical Study of API Usability.
In Proceedings of the 7th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM).
Pgg. 5–14, IEEE Computer Society, October 2013.

Abstract
Modern software development extensively involves reusing library components accessed through their Application Programming Interfaces (APIs). Usability is therefore a fundamental goal of API design, but rigorous empirical studies of API usability are still relatively uncommon. In this paper, we present the design of an API usability study which combines interview questions, based on the cognitive dimensions framework, with systematic observations of programmer behavior while solving programming tasks, based on "tokens". We also discuss the implementation of the study to assess the usability of a persistence library API (offering functionalities such as storing objects into relational databases). The study involved 25 programmers (including students, researchers, and professionals), and provided additional evidence to some critical features evidenced by related studies, such as the difficulty of finding good names for API features and of discovering relations between API types. It also discovered new issues relevant to API design, such as the impact of flexibility, and confirmed the crucial importance of accurate documentation for usability.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{PFM-ESEM13,
author = {Marco Piccioni and Carlo A. Furia and Bertrand Meyer},
title = {An Empirical Study of {API} Usability},
booktitle = {Proceedings of the 7th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM)},
editor    = {Forrest Shull and Carolyn Seaman and Guilherme Horta Travassos and Oscar Pastor and Clemente Izurieta and Emilia Mendes and Lorin Hochstein},
pages = {5--14},
year = {2013},
month = {October},
publisher = {IEEE Computer Society},
acceptancerate = {27\%}
}


Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Program Checking With Less Hassle.
In Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013).
Lecture Notes in Computer Science, 8164:149–169, Springer, 2014.

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

@InProceedings{TFNM-VSTTE13,
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Program Checking With Less Hassle},
booktitle = {Proceedings of the 5th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013)},
year = {2014},
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
pages = {149--169},
volume = {8164},
publisher = {Springer},
acceptancerate = {48\%}
}


H.-Christian Estler, Martin Nordio, Carlo A. Furia, and Bertrand Meyer.
Collaborative Debugging.
In Proceedings of the 8th International Conference on Global Software Engineering (ICGSE).
Pgg. 110–119, IEEE Computer Society, August 2013.

Abstract
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 VisualStudio, 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.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• This paper won the best paper award at ICGSE 2013.
• CDB is part of the CloudStudio web-based IDE.
@InProceedings{ENFM-ICGSE13,
author = {H.-Christian Estler and Martin Nordio and Carlo A. Furia and Bertrand Meyer},
title = {Collaborative Debugging},
booktitle = {Proceedings of the 8th International Conference on Global Software Engineering (ICGSE)},
editor    = {Marcelo Cataldo and J{\"u}rgen M{\"u}nch and Filippo Lanubile},
pages = {110--119},
year = {2013},
month = {August},
publisher = {IEEE Computer Society},
acceptancerate = {34\%},
note = {Best paper award}
}


Marco Trudel, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Really Automatic Scalable Object-Oriented Reengineering.
In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP).
Lecture Notes in Computer Science, 7920:477–501, Springer, July 2013.

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

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• AutoOO has been successfully evaluated by the ECOOP artifact evaluation committee and found to meet expectations.
• It has also been invited to ECOOP's Demonstrations satellite event.
• AutoOO is freely available for download as part of the C2Eif project.
@InProceedings{TFNM-ECOOP13,
author = {Marco Trudel and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Really Automatic Scalable Object-Oriented Reengineering},
booktitle = {Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP)},
year = {2013},
editor = {Giuseppe Castagna},
series = {Lecture Notes in Computer Science},
pages = {477--501},
volume = {7920},
month = {July},
publisher = {Springer},
acceptancerate = {25\%}
}


H.-Christian Estler, Martin Nordio, Carlo A. Furia, and Bertrand Meyer.
Unifying Configuration Management with Merge Conflict Detection and Awareness Systems.
In Proceedings of the 22nd Australasian Software Engineering Conference (ASWEC).
Pgg. 201–210, IEEE Computer Society, June 2013.

Abstract
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 CloudStudio, a collaboration framework that integrates a fine-grained software configuration management model and a real-time awareness system. CloudStudio'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 CloudStudio and a case study that demonstrates the usability of the approach for collaborative software development.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• This technical report describes a preliminary version of the work; it is superseded by this conference paper.
• The CloudStudio web-based IDE is available online.
@InProceedings{ENFM-ASWEC13,
author = {H.-Christian Estler and Martin Nordio and Carlo A. Furia and Bertrand Meyer},
title = {Unifying Configuration Management with Merge Conflict Detection and Awareness Systems},
booktitle = {Proceedings of the 22nd Australasian Software Engineering Conference (ASWEC)},
editor    = {Jens Dietrich and James Noble},
pages = {201--210},
year = {2013},
month = {June},
publisher = {IEEE Computer Society},
acceptancerate = {39\%}
}


Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, and Bertrand Meyer.
What Good Are Strong Specifications?.
In Proceedings of the 35th International Conference on Software Engineering (ICSE).
Pgg. 257–266, ACM, May 2013.

Abstract
Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and run-time performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a "sweet spot" with a favorable benefit to effort ratio.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• An extended version of the paper is available as technical report.
• A repository with supplementary material of the case study. The instrumentation tool runmbc (pun unintended) used for the paper's experiments is available as part of EiffelBase2.
• Nadia also prepared a stylish teaser video.
@InProceedings{PFPWM-ICSE13,
author = {Nadia Polikarpova and Carlo A. Furia and Yu Pei and Yi Wei and Bertrand Meyer},
title = {What Good Are Strong Specifications?},
booktitle = {Proceedings of the 35th International Conference on Software Engineering (ICSE)},
pages = {257--266},
year = {2013},
editor = {David Notkin and Betty H.C. Cheng and Klaus Pohl},
month = {May},
publisher = {ACM},
acceptancerate = {18\%}
}


Martin Nordio, Cristiano Calcagno, and Carlo A. Furia.
Javanni: A Verifier for JavaScript.
In Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE).
Lecture Notes in Computer Science, 7793:231–234, Springer, March 2013 (Tool demonstration paper).

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

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• A video demo of the tool.
@InProceedings{NCF13-FASE13,
author = {Martin Nordio and Cristiano Calcagno and Carlo A. Furia},
title = {{J}avanni: A Verifier for {J}ava{S}cript},
booktitle = {Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE)},
year = {2013},
editor = {Vittorio Cortellessa and Daniel Varr{\'o}},
series = {Lecture Notes in Computer Science},
pages = {231--234},
volume = {7793},
month = {March},
publisher = {Springer},
note = {Tool demonstration paper},
acceptancerate = {23\%}
}


Carlo A. Furia, Bertrand Meyer, Manuel Oriol, Andrey Tikhomirov, and Yi Wei.
The Search for the Laws of Automatic Random Testing.
In Proceedings of the 28th ACM Symposium on Applied Computing (SAC 2013), Software Verification and Testing Track.
Pgg. 1214–1219, ACM, March 2013.

Abstract
Can one estimate the number of remaining faults in a software system? A credible estimation technique would be immensely useful to project managers as well as customers. It would also be of theoretical interest, as a general law of software engineering. We investigate possible answers in the context of automated random testing, a method that is increasingly accepted as an effective way to discover faults. Our experimental results, derived from best-fit analysis of a variety of mathematical functions, based on a large number of automated tests of library code equipped with automated oracles in the form of contracts, suggest a poly-logarithmic law. Although further confirmation remains necessary on different code bases and testing techniques, we argue that understanding the laws of testing may bring significant benefits for estimating the number of detectable faults and comparing different projects and practices.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• An extended version is available as technical report.
@InProceedings{FMOTW13-SAC13,
author = {Carlo A. Furia and Bertrand Meyer and Manuel Oriol and Andrey Tikhomirov and Yi Wei},
title = {The Search for the Laws of Automatic Random Testing},
booktitle = {Proceedings of the 28th ACM Symposium on Applied Computing (SAC 2013)},
pages = {1214--1219},
year = {2013},
month = {March},
publisher = {ACM},
note = {Software Verification and Testing Track},
acceptancerate = {23\%}
}


Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.
In Tools for Practical Software Verification – LASER 2011, International Summer School.
Lecture Notes in Computer Science, 7682:133–155, Springer, 2012.

Abstract
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper discusses some techniques used in AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof's translation, including some whose implementation is underway, and demonstrates them with examples and a case study.

@InProceedings{TFNM12-LASER11,
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Automatic Verification of Advanced Object-Oriented Features: The {AutoProof} Approach},
booktitle = {Tools for Practical Software Verification -- LASER 2011, International Summer School},
pages = {133--155},
year = {2012},
editor = {Bertrand Meyer and Martin Nordio},
volume = {7682},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}


Marco Trudel, Carlo A. Furia, Martin Nordio, Bertrand Meyer, and Manuel Oriol.
C to O-O Translation: Beyond the Easy Stuff.
In Proceedings of the 19th Working Conference on Reverse Engineering (WCRE'12).
Pgg. 19–28, IEEE Computer Society, October 2012.

Abstract
Can we reuse some of the huge code-base developed in C to take advantage of modern programming language features such as type safety, object-orientation, and contracts? This paper presents a source-to-source translation of C code into Eiffel, a modern object-oriented programming language, and the supporting tool C2Eif. The translation is completely automatic and supports the entire C language (ANSI, as well as many GNU C Compiler extensions, through CIL) as used in practice, including its usage of native system libraries and inlined assembly code. Our experiments show that C2Eif can handle C applications and libraries of significant size (such as vim and libgsl), as well as challenging benchmarks such as the GCC torture tests. The produced Eiffel code is functionally equivalent to the original C code, and takes advantage of some of Eiffel's features to produce safe and easy-to-debug translations.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• An extended version of the paper is available as technical report.
• The C2Eif project page.
• Marco Trudel's spinoff company mtSystems offers C translation services based on some of the techniques first described in this paper (as well as in the companion papers WCRE'12 tool demo and ECOOP'13).
@InProceedings{TFNMO12-WCRE12,
author = {Marco Trudel and Carlo A. Furia and Martin Nordio and Bertrand Meyer and Manuel Oriol},
title = {{C} to {O-O} Translation: Beyond the Easy Stuff},
booktitle = {Proceedings of the 19th Working Conference on Reverse Engineering (WCRE'12)},
editor    = {Rocco Oliveto and Denys Poshyvanyk and James Cordy and Thomas Dean},
pages = {19--28},
year = {2012},
month = {October},
publisher = {IEEE Computer Society},
acceptancerate = {33\%}
}


Marco Trudel, Carlo A. Furia, and Martin Nordio.
Automatic C to O-O Translation with C2Eiffel.
In Proceedings of the 19th Working Conference on Reverse Engineering (WCRE'12).
Tool demonstration paper, pgg. 508–509, IEEE Computer Society, October 2012.

Abstract
C2Eiffel is a fully automatic source-to-source translator of C applications into the Eiffel object-oriented programming language. C2Eiffel supports the complete C language, including function pointers, unrestricted pointer arithmetic and jumps, arbitrary native libraries, and inlined assembly code. It produces readable Eiffel code that behaves as the source C application; it takes advantage of some of Eiffel's object-oriented features to produce translations that are easy to maintain and debug, and often even safer than their sources thanks to stricter correctness checks introduced automatically. Experiments show that C2Eiffel handles C applications of significant size (such as vim and libgsl); it is a fully automatic tool suitable to reuse C code within a high-level object-oriented programming language.

@InProceedings{TFN12-WCRE12-tool,
author = {Marco Trudel and Carlo A. Furia and Martin Nordio},
title = {Automatic {C} to {O-O} Translation with {C2Eiffel}},
booktitle = {Proceedings of the 19th Working Conference on Reverse Engineering (WCRE'12)},
editor    = {Rocco Oliveto and Denys Poshyvanyk and James Cordy and Thomas Dean},
pages = {508--509},
year = {2012},
month = {October},
publisher = {IEEE Computer Society},
note = {Tool demonstration paper}
}


Carlo A. Furia.
A Verifier for Functional Properties of Sequence-Manipulating Programs.
In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12).
Lecture Notes in Computer Science, 7561:183–186, Springer, October 2012.

Abstract
Many programs operate on data structures whose models are sequences, such as arrays, lists, and queues. When specifying and verifying functional properties of such programs, it is convenient to use an assertion language and a reasoning engine that incorporate sequences natively. This paper presents qfis, a program verifier geared to sequence-manipulating programs. qfis is a command-line tool that inputs annotated programs, generates the verification conditions that establish their correctness, tries to discharge them by calls to the SMT-solver CVC3, and reports the outcome back to the user. qfis can be used directly or as a back-end of more complex programming languages.

• The tool paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{Fur12-ATVA12,
author = {Carlo A. Furia},
title = {A Verifier for Functional Properties of Sequence-Manipulating Programs},
booktitle = {Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12)},
pages = {183--186},
year = {2012},
editor = {Supratik Chakraborty and Madhavan Mukund},
volume = {7561},
series = {Lecture Notes in Computer Science},
month = {October},
publisher = {Springer},
note = {Tool paper},
acceptancerate = {32\%}
}


Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi.
Modeling Time in Computing.
Monographs in Theoretical Computer Science. An EATCS series. Springer, 2012.

From the Preface
Time has become a part of computing, where it has claimed its own models. This book summarizes several decades of research on developing, analyzing, and applying time models to computing and, more generally, engineering.
Every researcher contributing to such a burgeoning field is forced to consider several available approaches, to understand what they have in common and how they differ. This continued effort prompts a systematic work of comparison, classification, and assessment of the diverse models and methods. This book picks up this call and tries to put it into practice.

an introduction and overview of the book.
2. Languages and interpretations:
what is a modeling language; and a crash course on logic.
3. Dimensions of the time modeling problem:
fundamental features of time modeling: discrete vs. dense time, deterministic vs. nondeterministic, time advancement, etc.
4. Dynamical systems:
the attributes of time in classic dynamical system theory.
5. Time in hardware modeling and design:
how time is modeled from transistors to asynchronous and synchronous logic circuits.
6. Time in the analysis of algorithms:
measures of time in computational complexity and automata theory.
7. Synchronous abstract machines:
transition systems, finite-state automata, Statecharts, timed automata, etc.
8. Asynchronous abstract machines: Petri nets:
Petri nets: untimed, timed, and stochastic.
9. Logic-based formalisms:
temporal logics: linear, branching, metric, interval-based, explicit-time, probabilistic, etc.
10. Algebraic formalisms:
Communicating Sequential Processes: untimed, timed, and stochastic.
11. Dual-language approaches:
the model-checking paradigm, TTM/RTTL, and TRIO-Petri nets.
12. Time is up:
conclusive remarks.
• The book is available online (in electronic and printed versions) from Springer's website.
@Book{FMMR-TimeBook-12,
author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi},
title = {Modeling Time in Computing},
publisher = {Springer},
year = {2012},
series = {Monographs in Theoretical Computer Science. An EATCS series},
isbn = {978-3-642-32331-7}
}


Carlo A. Furia and Sebastian Nanz.
TOOLS Europe 2012 Special Section (editorial).
Journal of Object Technology, Volume 12(3), August 2013.

@article{FN-JOT-TOOLSEurope12,
author = {Carlo A. Furia and Sebastian Nanz},
title = {{TOOLS Europe} 2012 Special Section},
journal = {Journal of Object Technology},
volume = {12},
number = {3},
month = {August},
year = {2013},
note = {(editorial)}
}


Carlo A. Furia and Sebastian Nanz, editors.
Objects, Models, Components, Patterns – 50th International Conference, TOOLS 2012, Prague, Czech Republic, May 29–31, 2012. Proceedings.
Springer, 2012.

From the Preface
Started in 1989, the TOOLS conference series has played a major role in the development of object technology and, with its emphasis on practically useful results, has contributed to making it mainstream and ubiquitous. This year's 50th edition of the International Conference on Objects, Models, Components, Patterns (TOOLS Europe 2012) appropriately celebrated this "triumph of objects": object technology is now commonplace.

@proceedings{FN-TOOLSEurope12,
editor    = {Carlo A. Furia and
Sebastian Nanz},
title     = {Objects, Models, Components, Patterns -- 50th International
Conference, TOOLS 2012, Prague, Czech Republic, May 29--31,
2012. Proceedings},
booktitle = {TOOLS (50)},
publisher = {Springer},
series    = {Lecture Notes in Computer Science},
volume    = {7304},
year      = {2012}
}


Carlo A. Furia and Paola Spoletini.
Automata-based Verification of Linear Temporal Logic Models with Bounded Variability.
In Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12).
Pgg. 89–96, IEEE Computer Society, September 2012.

Abstract
A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information—through the usage of next operators—can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into Büchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{FS12-TIME12,
author = {Carlo A. Furia and Paola Spoletini},
title = {Automata-based Verification of Linear Temporal Logic Models with Bounded Variability},
booktitle = {Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12)},
editor    = {Ben Moszkowski and Mark Reynolds and Paolo Terenziani},
pages = {89--96},
year = {2012},
month = {September},
publisher = {IEEE Computer Society},
acceptancerate = {50\%}
}


H.-Christian Estler, Martin Nordio, Carlo A. Furia, Bertrand Meyer, and Johannes Schneider.
Agile vs. Structured Distributed Software Development: A Case Study.
In Proceedings of the 7th International Conference on Global Software Engineering (ICGSE'12).
Pgg. 11–20, IEEE Computer Society, August 2012.

Abstract
This paper presents a case study on the impact of development processes on the success of globally distributed software projects. The study compares agile (Scrum, XP, etc.) vs. structured (RUP, waterfall) processes to determine if the choice of process impacts: the overall success and economic savings of distributed projects; the importance customers attribute to projects; the motivation of the development teams; and the amount of real-time or asynchronous communication required during project development.
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 some common critical aspects.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• This paper won the best paper award at ICGSE 2012.
@InProceedings{ENFMS-ICGSE12,
author = {H.-Christian Estler and Martin Nordio and Carlo A. Furia and Bertrand Meyer and Johannes Schneider},
title = {Agile vs.\ Structured Distributed Software Development: A Case Study},
booktitle = {Proceedings of the 7th International Conference on Global Software Engineering (ICGSE'12)},
editor    = {Erran Carmel and Rini {van Solingen}},
pages = {11--20},
year = {2012},
month = {August},
publisher = {IEEE Computer Society},
acceptancerate = {25\%},
note = {Best paper award}
}


Yi Wei, Hannes Roth, Carlo A. Furia, Yu Pei, Alexander Horton, Michael Steindorfer, Martin Nordio, and Bertrand Meyer
Stateful Testing: Finding More Errors in Code and Contracts.
In Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11).
Pgg. 440–443, ACM, November 2011.

Abstract
Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new errors, and also to improve the accuracy of the inferred contracts by discovering those that are unsound.
Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead.

@InProceedings{WRFPHSNM-ASE11,
author = {Yi Wei and Hannes Roth and Carlo A. Furia and Yu Pei and Alexander Horton and Michael Steindorfer and Martin Nordio and Bertrand Meyer},
title = {Stateful Testing: Finding More Errors in Code and Contracts},
booktitle = {Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)},
editor    = {Perry Alexander and Corina Pasareanu and John Hosking},
pages = {440--443},
year = {2011},
month = {November},
publisher = {ACM},
acceptancerate = {43\%}
}


Yu Pei, Yi Wei, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Code-Based Automated Program Fixing.
In Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11).
Pgg. 392–395, ACM, November 2011.

Abstract
Many programmers, when they encounter an error, would like to have the benefit of automatic fix suggestions—as long as they are, most of the time, adequate. Initial research in this direction has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches.
To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of dynamic analysis to gather evidence on the values taken by expressions derived from the program text.
The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches.

@InProceedings{PWFNM11-ASE11,
author = {Yu Pei and Yi Wei and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Code-Based Automated Program Fixing},
booktitle = {Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)},
editor    = {Perry Alexander and Corina Pasareanu and John Hosking},
pages = {392--395},
year = {2011},
month = {November},
publisher = {ACM},
acceptancerate = {43\%}
}


Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques.
In 9th International Conference on Software Engineering and Formal Methods (SEFM'11).
Lecture Notes in Computer Science, 7041:382–398, Springer, November 2011.

Abstract
With formal techniques becoming more and more powerful, the next big challenge is making software verification practical and usable. The Eve verification environment contributes to this goal by seamlessly integrating a static prover and an automatic testing tool into a development environment. The paper discusses the general principles behind the integration of heterogeneous verification tools; the peculiar challenges involved in combining static proofs and dynamic testing techniques; and how the combination, implemented in Eve through a blackboard architecture, can improve the user experience with little overhead over usual development practices. Eve is freely available for download.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• The Eve project page.
@InProceedings{TFNM11-SEFM11,
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques},
booktitle = {9th International Conference on Software Engineering and Formal Methods ({SEFM}'11)},
pages = {382--398},
year = {2011},
editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
volume = {7041},
series = {Lecture Notes in Computer Science},
month = {November},
publisher = {Springer},
acceptancerate = {28\%}
}


Carlo A. Furia and Paola Spoletini.
On Relaxing Metric Information in Linear Temporal Logic.
In Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME'11).
Pgg. 72–79, IEEE Computer Society, September 2011.

Abstract
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• Some technical details, that are omitted in the paper, can be found in this technical report.
@InProceedings{FS11-TIME11,
author = {Carlo A. Furia and Paola Spoletini},
title = {On Relaxing Metric Information in Linear Temporal Logic},
booktitle = {Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME'11)},
editor    = {Carlo Combi and Martin Leucker and Frank Wolter},
pages = {72--79},
year = {2011},
month = {September},
publisher = {IEEE Computer Society},
acceptancerate = {44\%}
}


Marco Trudel, Manuel Oriol, Carlo A. Furia, and Martin Nordio.
Automated Translation of Java Source Code to Eiffel.
In Objects, Components, Models, Patterns. 49th International Conference, TOOLS Europe 2011.
Lecture Notes in Computer Science, 6705:20–35, Springer, June 2011.

Abstract
Reusability is an important software engineering concept actively advocated for the last forty years. While reusability has been addressed for systems implemented using the same programming language, it does not usually handle interoperability with different programming languages. This paper presents a solution for the reuse of Java code within Eiffel programs based on a source-to-source translation from Java to Eiffel. The paper focuses on the critical aspects of the translation and illustrates them by formal means. The translation is implemented in the freely available tool J2Eif; it provides Eiffel replacements for the components of the Java runtime environment, including Java Native Interface services and reflection mechanisms. Our experiments demonstrate the practical usability of the translation scheme and its implementation, and record the performance slow-down compared to custom-made Eiffel applications: automatic translations of java.util data structures, java.io services, and SWT applications can be re-used as Eiffel programs, with the same functionalities as their original Java implementations.

@InProceedings{TOFN11-TOOLS11,
author = {Marco Trudel and Manuel Oriol and Carlo A. Furia and Martin Nordio},
title = {Automated Translation of {J}ava Source Code to {E}iffel},
booktitle = {Objects, Components, Models, Patterns. 49th International Conference, {TOOLS} Europe 2011},
pages = {20--35},
year = {2011},
editor = {Judith Bishop and Antonio Vallecillo},
volume = {6705},
series = {Lecture Notes in Computer Science},
month = {June},
publisher = {Springer},
acceptancerate = {28\%}
}


Yi Wei, Carlo A. Furia, Nikolay Kazmin, and Bertrand Meyer.
Inferring Better Contracts.
In Proceedings of the 33rd International Conference on Software Engineering (ICSE'11).
Pgg. 191–200, ACM, May 2010.

Abstract
Considerable progress has been made towards automatic support for one of the principal techniques available to enhance program reliability: equipping programs with extensive contracts. The results of current contract inference tools are still often unsatisfactory in practice, especially for programmers who already apply some kind of basic Design by Contract discipline, since the inferred contracts tend to be simple assertions—the very ones that programmers find easy to write. We present new, completely automatic inference techniques and a supporting tool, which take advantage of the presence of simple programmer-written contracts in the code to infer sophisticated assertions, involving for example implication and universal quantification.
Applied to a production library of classes covering standard data structures such as linked lists, arrays, stacks, queues and hash tables, the tool is able, entirely automatically, to infer 75% of the complete contracts—contracts yielding the full formal specification of the classes—with very few redundant or irrelevant clauses.

@InProceedings{WFKM11-ICSE11,
author = {Yi Wei and Carlo A. Furia and Nikolay Kazmin and Bertrand Meyer},
title = {Inferring Better Contracts},
booktitle = {Proceedings of the 33rd International Conference on Software Engineering (ICSE'11)},
editor    = {Richard N. Taylor and Harald Gall and Nenad Medvidovi{\' c}},
pages = {191--200},
year = {2011},
month = {May},
publisher = {ACM},
acceptancerate = {14\%}
}


Carlo A. Furia and Matteo Rossi.
A Theory of Sampling for Continuous-Time Metric Temporal Logic.
ACM Transactions on Computational Logic, 12(1):1–40, October 2010.

Abstract
This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to "flat" formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• A previous version is available as technical report.
@Article{FR10-TOCL10,
author = {Carlo A. Furia and Matteo Rossi},
title = {A Theory of Sampling for Continuous-Time Metric Temporal Logic},
journal = {ACM Transactions on Computational Logic},
volume = {12},
number = {1},
year = {2010},
pages = {1--40},
publisher = {ACM},
month = {October},
note = {Article 8}
}


Carlo A. Furia and Bertrand Meyer.
Inferring Loop Invariants Using Postconditions.
In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday.
Lecture Notes in Computer Science, 6300:277–300, Springer, August 2010.

Abstract
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• A previous version is available as technical report.
@InProceedings{FM10-YG70-post,
author = {Carlo A. Furia and Bertrand Meyer},
title = {Inferring Loop Invariants Using Postconditions},
booktitle = {Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday},
pages = {277--300},
year = {2010},
editor = {Andreas Blass and Nachum Dershowitz and Wolfgang Reisig},
volume = {6300},
series = {Lecture Notes in Computer Science},
month = {August},
publisher = {Springer}
}


Carlo A. Furia.
In Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10).
Lecture Notes in Computer Science, 6252:128–142, Springer-Verlag, September 2010.

Abstract
We present a first-order theory of (finite) sequences with integer elements, Presburger arithmetic, and regularity constraints, which can model significant properties of data structures such as lists and queues. We give a decision procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., "for all even i's, the element at position i has value i+3 or 2i"). The resulting expressive power is orthogonal to that of the most expressive decidable logics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
• Some technical details, that are omitted in the paper, can be found in this technical report.
• In Section 4 of the published paper, the verification condition for the Mergesort example is incorrect; the version available here corrects the lapses. The rest of the paper is, in any case, unaffected.
• QFIS is a prototype tool for the theory of sequences described in the paper. You can download QFIS and read its user manual.
@InProceedings{Fur10-ATVA10,
author = {Carlo A. Furia},
title = {What's Decidable About Sequences?},
booktitle = {Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10)},
pages = {128--142},
year = {2010},
editor = {Ahmed Bouajjani and Wei-Ngan Chin},
volume = {6252},
series = {Lecture Notes in Computer Science},
month = {September},
publisher = {Springer},
acceptancerate = {41\%}
}


Dino Mandrioli, Stephen Fickas, Carlo A. Furia, Mehdi Jazayeri, Matteo Rossi, and Michal Young.
SCORE: the first student contest on software engineering.
SIGSOFT Software Engineering Notes 35(4):24–30, July 2010.

Abstract
The Student Contest on Software Engineering (SCORE), organized for the first time in conjunction with the International Conference on Software Engineering (ICSE) 2009, attracted 50 student teams from around the world, produced an impressive and varied set of projects, and earned appreciative comments from participants and even from teams who chose not to submit their results to the competition. It was a remarkable success, but not without problems and setbacks. In this article we explain the objectives, constraints, and design philosophy of SCORE, particularly as they distinguish it from the tradition of computer science contests focused more narrowly on programming. We also recount key approaches taken to design and management of this novel kind of contest, the difficulties we met (some still outstanding), and the lessons learned.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@Article{MFFJRY10-SEN10,
author = {Dino Mandrioli and Stephen Fickas and Carlo A. Furia and Mehdi Jazayeri and Matteo Rossi and Michal Young},
title = {{SCORE}: the first student contest on software engineering},
journal = {SIGSOFT Software Engineering Notes},
year = {2010},
volume = {35},
number = {4},
pages = {24--30},
month = {July}
}


Nadia Polikarpova, Carlo A. Furia, and Bertrand Meyer.
Specifying Reusable Components.
In Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10).
Lecture Notes in Computer Science, 6217:127–141, Springer-Verlag, August 2010.

Abstract
Reusable software components need expressive specifications. This paper outlines a rigorous foundation of model-based contracts, a method to equip classes with strong contracts that support accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract approach with a notion of model, which underpins the precise definitions of such concepts as abstract object equivalence and specification completeness. Experiments applying model-based contracts to libraries of data structures suggest that the method enables accurate specification of practical software.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{PFM10-VSTTE10,
author = {Nadia Polikarpova and Carlo A. Furia and Bertrand Meyer},
title = {Specifying Reusable Components},
booktitle = {Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10)},
pages = {127--141},
year = {2010},
editor = {Gary T. Leavens and Peter O'Hearn and Sriram Rajamani},
volume = {6217},
series = {Lecture Notes in Computer Science},
month = {August},
publisher = {Springer},
acceptancerate = {36\%}
}


Yi Wei, Yu Pei, Carlo A. Furia, Lucas S. Silva, Stefan Buchholz, Bertrand Meyer, and Andreas Zeller.
Automated Fixing of Programs with Contracts.
In Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA'10).
Pgg. 61–72, ACM, July 2010.

Abstract
In program debugging, finding a failing run is only the first step; what about correcting the fault? Can we automate the second task as well as the first? The AutoFix-E tool automatically generates and validates fixes for software faults. The key insights behind AutoFix-E are to rely on contracts present in the software to ensure that the proposed fixes are semantically sound, and on state diagrams using an abstract notion of state based on the boolean queries of a class.
Out of 42 faults found by an automatic testing tool in two widely used Eiffel libraries, AutoFix-E proposes successful fixes for 16 faults. Submitting some of these faults to experts shows that several of the proposed fixes are identical or close to fixes proposed by humans.

@InProceedings{WPFSBMZ10-ISSTA10,
author = {Yi Wei and Yu Pei and Carlo A. Furia and Lucas S. Silva and Stefan Buchholz and Bertrand Meyer and Andreas Zeller},
title = {Automated Fixing of Programs with Contracts},
booktitle = {Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA'10)},
editor    = {Paolo Tonella and Alessandro Orso},
pages = {61--72},
year = {2010},
month = {July},
publisher = {ACM},
acceptancerate = {23\%}
}


Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi.
Modeling Time in Computing: a taxonomy and a comparative survey.
ACM Computing Surveys, 42(2):1–59, February 2010.

Abstract
The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a growing attention to the temporal aspects of computing, not only in the computer science domain, but also in more traditional fields of engineering.
This article surveys various approaches to the formal modeling and analysis of the temporal features of computer-based systems, with a level of detail that is also suitable for nonspecialists. In doing so, it provides a unifying framework, rather than just a comprehensive list of formalisms.
The article first lays out some key dimensions along which the various formalisms can be evaluated and compared. Then, a significant sample of formalisms for time modeling in computing are presented and discussed according to these dimensions. The adopted perspective is, to some extent, historical, going from "traditional" models and formalisms to more modern ones.

@Article{FMMR10-CSUR10,
author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi},
title = {Modeling Time in Computing: a taxonomy and a comparative survey},
journal = {ACM Computing Surveys},
volume = {42},
number = {2},
year = {2010},
pages = {1--59},
publisher = {ACM},
month = {February},
note = {Article 6}
}


Luca Cavallaro, Elisabetta Di Nitto, Carlo A. Furia, and Matteo Pradella.
A Tile-based Approach for Self-assembling Service Compositions.
In Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10).
Pgg. 43–52, IEEE, March 2010.

Abstract
This paper presents a novel approach to the design of self-adaptive service-oriented applications based on a new model called service tiles. The approach allows designers to develop a service-oriented system by building an assembly of component services that accomplishes the given goal. The assembly is computed automatically starting from the specification of a subset of the whole system, a few constraints, and the goals the application should fulfill. An application designed according to the service-tile model can also dynamically self-adapt by replacing, in part or entirely, services in the assembly whenever they fail or the application context changes. The service-tile design technique has been implemented in a prototype and some experiments with several examples demonstrate the feasibility of the approach and its practical efficiency.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{CDFP10-ICECCS10,
author = {Luca Cavallaro and Elisabetta {Di Nitto} and Carlo A. Furia and Matteo Pradella},
title = {A Tile-based Approach for Self-assembling Service Compositions},
booktitle = {Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10)},
pages = {43--52},
year = {2010},
month = {March},
publisher = {IEEE},
acceptancerate = {23\%}
}


Silvia Bindelli, Elisabetta Di Nitto, Carlo A. Furia, and Matteo Rossi.
Using Compositionality to Formally Model and Analyze Systems Built of a High Number of Components.
In Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10).
Pgg. 85–94, IEEE, March 2010.

Abstract
When dependability of systems with a large number of components is a concern, being able to model and analyze their properties, especially non-functional ones, in a formal and automated way becomes essential. Often, however, the application of formal methods and automated reasoning is seen by practitioners as complex and time consuming. Compositional techniques can help modify this belief.
In this paper we show how a compositional modeling and verification technique can be applied to the analysis of distributed systems with numerous interacting nodes. We automate the proof by exploiting a SAT-based tool. We demonstrate the validity of the resulting approach by applying it to an autonomic service-based system that manages, in a coordinated peer-to-peer manner, electricity consumption in a geographical area. In particular, we show that in this case the time needed for performing the proof is remarkably shorter than in the case in which we adopt a non-compositional approach.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{BDFR10-ICECCS10,
author = {Silvia Bindelli and Elisabetta {Di Nitto} and Carlo A. Furia and Matteo Rossi},
title = {Using Compositionality to Formally Model and Analyze Systems Built of a High Number of Components},
booktitle = {Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10)},
pages = {85--94},
year = {2010},
month = {March},
publisher = {IEEE},
acceptancerate = {23\%}
}


Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms.
In Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09).
Pgg. 13–22, IEEE Computer Society Press, November 2009.

Abstract
In this paper we present a technique to model different aspects of the same system with different formalisms, while keeping the various models tightly integrated with one another. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms can be better suited to describe different aspects of complex systems. While each paradigm provides a different view on the many facets of the system, it is of paramount importance that a coherent comprehensive model emerges from the combination of the various partial descriptions. Our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the Boolean satisfiability (SAT) problem; this allows users to carry out formal verification activities both on the whole model and on parts thereof. The effectiveness of the approach is illustrated through the example of a monitoring system.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{BFPR09-SEFM09,
author = {Marcello M. Bersani and Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms},
booktitle = {Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09)},
pages = {13--22},
year = {2009},
month = {November},
publisher = {IEEE Computer Society Press},
acceptancerate = {35\%}
}


Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Comments on "Temporal Logics for Real-Time System Specification".
ACM Computing Surveys, 41(2):1–5, February 2009.

Abstract
The article "Temporal Logics for Real-Time System Specification" surveys some of the relevant literature dealing with the use of temporal logics for the specification of real-time systems. Unfortunately, it introduces some imprecisions that mightcreate some confusion in the reader. While a certain degree of informality is certainly useful when addressing a broad audience, imprecisions can negatively impact the legibility of the exposition. We clarify some of its remarks on a few topics, in an effort to contribute to the usefulness of the survey for the reader.

• The paper in PDF format (updated, improved, and extended text, also published as technical report) and its DOI.

Notes
Publication timeline: Received September 2005; revised July 2007, April 2008; accepted April 2008.

@Article{FPR09-CSUR09,
author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Comments on {T}emporal Logics for Real-Time System Specification'},
journal = {ACM Computing Surveys},
volume = {41},
number = {2},
year = {2009},
pages = {1--5},
publisher = {ACM},
month = {February},
note = {Extended version as Technical Report 2008.7, Dipartimento di Elettronica e Informazione, Politecnico di Milano, April 2008}
}


Carlo A. Furia and Paola Spoletini.
Practical Efficient Modular Linear-Time Model-Checking.
In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08).
Lecture Notes in Computer Science, 5311:408–417, Springer-Verlag, October 2008.

Abstract
This paper shows how the modular structure of composite systems can guide the state-space exploration in explicit-state linear-time model-checking and make it more efficient in practice. Given a composite system where every module has input and output variables — and variables of different modules can be connected — a total ordering according to which variables are generated is determined, through heuristics based on graph-theoretical analysis of the modular structure. The technique is shown to outperform standard exploration techniques (that do not take the modular structure information into account) by several orders of magnitude in experiments with Spin models of MTL formulas.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{FS08-ATVA08,
author = {Carlo A. Furia and Paola Spoletini},
title = {Practical Efficient Modular Linear-Time Model-Checking},
booktitle = {Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)},
pages = {408--417},
year = {2008},
editor = {Sungdeok (Steve) Cha and Jin-Young Choi and Monzoo Kim and Insup Lee and Mahesh Viswanathan},
volume = {5311},
series = {Lecture Notes in Computer Science},
month = {October},
publisher = {Springer-Verlag},
acceptancerate = {34\%}
}


Carlo A. Furia and Matteo Rossi.
MTL with Bounded Variability: Decidability and Complexity.
In Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08).
Lecture Notes in Computer Science, 5215:109–123, Springer-Verlag, September 2008.

Abstract
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FR08-FORMATS08,
author = {Carlo A. Furia and Matteo Rossi},
title = {{MTL} with Bounded Variability: Decidability and Complexity},
booktitle = {Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08)},
pages = {109--123},
year = {2008},
editor = {Franck Cassez and Claude Jard},
volume = {5215},
series = {Lecture Notes in Computer Science},
month = {September},
publisher = {Springer-Verlag},
acceptancerate = {45\%}
}


Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models.
In Proceedings of the 10th International Conference on Formal Engineering Methods (ICFEM'08).
Lecture Notes in Computer Science, 5256:298–317, Springer-Verlag, October 2008.

Abstract
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based) formalisms. The technique relies on the reduction, under reasonable assumptions, of the continuous-time verification problem to its discrete-time counterpart. This reconciles in a viable and effective way the dense/discrete and operational/descriptive dichotomies that are often encountered in practice when it comes to specifying and analyzing complex critical systems. The article investigates the applicability of the technique through a significant example centered on a communication protocol. Concurrent runs of the protocol are formalized by parallel instances of a Timed Automaton, while the synchronization rules between these instances are specified through Metric Temporal Logic formulas, thus creating a multi-paradigm model. Verification tests run on this model using a bounded satisfiability checker implementing the technique show consistent results and interesting performances.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FPR08-ICFEM08,
author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Practical Automated Partial Verification of Multi-Paradigm Real-Time Models},
booktitle = {Proceedings of the 10th International Conference on Formal Engineering Methods (ICFEM'08)},
pages = {298--317},
year = {2008},
editor = {Shaoying Liu and Tom Maibaum and Keijiro Araki},
volume = {5256},
series = {Lecture Notes in Computer Science},
month = {October},
publisher = {Springer-Verlag},
acceptancerate = {32\%}
}


Carlo A. Furia, Marco Mazzucchelli, Paola Spoletini, and Mara Tanelli.
Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation.
In Proceedings of the 9th IEEE International Symposium on Computer-Aided Control System Design (CACSD'08).
Pgg. 1265–1270, IEEE Press, September 2008.

Abstract
In industrial applications, the number of final products endowed with real-time automatic control systems that manage safety-critical situations has dramatically increased. Thus, it is of growing importance that the control system design flow encompasses also its translation into software code and its embedding into a hardware and software network. In this paper, a tool-supported approach to the formal analysis of real-time aspects in controller implementation is proposed. The analysis can ensure that some desired properties of the control loop are preserved in its implementation on a distributed architecture. Moreover, the tool provides as output information which can be used to approach straightforwardly some design problems, such as hardware sizing in the final implementation.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Several technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FMST08-CACSD08,
author = {Carlo A. Furia and Marco Mazzucchelli and Paola Spoletini and Mara Tanelli},
title = {Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation},
booktitle = {Proceedings of the 9th IEEE International Symposium on Computer-Aided Control System Design (CACSD'08)},
pages = {1265--1270},
year = {2008},
month = {September},
publisher = {IEEE Press},
note = {CACSD'08 is part of the 2nd IEEE Multi-conference on Systems and Control}
}


Carlo A. Furia and Paola Spoletini.
Tomorrow and All Our Yesterdays: MTL Satisfiability over the Integers.
In Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08).
Lecture Notes in Computer Science, 5160:126–140, Springer-Verlag, September 2008.

Abstract
We investigate the satisfiability problem for metric temporal logic (MTL) with both past and future operators over linear discrete bi-infinite time models isomorphic to the integer numbers, where time is unbounded both in the future and in the past. We provide a technique to reduce satisfiability over the integers to satisfiability over the well-known mono-infinite time model of natural numbers, and we show how to implement the technique through an automata-theoretic approach. We also prove that MTL satisfiability over the integers is EXPSPACE-complete, hence the given algorithm is optimal in the worst case.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FS08-ICTAC08,
author = {Carlo A. Furia and Paola Spoletini},
title = {Tomorrow and All Our Yesterdays: {MTL} Satisfiability over the Integers},
booktitle = {Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08)},
pages = {126--140},
year = {2008},
editor = {John S. Fitzgerald and Anne E. Haxthausen and Husnu Yenigun},
volume = {5160},
series = {Lecture Notes in Computer Science},
month = {September},
publisher = {Springer-Verlag},
acceptancerate = {38\%}
}


Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Automated Verification of Dense-Time MTL Specifications via Discrete-Time Approximation.
In Proceedings of the 15th International Symposium on Formal Methods (FM'08).
Lecture Notes in Computer Science, 5014:132–147, Springer-Verlag, May 2008.

Abstract
This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [FR06]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers for some formulas. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of the Zot tool for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some results that are promising in terms of performance.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FPR08-FM08,
author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Automated Verification of Dense-Time {MTL} Specifications via Discrete-Time Approximation},
booktitle = {Proceedings of the 15th International Symposium on Formal Methods (FM'08)},
pages = {132--147},
year = {2008},
editor = {Jorge Cu{\'e}llar and Tom Maibaum and Kaisa Sere},
volume = {5014},
series = {Lecture Notes in Computer Science},
month = {May},
publisher = {Springer-Verlag},
acceptancerate = {21\%}
}


Carlo A. Furia and Matteo Rossi.
No Need To Be Strict: on the expressiveness of metric temporal logics with (non-)strict operators.
Bulletin of the European Association for Theoretical Computer Science, 92:150–160, June 2007.

Abstract
The until modality of temporal logic "A until B" is called strict in its first argument when it does not constrain the value of the first argument A at the instant at which the formula is evaluated. In this paper, we show that linear metric temporal logics with bounded until modalities that are non-strict in the first argument are as expressive as those with strict modalities, when interpreted over non-Zeno dense-time models.

• The extended version of the paper in manuscript PDF format (updated, improved, and extended text); and the BEATCS version.
@Article{FR07-BEATCS,
author = {Carlo A. Furia and Matteo Rossi},
title = {No Need To Be Strict: on the expressiveness of metric temporal logics with (non-)strict operators},
journal = {Bulletin of the European Association for Theoretical Computer Science},
year = {2007},
volume = {92},
pages = {150--160},
month = {June}
}


Carlo A. Furia and Matteo Rossi.
On the Expressiveness of MTL Variants over Dense Time.
In Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'07).
Lecture Notes in Computer Science, 4763:163–178, Springer-Verlag, October 2007.

Abstract
The basic modal operator bounded until of Metric Temporal Logic (MTL) comes in several variants. In particular it can be strict (when it does not constrain the current instant) or not, and matching (when it requires its two arguments to eventually hold together) or not. This paper compares the relative expressiveness of the resulting MTL variants over dense time. We prove that the expressiveness is not affected by the variations when considering non-Zeno interpretations and arbitrary nesting of temporal operators. On the contrary, the expressiveness changes for flat (i.e., without nesting) formulas, or when Zeno interpretations are allowed.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FR07-FORMATS07,
author = {Carlo A. Furia and Matteo Rossi},
title = {On the Expressiveness of {MTL} Variants over Dense Time},
booktitle = {Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'07)},
pages = {163--178},
year = {2007},
editor = {Jean-Fran{\c c}ois Raskin and P. S. Thiagarajan},
volume = {4763},
series = {Lecture Notes in Computer Science},
month = {October},
publisher = {Springer-Verlag},
acceptancerate = {45\%}
}


Carlo A. Furia, Matteo Rossi, Dino Mandrioli, and Angelo Morzenti.
Automated Compositional Proofs for Real-Time Systems.
Theoretical Computer Science, 376(3):164–184, May 2007.

Abstract
We present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a methodology concerning the integration of the different parts into a whole system. The reference specification language is the TRIO metric linear temporal logic.
The novelty of our approach with respect to existing compositional frameworks — most of which do not deal explicitly with real-time requirements — consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verification through theorem-proving of modular real-time axiom systems.
As an example of application, we show the verification of a real-time version of the old-fashioned but still relevant "benchmark" of the dining philosophers problem.

• The paper in manuscript PDF format (updated, improved, and extended text) and its DOI.

Notes

• The paper is an extended version of the conference paper with the same title.
• The paper is published in a special issue of TCS with invited papers from FASE 2004 and 2005.
@Article{FRMM07-TCS07,
author = {Carlo A. Furia and Matteo Rossi and Dino Mandrioli and Angelo Morzenti},
title = {Automated Compositional Proofs for Real-Time Systems},
journal = {Theoretical Computer Science},
year = {2007},
volume = {376},
number = {3},
pages = {164--184}
}


Carlo A. Furia, Matteo Rossi, and Dino Mandrioli.
Modeling the Environment in Software-Intensive Systems.
In Proceedings of the Workshop on Modeling in Software Engineering (MISE'07), May 2007.
A Workshop of the 29th International Conference on Software Engineering (ICSE'07).

Abstract
In this paper we argue that the modeling activity in the development of software-intensive systems should formalize as much as possible of the environment in which the application being developed operates. We also show that a rich formal model of the environment helps developers clearly state requirements that might typically be considered intrinsically informal (or non-formalizable in general). To illustrate this point, we show how a requirement for "orderly safe traffic" in a traffic system can be modeled, and we briefly discuss the benefits thereof.

• The paper in manuscript PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{FRM07-MISE07,
author = {Carlo A. Furia and Matteo Rossi and Dino Mandrioli},
title = {Modeling the Environment in Software-Intensive Systems},
booktitle = {Proceedings of the Workshop on Modeling in Software Engineering (MISE'07)},
year = {2007},
month = {May},
note = {A Workshop of the 29th International Conference on Software Engineering (ICSE'07)},
acceptancerate = {43\%}
}


Carlo A. Furia, Angelo Morzenti, Matteo Pradella, and Matteo Rossi.
Comments on "A Temporal Logic for Real-Time System Specification".
IEEE Transactions on Software Engineering, 32(6):424–427, June 2006. (Comments paper).

Abstract
The paper "An Interval Logic for Real-Time System Specification" presents the TILCO specification language and compares it to other existing similar languages. In this comment, we show that several of the logic formulas used for the comparison are flawed and/or overly complicated, and we explain why, in this respect, the comparison is moot.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
The paper comments on: R. Mattolini and P. Nesi, "A Temporal Logic for Real-Time System Specification". IEEE Transactions on Software Engineering, 27(3):208–227, March 2001.

@Article{FMPR06-TSE06comments,
author = {Carlo A. Furia and Angelo Morzenti and Matteo Pradella and Matteo G. Rossi},
title = {Comments on {A} Temporal Logic for Real-Time System Specification'},
journal = {IEEE Transactions on Software Engineering},
year = {2006},
volume = {32},
number = {6},
pages = {424--427},
month = {June},
}


Carlo A. Furia and Matteo Rossi.
Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling.
In Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06).
Lecture Notes in Computer Science, 4202:215–229, Springer-Verlag, September 2006.

Abstract
Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time.
In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions under which TRIO formulas have a consistent truth value when moving from continuous-time to discrete-time interpretations, or vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language and a requirement on the finite variability over time of the basic items in the specification formulas. We demonstrate the approach with an example of specification and verification.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report.

@InProceedings{FR06-FORMATS06,
author = {Carlo A. Furia and Matteo Rossi},
title = {Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling},
booktitle = {Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06)},
pages = {215--229},
year = {2006},
editor = {Eugene Asarin and Patricia Bouyer},
volume = {4202},
series = {Lecture Notes in Computer Science},
month = {September},
publisher = {Springer-Verlag},
acceptancerate = {44\%}
}


Carlo A. Furia, Matteo Rossi, Dino Mandrioli, and Angelo Morzenti.
Automated Compositional Proofs for Real-Time Systems.
In Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE'05).
Lecture Notes in Computer Science, 3442:326–340, Springer-Verlag, March 2005.

Abstract
We present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a small set of conditions concerning the integration of the different parts into a whole system. The reference specification language is the TRIO metric linear temporal logic.
The novelty of our approach with respect to existing compositional frameworks — most of which do not deal explicitly with real-time requirements — consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verification through theorem-proving of modular real-time axiom systems.
As an example of application, we show the verification of a real-time version of the old-fashioned but still relevant "benchmark" of the dining philosophers problem.

• An extended version containing appendices with proofs and details of the case study in PDF format (updated, improved, and extended text), and the DOI. of the published shorter version.

Notes
The paper published in the proceedings contains a minor error due to the variation of the time progression operator ->>, including the current instant and denoted as ->>_i, introduced and used to specify the case study. The inference rule of Proposition 1 no longer holds for this variation of the operator: Lemma 1 cannot be proved, since one can no longer rule out the accumulation of the future intervals of the NowOn operator (to see this, consider a right-open interval and what happens on its right boundary). Nonetheless, the case study can still be specified using the base ->> operator, with really minimal changes. Here, of course, you find the patched versions of the paper.

@InProceedings{FRMM05-FASE05,
author = {Carlo A. Furia and Matteo Rossi and Dino Mandrioli and Angelo Morzenti},
title = {Automated Compositional Proofs for Real-Time Systems},
booktitle = {Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE'05)},
pages = {326--340},
year = {2005},
editor = {Maura Cerioli},
volume = {3442},
series = {Lecture Notes in Computer Science},
month = {March},
publisher = {Springer-Verlag},
note = {Conference held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS'05)},
acceptancerate = {22\%}
}


Andrea Matta, Carlo A. Furia, and Matteo Rossi.
Semi-Formal and Formal Models Applied to Flexible Manufacturing Systems.
In Proceedings of the 19th International Symposium on Computer and Information Sciences (ISCIS'04).
Lecture Notes in Computer Science, 3280:718–728, Springer-Verlag, October 2004.

Abstract
Flexible Manufacturing Systems (FMSs) are adopted to process different goods in different mix ratios allowing firms to react quickly and efficiently to changes in products and production targets (e.g. volumes, etc.). Due to their high costs, FMSs require careful design, and their performance must be precisely evaluated before final deployment. To support and guide the design phase, this paper presents a UML semi-formal model for FMSs that captures the most prominent aspects of these systems. For a deeper analysis, two refinements could then be derived from the UML intermediate description: simulation components for "empirical" analysis, and an abstract formal model that is suitable for formal verification. In this paper we focus on the latter, based on the TRIO temporal logic. In particular, we hint at a methodology to derive TRIO representations from the corresponding UML descriptions, and apply it to the case of FMSs. A subset of the resulting formal model is then used to verify, through logic deduction, a simple property of the FMS.

• The paper in PDF format (updated, improved, and extended text) and its DOI.
@InProceedings{MFR04-ISCIS04,
author = {Andrea Matta and Carlo A. Furia and Matteo Rossi},
title = {Semi-Formal and Formal Models Applied to Flexible Manufacturing Systems},
booktitle = {Proceedings of the 19th International Symposium on Computer and Information Sciences (ISCIS'04)},
pages = {718--728},
year = {2004},
editor = {Cevdet Aykanat and Tugrul Dayar and Ibrahim Korpeoglu},
volume = {3280},
series = {Lecture Notes in Computer Science},
month = {October},
publisher = {Springer-Verlag},
acceptancerate = {29\%}
}


Carlo A. Furia, and Matteo Rossi.
A Compositional Framework for Formally Verifying Modular Systems.
In Proceedings of the International Workshop on Test and Analysis of Component Based Systems (TACoS'04).
Electronic Notes in Theoretical Computer Science, 116:185–198, Elsevier, March 2004.

Abstract
We present a tool-supported framework for proving that the composition of the behaviors of the separate parts of a complex system ensures a desired global property of the overall system. A compositional inference rule is formally introduced and encoded in the logic of the PVS theorem prover. Methodological considerations on the usage of the inference rule are presented, and the framework is then used to prove a meaningful property of a simple, but significant, control system.

• The paper in PDF format (updated, improved, and extended text) and its DOI.

Notes
This paper presents sketchily the inference rule also shown, more extensively and within a broader framework, in the FASE'05 paper, and then discusses some details of how it has been implemented in the PVS tools for TRIO.

@InProceedings{FR04-TACoS04,
author = {Carlo A. Furia and Matteo Rossi},
title = {A Compositional Framework for Formally Verifying Modular Systems},
booktitle = {Proceedings of the International Workshop on Test and Analysis of Component Based Systems (TACoS'04)},
pages = {185--198},
year = {2004},
volume = {116},
series = {Electronic Notes in Theoretical Computer Science},
month = {January},
publisher = {Elsevier}
}


Carlo A. Furia, Julian Tschannen, and Bertrand Meyer.
The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel.
In Proceedings of the 1st Workshop on Formal Integrated Development Environments (F-IDE) – An ETAPS event.
Electronic Proceedings in Theoretical Computer Science, 149:1–2, April 2014.

This is an invited talk I gave at the F-IDE workshop organized by Catherine Dubois, Dimitra Giannakopoulou, and Dominique Mery. Julian Tschannen contributed to the presentation with a live demo of EVE.

@InProceedings{FIDE14-gotthard,
author = {Carlo A. Furia and Julian Tschannen and Bertrand Meyer},
title = {The {G}otthard Approach: Designing an Integrated Verification Environment for {E}iffel},
booktitle = {Proceedings of the 1st Workshop on Formal Integrated Development Environments (F-IDE) -- An ETAPS event},
year = {2014},
editor = {Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'e}ry},
series = {Electronic Procedings in Theoretical Computer Science},
volume = {149},
pages = {1--2},
month = {April},
publisher = {EPTCS},
note = {Abstract of invited talk},
}


Steven Fraser, Luciano Baresi, Jane Cleland-Huang, Carlo A. Furia, Georges Gonthier, Paola Inverardi, and Moshe Y. Vardi.
A publication culture in software engineering (panel).
In Proceedings of the 9th Join Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE).
Pgg. 19–23, ACM, August 2013.

In this panel organized by Steven Fraser, we discussed "the publication process in the software engineering community" and "how it serves the needs of the community, [and] whether it is fair", concluding with "a discussion on suggested next steps".

@InProceedings{FSE13-PublicationPanel,
author = {Steven Fraser and Luciano Baresi and Jane Cleland-Huang and Carlo A. Furia and Georges Gonthier and Paola Inverardi and Moshe Y. Vardi},
title = {A publication culture in software engineering (panel)},
booktitle = {Proceedings of the 9th Join Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE)},
pages = {19--23},
year = {2013},
month = {August},
publisher = {ACM}
}


Carlo Alberto Furia.
Scaling Up the Formal Analysis of Real-Time Systems.
PhD Thesis.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2007.

Abstract
We develop techniques and methods to scale the application of formal methods up to large and heterogenous systems. Our solution focuses on real-time systems, and develops along the two aspects of compositionality and integration.
In the first part, we provide a compositional framework for specifying and verifying properties of modular systems, written using metric temporal logics with a descriptive approach. The framework consists in technical as well as methodological features. On the technical side, we provide an array of compositional inference rules to deduce facts about the composition of modules from facts about each component in isolation. Each rule has different features that make it more suitable for certain classes of systems. We also provide a general methodology to guide the formal specification of modular systems, and the application of the inference rules to verify them.
In the second part, we consider the problem of integration for systems with both discrete-time and continuous-time components. We provide suitable conditions under which metric temporal logic formulas have a consistent truth value whether they are interpreted in discrete or in continuous time, and we identify a language subset that meets these conditions. We also characterize the conditions and the language subset with detail. Our approach to integration permits the verification of global properties of heterogenous systems.

@PhdThesis{Fur07-PhD,
author = {Carlo Alberto Furia},
title = {Scaling Up the Formal Analysis of Real-Time Systems},
school = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2007},
month = {May}
}


Carlo Alberto Furia.
Compositional Proofs for Real-Time Modular Systems.
Master's Thesis (Tesi di Laurea).
Politecnico di Milano, December 2003.

Notes
The "Laurea degree thesis" is basically an extended version of the Master's thesis, and it's entirely written in English.

Folklore note
When I graduated, the degree I earned was simply called "Laurea", and concluded five years of university studies (thus basically corresponding to a Master's). After a reform of public Italian university, five-year-long degrees were split into a three-year-long one plus a two-year-long one, similarly to a Bachelor and Master's. However, the three-year-long degree was now called "Laurea", whereas the one obtained after two more years passed through the names "Laurea Specialistica" (specialized laurea) and the silly-sounding (at least to me) "Laurea Magistrale" (magisterial laurea). I don't know to what names it will be changed to in the future, but I just wanted to explain to which "Laurea" I'm referring to here.

@MastersThesis{Fur03-Laurea,
author = {Carlo Alberto Furia},
title = {Compositional Proofs for Real-Time Modular Systems},
school = {Politecnico di Milano},
year = {2003},
month = {December},
note = {(Tesi di Laurea)}
}


Carlo Alberto Furia.
Compositional Proofs for Real-Time Modular Systems.
Master's Thesis.
University of Illinois at Chicago, October 2003.

@MastersThesis{Fur03-MS,
author = {Carlo Alberto Furia},
title = {Compositional Proofs for Real-Time Modular Systems},
school = {University of Illinois at Chicago},
year = {2003},
month = {October}
}


Sebastian Nanz and Carlo A. Furia.
A Comparative Study of Programming Languages in Rosetta Code
arXiv.org > cs > 1409.0252, September 2014.

Abstract
Sometimes debates on programming languages are more religious than scientific. Questions about which language is more succinct or efficient, or makes developers more productive are discussed with fervor, and their answers are too often based on anecdotes and unsubstantiated beliefs. In this study, we use the largely untapped research potential of Rosetta Code, a code repository of solutions to common programming tasks in various languages, to draw a fair and well-founded comparison. Rosetta Code offers a large data set for analysis. Our study is based on 7087 solution programs corresponding to 745 tasks in 8 widely used languages representing the major programming paradigms (procedural: C and Go; object-oriented: C# and Java; functional: F# and Haskell; scripting: Python and Ruby). Our statistical analysis reveals, most notably, that: functional and scripting languages are more concise than procedural and object-oriented languages; C is hard to beat when it comes to raw speed on large inputs, but performance differences over inputs of moderate size are less pronounced and allow even interpreted languages to be competitive; compiled strongly-typed languages, where more defects can be caught at compile time, are less prone to runtime failures than interpreted or weakly-typed languages. We discuss implications of these results for developers, language designers, and educators, who can make better informed choices about programming languages.

@Misc{RosettaCode-TR-02092014,
author = {Sebastian Nanz and Carlo A. Furia},
title = {A Comparative Study of Programming Languages in {R}osetta {C}ode},
howpublished = {\url{http://arxiv.org/abs/1409.0252}},
month =         {September},
year =          {2014}
}


Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller.
Automating Full Functional Verification of Programs with Loops
arXiv.org > cs > 1407.5286, July 2014.

Abstract
Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants — properties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques to support a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various java.util classes, our DynaMate prototype automatically discharged 97% of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods — outperforming several state-of-the-art tools for fully automatic verification.

@Misc{DynaMate-TR-20072014,
author = {Juan P. Galeotti and Carlo A. Furia and Eva May and Gordon Fraser and Andreas Zeller},
title = {Automating Full Functional Verification of Programs with Loops},
howpublished = {\url{http://arxiv.org/abs/1407.5286}},
month =         {July},
year =          {2014}
}


Carlo A. Furia.
Rotation of Sequences: Algorithms and Proofs
arXiv.org > cs > 1406.5453, June 2014.

Abstract
Sequence rotation consists of a circular shift of the sequence's elements by a given number of positions. We present the four classic algorithms to rotate a sequence; the loop invariants underlying their correctness; detailed correctness proofs; and fully annotated versions for the Boogie verifier. The presentation illustrates in detail both how the algorithms work and what it takes to carry out mechanized proofs of their correctness.

@Misc{F14-TR-20062014,
author = {Carlo A. Furia},
title = {Rotation of Sequences: Algorithms and Proofs},
howpublished = {\url{http://arxiv.org/abs/1406.5453}},
month = {June},
year = {2014}
}


Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, and Andreas Zeller.
Automated Fixing of Programs with Contracts.
arXiv.org > 1403.1117, March 2014.

Abstract
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% 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.

@Misc{AutoFix-TR-05032014,
author = {Yu Pei and Carlo A. Furia and Martin Nordio and Yi Wei and Bertrand Meyer and Andreas Zeller},
title = {Automated Fixing of Programs with Contracts},
howpublished = {\url{http://arxiv.org/abs/1403.1117}},
month = {March},
year = {2014}
}


Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer.
Flexible Invariants Through Semantic Collaboration.
arXiv.org > 1311.6329, November 2013.

Abstract
Modular reasoning about class invariants is challenging in the presence of dependencies among collaborating objects that need to maintain global consistency. This paper presents semantic collaboration: a novel methodology to specify and reason about class invariants of sequential object-oriented programs, which models dependencies between collaborating objects by semantic means. Combined with a simple ownership mechanism and useful default schemes, semantic collaboration achieves the flexibility necessary to reason about complicated inter-object dependencies but requires limited annotation burden when applied to standard specification patterns. The methodology is implemented in AutoProof, our program verifier for the Eiffel programming language (but it is applicable to any language supporting some form of representation invariants). An evaluation on several challenge problems proposed in the literature demonstrates that it can handle a variety of idiomatic collaboration patterns, and is more widely applicable than the existing invariant methodologies.

@Misc{SemiCola-TR13-25112013,
author = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia and Bertrand Meyer},
title = {Flexible Invariants Through Semantic Collaboration},
howpublished = {\url{http://arxiv.org/abs/1311.6329}},
month = {November},
year = {2013}
}


Carlo A. Furia and Paola Spoletini.
Bounded Variability of Metric Temporal Logic.
arXiv.org > 1306.2141, June 2013, revised July 2014.

Abstract
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability—where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability?
In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.

@Misc{BoundedVarMTL-TR13-10062013,
author = {Carlo A. Furia and Paola Spoletini},
title = {Bounded Variability of Metric Temporal Logic},
howpublished = {\url{http://arxiv.org/abs/1306.2141}},
month = {June},
year = {2013},
note = {Last revised in July 2014}
}


Carlo A. Furia and Dino Mandrioli.
Turing: la vita, l'opera, l'impatto.
La Matematica nella Società e nella Cultura – Rivista dell'Unione Matematica Italiana.
Series I, V(2):105–148, August 2012 (in Italian).

Abstract
Written on the occasion of his birth's 100th anniversary, this article revisits the main steps of Alan Turing's life, and illustrates his fundamental contributions and his preeminent impact in the foundation of modern computer science. After an initial section that outlines Turing's biography and his most important results, we give a detailed presentation -- tailored to a general public with basic mathematical background but no expertise in theoretical computer science -- of what is possibly the most important and best known result of Turing's: his 1937 paper on the theory of computation, which introduces the class of automata known as "Turing machines". Finally, in the closing section we offer some historical/philosophical remarks about the notion of computation and its intrinsic limitations; this shows how Turing's contribution goes well beyond the limits of pure theoretical speculation as it carries practical and cultural implications that are general and still markedly relevant to the present time.

• The paper in PDF format.
@Article{FM12-TURING12,
author = 		  {Carlo A. Furia and Dino Mandrioli},
title = 		  {{T}uring: la vita, l'opera, l'impatto},
journal = 	  {La Matematica nella Societ{\a} e nella Cultura -- Rivista dellUnione Matematica Italiana},
year = 		  {2012},
volume = 	  {V},
number = 	  {2},
pages = 	  {105--148},
month = 	  {August},
note = 	  {Series I; in Italian}
}


H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, and Bertrand Meyer.
Contracts in Practice.
arXiv.org > 1211.4775, August 2012 (latest revision in February 2014).

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

@Misc{HowSpecChange-TR-17082012,
author = {H.-Christian Estler and Carlo A. Furia and Martin Nordio and Marco Piccioni and Bertrand Meyer},
title = {Contracts in Practice},
howpublished = {\url{http://arxiv.org/abs/1211.4775}},
month = {August},
year = {2012},
note = {Latest revision: February 2014}
}


Carlo A. Furia, Bertrand Meyer, and Sergey Velder.
Loop Invariants: Analysis, Classification, and Examples.
arXiv.org > 1211.4470, November 2012, revised June 2013, January 2014.

Abstract
A key step in the verification of imperative programs is to identify, for every loop, a loop invariant: a property ensured by the initialization and maintained by every iteration so that, when combined with the exit condition, it yields the loop's final effect. The invariant is a fundamental characteristic of any loop, useful not only to prove its correctness but also simply to understand why it works. Expanding on this observation, we analyze fundamental algorithms from a wide range of application areas of computer science and study their invariants, showing that they belong to a small number of general patterns identified in the article. The conclusions also include suggestions for automatic invariant inference, and general techniques for model-based specification.

• The report in PDF format.
• Implementations in Boogie of the algorithms discussed in the paper are available in this repository under branch inv_survey. You can get it with the command line hg clone -u inv_survey https://bitbucket.org/sechairethz/verified.
@Misc{LoopInvariantSurvey-TR-19112012,
author = {Carlo A. Furia and Bertrand Meyer and Sergey Velder},
title = {Loop Invariants: Analysis, Classification, and Examples},
howpublished = {\url{http://arxiv.org/abs/1211.4470}},
month = {November},
year = {2012},
note = {Revised in June 2013, January 2014}
}


Carlo A. Furia, Bertrand Meyer, Manuel Oriol, Andrey Tikhomirov, and Yi Wei.
The Search for the Laws of Automatic Random Testing.
arXiv.org > 1211.3257, November 2012.

Abstract
Can one estimate the number of remaining faults in a software system? A credible estimation technique would be immensely useful to project managers as well as customers. It would also be of theoretical interest, as a general law of software engineering. We investigate possible answers in the context of automated random testing, a method that is increasingly accepted as an effective way to discover faults. Our experimental results, derived from best-fit analysis of a variety of mathematical functions, based on a large number of automated tests of library code equipped with automated oracles in the form of contracts, suggest a poly-logarithmic law. Although further confirmation remains necessary on different code bases and testing techniques, we argue that understanding the laws of testing may bring significant benefits for estimating the number of detectable faults and comparing different projects and practices.

@Misc{LawsOfTesting-TR-14112012,
author = {Carlo A. Furia and Bertrand Meyer and Manuel Oriol and Andrey Tikhomirov and Yi Wei},
title = {The Search for the Laws of Automatic Random Testing},
howpublished = {\url{http://arxiv.org/abs/1211.3257}},
month = {November},
year = {2012}
}


Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, and Bertrand Meyer.
What Good Are Strong Specifications?
arXiv.org > 1208.3337, August 2012.

Abstract
Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and runtime performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a "sweet spot" with a favorable benefit to effort ratio.

@Misc{WhatGoodStrongSpec-TR-16082012,
author = {Nadia Polikarpova and Carlo A. Furia and Yu Pei and Yi Wei and Bertrand Meyer},
title = {What Good Are Strong Specifications?},
howpublished = {\url{http://arxiv.org/abs/1208.3337}},
month = {August},
year = {2012}
}


Marco Trudel, Carlo A. Furia, Martin Nordio, Bertrand Meyer, and Manuel Oriol.
C to O-O Translation: Beyond the Easy Stuff
arXiv.org > cs > 1206.5648, June 2012, revised April 2013.

Abstract
Can we reuse some of the huge code-base developed in C to take advantage of modern programming language features such as type safety, object-orientation, and contracts? This paper presents a source-to-source translation of C code into Eiffel, a modern object-oriented programming language, and the supporting tool C2Eif. The translation is completely automatic and supports the entire C language (ANSI, as well as many GNU C Compiler extensions, through CIL) as used in practice, including its usage of native system libraries and inlined assembly code. Our experiments show that C2Eif can handle C applications and libraries of significant size (such as vim and libgsl), as well as challenging benchmarks such as the GCC torture tests. The produced Eiffel code is functionally equivalent to the original C code, and takes advantage of some of Eiffel's object-oriented features to produce safe and easy-to-debug translations.

@Misc{C2Eif12-TR-26062012,
author = {Marco Trudel and Carlo A. Furia and Martin Nordio and Bertrand Meyer and Manuel Oriol},
title = {{C} to {O-O} Translation: Beyond the Easy Stuff},
howpublished = {\url{http://arxiv.org/abs/1206.5648}},
month = {June},
year = {2012},
note = {Latest revision: April 2013}
}


Carlo A. Furia.
Asynchronous Multi-Tape Automata Intersection: Undecidability and Approximation
arXiv.org > cs > 1206.4860, June 2012, latest revision February 2014.

Abstract
When their reading heads are allowed to move completely asynchronously, finite-state automata with multiple tapes achieve a significant expressive power, but also lose useful closure properties—closure under intersection, in particular. This paper investigates to what extent it is still feasible to use multi-tape automata as recognizer of polyadic predicates on words. On the negative side, determining whether the intersection of asynchronous multi-tape automata is expressible is not even semidecidable. On the positive side, we present an algorithm that computes under-approximations of the intersection; and discuss simple conditions under which it can construct complete intersections. A prototype implementation and a few non-trivial examples demonstrate the algorithm in practice.

@Misc{F12-TR-21062012,
author = {Carlo A. Furia},
title = {Asynchronous Multi-Tape Automata Intersection: Undecidability and Approximation},
howpublished = {\url{http://arxiv.org/abs/1206.4860}},
month = {June},
year = {2012},
note = {Latest revision: February 2014}
}


Carlo A. Furia.
A Survey of Multi-Tape Automata
arXiv.org > cs > 1205.0178, May 2012.

Abstract
This paper summarizes the fundamental expressiveness, closure, and decidability properties of various finite-state automata classes with multiple input tapes. It also includes an original algorithm for the intersection of one-way nondeterministic finite-state automata.

@Misc{F12-TR-01052012,
author = {Carlo A. Furia},
title = {A Survey of Multi-Tape Automata},
howpublished = {\url{http://arxiv.org/abs/1205.0178}},
month = {May},
year = {2012},
note = {Latest revision: November 2013}
}


Martin Nordio, H.-Christian Estler, Carlo A. Furia, and Bertrand Meyer
Collaborative Software Development on the Web.
arXiv.org > cs > 1105.0768, September 2011.

Abstract
Software development environments (IDEs) have not followed the IT industry's inexorable trend towards distribution. They do too little to address the problems raised by today's increasingly distributed projects; neither do they facilitate collaborative and interactive development practices. A consequence is the continued reliance of today's IDEs on paradigms such as traditional configuration management, which were developed for earlier modes of operation and hamper collaborative projects. This contribution describes a new paradigm: cloud-based development, which caters to the specific needs of distributed and collaborative projects. The CloudStudio IDE embodies this paradigm by enabling developers to work on a shared project repository. Configuration management becomes unobtrusive; it replaces the explicit update-modify-commit cycle by interactive editing and real-time conflict tracking and management. A case study involving three teams of pairs demonstrates the usability of CloudStudio and its advantages for collaborative software development over traditional configuration management practices.

@Misc{NEFM-TR-20110919,
author = {Martin Nordio and  H.-Christian Estler and Carlo A. Furia and Bertrand Meyer},
title = {Collaborative Software Development on the Web},
howpublished = {\url{http://arxiv.org/abs/1105.0768}},
month = {September},
year = {2011}
}


Yi Wei, Hannes Roth, Carlo A. Furia, Yu Pei, Alexander Horton, Michael Steindorfer, Martin Nordio, and Bertrand Meyer
Stateful Testing: Finding More Errors in Code and Contracts.
arXiv.org > cs > 1108.1068, August 2011.

Abstract
Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new errors, and also to improve the accuracy of the inferred contracts by discovering those that are unsound.
Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead.

@Misc{WRFPHSNM-TR-20110804,
author = {Yi Wei and Hannes Roth and Carlo A. Furia and Yu Pei and Alexander Horton and Michael Steindorfer and Martin Nordio and Bertrand Meyer},
title = {Stateful Testing: Finding More Errors in Code and Contracts},
howpublished = {\url{http://arxiv.org/abs/1108.1068}},
month = {August},
year = {2011}
}


Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Verifying Eiffel Programs with Boogie.
arXiv.org > cs > 1106.4700, June 2011.

Abstract
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper presents AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof's translation, including some whose implementation is underway, and demonstrates them with examples and a case study.

• The report in PDF format.
• This work has been presented at the First International Workshop on Intermediate Verification Languages (Boogie'11), held in Wroclaw, Poland, on 1 August 2011.
@Misc{TFNM11-TR-20110624,
author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Verifying {E}iffel Programs with {B}oogie},
howpublished = {\url{http://arxiv.org/abs/1106.4700}},
month = {June},
year = {2011}
}


Carlo A. Furia
QFIS – A verifier for the theory of quantifier-free integer sequences.
User manual, v. 1.1, 2011–2012.

• The manual in PDF format.
• The theory of quantifier-free integer sequences is described in this paper.
• Version 0.1 was released on 24 March 2011.
@Misc{QFIS-manual,
author = {Carlo A. Furia},
title = {{QFIS} -- A verifier for the theory of quantifier-free integer sequences},
howpublished = {User manual, v.~1.1},
year = {2011--2012}
}


Yu Pei, Yi Wei, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Code-Based Automated Program Fixing.
arXiv.org > cs > 1102.1059, February 2011, revised August 2011.

Abstract
Many programmers, when they encounter an error, would like to have the benefit of automatic fix suggestions—as long as they are, most of the time, adequate. Initial research in this direction has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches.
To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of dynamic analysis to gather evidence on the values taken by expressions derived from the program text.
The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches.

@Misc{PWFNM11-TR-20110205,
author = {Yu Pei and Yi Wei and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
title = {Code-Based Automated Program Fixing},
howpublished = {\url{http://arxiv.org/abs/1102.1059}},
month = {February},
year = {2011},
note = {Revised in August 2011}
}


Carlo A. Furia.
Review of The Calculus of Computation by A. R. Bradley and Z. Manna.
ACM SIGACT News, 42(1):32–35, March 2011.

@Article{Fur11-Review-BradleyManna,
author = {Carlo A. Furia},
title = {Review of \emph{The Calculus of Computation} by {A.\ R.\ Bradley} and {Z.\ Manna}},
journal = {ACM SIGACT News},
year = {2011},
volume = {42},
number = {1},
pages = {32--35},
month = {March}
}


Carlo A. Furia, Alberto Leva, Martina Maggio, and Paola Spoletini.
A control-theoretical methodology for the scheduling problem.
arXiv.org > cs > 1009.3455, September 2010.

Abstract
This paper presents a novel methodology to develop scheduling algorithms. The scheduling problem is phrased as a control problem, and control-theoretical techniques are used to design a scheduling algorithm that meets specific requirements. Unlike most approaches to feedback scheduling, where a controller integrates a "basic" scheduling algorithm and dynamically tunes its parameters and hence its performances, our methodology essentially reduces the design of a scheduling algorithm to the synthesis of a controller that closes the feedback loop. This approach allows the re-use of control-theoretical techniques to design efficient scheduling algorithms; it frames and solves the scheduling problem in a general setting; and it can naturally tackle certain peculiar requirements such as robustness and dynamic performance tuning. A few experiments demonstrate the feasibility of the approach on a real-time benchmark.

@Misc{FLMS10-TR-20092010,
author = {Carlo A. Furia and Alberto Leva and Martina Maggio and Paola Spoletini},
title = {A control-theoretical methodology for the scheduling problem},
howpublished = {\url{http://arxiv.org/abs/1009.3455}},
month = {September},
year = {2010}
}


Nadia Polikarpova, Carlo A. Furia, and Bertrand Meyer.
Specifying Reusable Components.
arXiv.org > cs > 1003.5777, March 2010.

Abstract
Reusable software components need well-defined interfaces, rigorously and completely documented features, and a design amenable both to reuse and to formal verification; all these requirements call for expressive specifications. This paper outlines a rigorous foundation to model-based contracts, a methodology to equip classes with expressive contracts supporting the accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract by means of expressive models based on mathematical notions, which underpin the precise definitions of notions such as abstract equivalence and specification completeness. Preliminary experiments applying model-based contracts to libraries of data structures demonstrate the versatility of the methodology and suggest that it can introduce rigorous notions, but still intuitive and natural to use in practice.

@Misc{PFM10-TR-30032010,
author = {Nadia Polikarpova and Carlo A. Furia and Bertrand Meyer},
title = {Specifying Reusable Components},
howpublished = {\url{http://arxiv.org/abs/1003.5777}},
month = {March},
year = {2010}
}


Paul Z. Kolano, Carlo A. Furia, Richard A. Kemmerer, and Dino Mandrioli.
Refinement and Verification of Real-Time Systems.
arXiv.org > cs > 1002.1796, February 2010.

Abstract
This paper discusses highly general mechanisms for specifying the refinement of a real-time system as a collection of lower level parallel components that preserve the timing and functional requirements of the upper level specification. These mechanisms are discussed in the context of ASTRAL, which is a formal specification language for real-time systems. Refinement is accomplished by mapping all of the elements of an upper level specification into lower level elements that may be split among several parallel components. In addition, actions that can occur in the upper level are mapped to actions of components operating at the lower level. This allows several types of implementation strategies to be specified in a natural way, while the price for generality (in terms of complexity) is paid only when necessary. The refinement mechanisms are first illustrated using a simple digital circuit; then, through a highly complex phone system; finally, design guidelines gleaned from these specifications are presented.

@Misc{KFKM10-TR-09022010,
author = {Paul Z. Kolano and Carlo A. Furia and Richard A. Kemmerer and Dino Mandrioli},
title = {Refinement and Verification of Real-Time Systems},
howpublished = {\url{http://arxiv.org/abs/1002.1796}},
month = {February},
year = {2010}
}


Carlo A. Furia.
arXiv.org > cs > 1001.2100, January 2010.

Abstract
We present a first-order theory of sequences with integer elements, Presburger arithmetic, and regular constraints, which can model significant properties of data structures such as arrays and lists. We give a decision procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., "for all even i's, the element at position i has value i+3 or 2i"). The resulting expressive power is orthogonal to that of the most expressive decidable logics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics.

@Misc{F10-TR-13012010,
author = {Carlo A. Furia},
title = {What's Decidable About Sequences?},
howpublished = {\url{http://arxiv.org/abs/1001.2100}},
month = {January},
year = {2010}
}


Carlo A. Furia and Matteo Rossi.
A Theory of Sampling for Continuous-time Metric Temporal Logic.
arXiv.org > cs > 0911.5642, November 2009.

Abstract
This paper revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied; more precisely, it is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. These results are applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique.

@Misc{FR09-TR-30112009,
author = {Carlo A. Furia and Matteo Rossi},
title = {A Theory of Sampling for Continuous-time {M}etric {T}emporal {L}ogic},
howpublished = {\url{http://arxiv.org/abs/0911.5642}},
month = {November},
year = {2009}
}


Carlo A. Furia and Bertrand Meyer.
Inferring Loop Invariants using Postconditions.
arXiv.org > cs > 0909.0884, September 2009.

Abstract
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained.

@Misc{FM09-TR-04092009,
author = {Carlo A. Furia and Bertrand Meyer},
title = {Inferring Loop Invariants using Postconditions},
howpublished = {\url{http://arxiv.org/abs/0909.0884}},
month = {September},
year = {2009}
}


Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms.
arXiv.org > cs > 0907.5074, July 2009.

Abstract
Complex systems typically have many different parts and facets, with different characteristics. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms can be better suited to describe different aspects of the system. While each paradigm provides a different view on the many facets of the system, it is of paramount importance that a coherent comprehensive model emerges from the combination of the various partial descriptions. In this paper we present a technique to model different aspects of the same system with different formalisms, while keeping the various models tightly integrated with one another. In addition, our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the propositional satisfiability (SAT) problem; this allows users to carry out formal verification activities both on the whole model and on parts thereof. The effectiveness of the approach is illustrated through the example of a monitoring system.

@Misc{BFPR09-TR-29072009,
author = {Marcello M. Bersani and Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms},
howpublished = {\url{http://arxiv.org/abs/0907.5074}},
month = {July},
year = {2009}
}


Carlo A. Furia and Paola Spoletini.
On Relaxing Metric Information in Linear Temporal Logic.
arXiv.org > cs > 0906.4711, June 2009, revised April 2010, April 2011, June 2011.

Abstract
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.

• The report in PDF format (June 2011 version).

Notes
The April 2010 version of the report is a major revision that eliminates the exponential blow-up in the transformation from M to Q (present in the June 2009 version of the report). The April 2011 version further refines the main result of the paper in considering the satisfiability of Q over unconstrained words. The June 2011 version is a minor revision which fixes some typos.

@Misc{FS09-TR-RelaxingMetricLTL,
author = {Carlo A. Furia and Paola Spoletini},
title = {On Relaxing Metric Information in Linear Temporal Logic},
howpublished = {\url{http://arxiv.org/abs/0906.4711}},
month = {June},
year = {2009},
note = {Last revised in June 2011}
}


Carlo A. Furia and Matteo Rossi.
MTL with Bounded Variability: Decidability and Complexity.
Technical Report 2008.10.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2008.

Abstract
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.

@TechReport{FR08-TR2008-10,
author = {Carlo A. Furia and Matteo Rossi},
title = {{MTL} with Bounded Variability: Decidability and Complexity},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2008},
number = {2008.10},
month = {May}
}


Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models.
arXiv.org > cs > 0804.4383, April 2008.

Abstract
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based) formalisms. The technique relies on the reduction, under reasonable assumptions, of the continuous-time verification problem to its discrete-time counterpart. This reconciles in a viable and effective way the dense/discrete and operational/descriptive dichotomies that are often encountered in practice when it comes to specifying and analyzing complex critical systems. The article investigates the applicability of the technique through a significant example centered on a communication protocol. More precisely, concurrent runs of the protocol are formalized by parallel instances of a Timed Automaton, while the synchronization rules between these instances are specified through Metric Temporal Logic formulas, thus creating a multi-paradigm model. Verification tests run on this model using a bounded validity checker implementing the technique show consistent results and interesting performances.

@Misc{FPR08-TR-28042008,
author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Practical Automated Partial Verification of Multi-Paradigm Real-Time Models},
howpublished = {\url{http://arxiv.org/abs/0804.4383}},
month = {April},
year = {2008}
}


Carlo A. Furia and Paola Spoletini.
MTL Satisfiability over the Integers.
Technical Report 2008.2.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, February 2008.

Abstract
We investigate the satisfiability problem for metric temporal logic (MTL) with both past and future operators over linear discrete bi-infinite time models — where time is unbounded both in the future and in the past — isomorphic to the integer numbers. We provide a technique to reduce satisfiability over the integers to satisfiability over the well-known mono-infinite time model of natural numbers, and we show how to implement the technique through an automata-theoretic approach. We also prove that MTL satisfiability over the integers is EXPSPACE-complete, hence the given algorithm is optimal in the worst case.

@TechReport{FS08-TR2008-2,
author = {Carlo A. Furia and Paola Spoletini},
title = {{MTL} Satisfiability over the Integers},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2008},
number = {2008.2},
month = {February}
}


Carlo A. Furia, Marco Mazzucchelli, Paola Spoletini, and Mara Tanelli.
Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation.
Technical Report 2008.1.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2008.

Abstract
In industrial applications, the number of final products endowed with real-time automatic control systems that manage critical situations as far as human safety is concerned has dramatically increased. Thus, it is of growing importance that the control system design flow encompasses also its translation into software code and its embedding into a hardware and software network. In this paper, a tool-supported approach to the formal analysis of real-time aspects in controller implementation is proposed. The analysis can ensure that some desired properties of the control loop are preserved in its implementation on a distributed architecture. Moreover, the information extracted automatically from the model can also be used to approach straightforwardly some design problems, such as the hardware sizing in the final implementation.

@TechReport{FMST08-TR2008-1,
author = {Carlo A. Furia and Marco Mazzucchelli and Paola Spoletini and Mara Tanelli},
title = {Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2008},
number = {2008.1},
month = {January}
}


Carlo A. Furia and Matteo Rossi.
On the Expressiveness of MTL Variants over Dense Time.
Technical Report 2007.41.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2007.

Abstract
The basic modal operator bounded until of Metric Temporal Logic (MTL) comes in several variants. In particular it can be strict (when it does not constraint the current instant) or not, and matching (when it requires its two arguments to eventually hold together) or not. This paper compares the relative expressiveness of the resulting MTL variants over dense time. We prove that the expressiveness is not affected by the variations when considering non-Zeno interpretations and arbitrary nesting of temporal operators. On the contrary, the expressiveness changes for flat (i.e., without nesting) formulas, or when Zeno interpretations are allowed.

@TechReport{FR07-TR2007-41,
author = {Carlo A. Furia and Matteo Rossi},
title = {On the Expressiveness of {MTL} Variants over Dense Time},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2007},
number = {2007.41},
month = {May}
}


Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Dense-Time MTL Verification Through Sampling.
Technical Report 2007.37.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, April 2007.

Abstract
This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [FR06]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers on some problem instances. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of a tool for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some promising results.

@TechReport{FPR07-TR2007-37,
author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
title = {Dense-Time {MTL} Verification Through Sampling},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2007},
number = {2007.37},
month = {April}
}


Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi.
Modeling Time in Computing: a taxonomy and a comparative survey.
arXiv.org > cs > 0807.4132, July 2008.
(A preliminary version appeared as Technical Report 2007.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2007).

Abstract
The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a growing attention to the temporal aspects of computing, not only in the computer science domain, but also in more traditional fields of engineering.
This article surveys various approaches to the formal modeling and analysis of the temporal features of computer-based systems, with a level of detail that is suitable also for non-specialists. In doing so, it provides a unifying framework, rather than just a comprehensive list of formalisms.
The paper first lays out some key dimensions along which the various formalisms can be evaluated and compared. Then, a significant sample of formalisms for time modeling in computing are presented and discussed according to these dimensions. The adopted perspective is, to some extent, historical, going from "traditional" models and formalisms to more modern ones.

• The report in PDF format (October 2010 version, with several typos fixed).
@Misc{FMMR08-TR-25072008,
author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi},
title = {Modeling Time in Computing: a taxonomy and a comparative survey},
howpublished = {\url{http://arxiv.org/abs/0807.4132}},
month = {July},
year = {2008},
note = {(A preliminary version appeared as Technical Report 2007.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2007)}
}


Carlo Alberto Furia.
Discrete Meets Continuous, Again.
Technical Report 2006.77.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, December 2006.

Abstract
This report collects some contributions about issues related to the notion of sampling invariance that has been introduced in [FR05,FR06], of which the present report can therefore be considered a follow-up and a complement.
In particular: we compare the expressiveness of the language R-Z-TRIO against that of MTL (and MITL), by also showing a result about the expressiveness of non-strict temporal operators; we characterize behaviors of bounded variability and formulas that preserve the bounded variability requirement; we compare the notion of sampling invariance with that of digitization [HMP92]; we discuss how to describe the runs of a timed automata with R-Z-TRIO formulas; we provide an example of application of the sampling invariance techniques to a simple verification problem; we summarize several related works on the expressiveness, decidability, and complexity of formalisms that are somewhat related to the R-Z-TRIO temporal logic.

@TechReport{Fur06-TR2006-77,
author = {Carlo Alberto Furia},
title = {Discrete Meets Continuous, Again},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2006},
number = {2006.77},
month = {December}
}


Carlo Alberto Furia.
Technical Report 2006.76.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, December 2006.

Abstract
This paper develops some methods and techniques for the practical use of compositionality to prove the correctness of modular systems, with reference to the metric temporal logic TRIO. It advocates a "lightweight" approach to compositionality, driven by the specifics of the system under development, where methodology is as important as technical solutions.

@TechReport{Fur06-TR2006-76,
author = {Carlo Alberto Furia},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2006},
number = {2006.76},
month = {December}
}


Carlo A. Furia, Matteo Rossi, Elisabeth A. Strunk, Dino Mandrioli, and John C. Knight.
Raising Formal Methods To The Requirements Level.
Technical Report 2006.64.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, November 2006.
Also: Technical Report CS-2006-24, Department of Computer Science, University of Virginia.

Abstract
In contrast with a formal notion of specification, requirements are often considered an informal entity. In a companion paper [SFRKM06], we have proposed a reference model that provides a clear distinction between requirements and specification, a distinction not based on the degree of formality. Using that notion of requirements, this paper shows how requirements as well as specifications can be formalized.
The formalization of requirements allows one to "lift" the well-known practices of formal analysis and verification from the specification/implementation level up to the highest level of abstraction in the development of a software product. In particular, we show how a formal validity argument can be constructed, proving that the formal specification satisfies its formal requirements. These ideas are demonstrated in an illustrative example based on a runway incursion prevention system, which was also partially presented in [SFRKM06]. Although our results and methods are of general applicability, we focus especially on the real-time aspects of the example; in order to support real-time formalization and reasoning, we exploit the ArchiTRIO formal language in a UML-like environment.

@TechReport{FRSMK06-TR2006-64,
author = {Carlo A. Furia and Matteo Rossi and Elisabeth A. Strunk and Dino Mandrioli and John C. Knight},
title = {Raising Formal Methods To The Requirements Level},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2006},
number = {2006.64},
month = {November},
note = {Also: Technical Report CS-2006-24, Department of Computer Science, University of Virginia}
}


Elisabeth A. Strunk, Carlo A. Furia, Matteo Rossi, John C. Knight, and Dino Mandrioli.
The Engineering Roles of Requirements and Specification.
Technical Report CS-2006-21.
Department of Computer Science, University of Virginia, October 2006.
Also: Technical Report 2006.61, Dipartimento di Elettronica e Informazione, Politecnico di Milano

Abstract
The distinction between requirements and specification is often confused in practice. This obstructs the system validation process, because it is unclear what exactly should be validated, and against what it should be validated. The reference model of Gunter et al. addresses this difficulty by providing a framework within which requirements can be distinguished from specification. It separates world phenomena from machine phenomena. However, it does not explain how the characterization can be used to help assure system validity.
In this paper, we enhance the reference model to account for certain key elements that are necessary to expose and clarify the distinction and the link between requirements and specification. We use the enhanced version to present a more refined picture of validity, where validation has two steps that can be undertaken separately. We use this picture to question whether the "what the system will do, not how it will do it" paradigm is useful in describing how to construct a specification, and propose an alternative. Finally, we present the requirements and specification for an illustrative example based on a runway incursion prevention system, with the ArchiTRIO formal language in a UML-like environment, to show how this might be done in practice.

@TechReport{SFRKM06-TR2006-61,
author = {Elisabeth A. Strunk and Carlo A. Furia and Matteo Rossi and John C. Knight and Dino Mandrioli},
title = {The Engineering Roles of Requirements and Specification},
institution = {Department of Computer Science, University of Virginia},
year = {2006},
number = {CS-2006-21},
month = {October},
note = {Also: Technical Report 2006.61, Dipartimento di Elettronica e Informazione, Politecnico di Milano}
}


Carlo Alberto Furia.
Quantum Informatics: A Survey.
Technical Report 2006.16.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2006.

Abstract
We survey the emerging field of quantum computing by showing its motivations and founding principles, and by presenting the most significant results in some selected areas. In particular, we outline the topics of quantum information, quantum algorithms, quantum cryptography, quantum finite automata, quantum error correction, and the physical realizations of quantum computing systems.

@TechReport{Fur06-TR2006-16,
author = {Carlo Alberto Furia},
title = {Quantum Informatics: A Survey},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2006},
number = {2006.16},
month = {January}
}


Carlo A. Furia, and Matteo Rossi.
When Discrete Met Continuous: on the integration of discrete- and continuous-time metric temporal logics.
Technical Report 2005.44.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, October 2005.

Abstract
Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time.
In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions for a TRIO specification to be invariant under change of time model from discrete to continuous and vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language (which we call TRIOsi) and a requirement on the finite variability over time of the values of the basic items that constitute the formulas of the specification. A specification which is invariant can then be verified entirely under the simpler discrete-time model, with the results of the verification holding for the continuous-time model as well.
We believe that this approach is general enough to be easily extendible to other temporal logics of comparable expressive power.

@TechReport{FR05-TR2005-44,
author = {Carlo A. Furia and Matteo Rossi},
title = {When Discrete Met Continuous: on the integration of discrete- and continuous-time metric temporal logics},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2005},
number = {2005.44},
month = {October}
}


Carlo Alberto Furia.
A Compositional World: a survey of recent works on compositionality in formal methods.
Technical Report 2005.22.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, March 2005.

Abstract
We survey the most significant literature about compositional techniques for concurrent and real-time system verification. We especially focus on abstract frameworks for rely/guarantee compositionality that handles circularity, but also consider different developments.

@TechReport{Fur05-TR2005-22,
author = {Carlo Alberto Furia},
title = {A Compositional World: a survey of recent works on compositionality in formal methods},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2005},
number = {2005.22},
month = {March}
}


Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Pradella, Matteo Rossi, and Pierluigi San Pietro.
Higher-Order TRIO.
Technical Report 2004.28.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, September 2004.

Notes
This paper introduces the basics about a higher-order extension of the first-order metric temporal logic TRIO.

@TechReport{FMMPRS04-TR2004-28,
author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Pradella and Matteo Rossi and Pierluigi {San Pietro}},
title = {Higher-Order {TRIO}},
institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
year = {2004},
number = {2004.28},
month = {September}
}