The thesis studies the formal verification of temporal properties of safety and liveness of parametrized concurrent systems, with a special focus on programs that manipulate complex concurrent data structures in the heap. This work presents a formal framework based on deductive methods which cleanly separates the analysis of the program control flow from the data manipulated by the program. The program control flow is analyzed using novel specialized deductive verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, the techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. Additionally, the thesis explores the construction of decidable theories equipped with decision procedures that can automatically check the generated verification conditions for some complex concurrent data structures. Finally, the whole framework is evaluated over some safety and liveness properties for a collection of mutual exclusion protocols and concurrent pointer-based data structures.
The European Researchers' Night in Madrid 2015, coordinated by the madrimasd Foundation for Knowledge, is an action framed under the Horizon 2020 European programme, celebrated in over 300 european cities at a time. Twenty scientific institutions in Madrid, including the IMDEA Institutes, collaborated this year.
More details can be found here.
It is our great pleasure to welcome Professor Somesh Jha of the University of Wisconsin, Madison as an IMDEA Software Institute visiting faculty member. Somesh is best known his visionary work in information security, formal methods, programming languages, software engineering, and computational finance. Somesh is the author of over 100 publications in international journals and conferences, a recipient of the 2015 CAV Award, and an NSF CAREER Award recipient.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 22nd ACM Conference on Computer and Communications Security, a top-ranked conference in this important area, held in Denver, CO.
IMDEA Software Institute faculty member Dario Fiore has a paper on homomorphic encryption together with D. Catalano (University of Catania, Italy). Their work proposes new techniques that enable third parties to compute over encrypted data, namely to evaluate a function without learning its inputs.
Faculty member Juan Caballero has two papers. One paper with visiting Ph.D. student Srdjan Matic from Università degli Studi di Milano and IMDEA Ph.D. student Platon Kotzias proposes an approach for deanonymizing hidden services in the TOR anonymity network. The other one with Ph.D. students Platon Kotzias and Richard Rivera, and visiting Ph.D. student Srdjan Matic analyzes digitally signed malware and potentially unwanted programs such as adware.
Faculty members Gilles Barthe and Benedikt Schmidt have a paper on formal proofs for pairing-based cryptography together with B. Grégoire (INRIA). Their work describes a new method and a new tool to perform such proofs automatically.
More information at CCS 2015.
The IMDEA Software Institute has been awarded the Syncrypt cybersecurity project. The project, featuring IMDEA Software Institute researchers Gilles Barthe and Benedikt Schmidt, is joint with Stanford University and The University of Pennsylvania, and has been awarded over one million dollars of funding from the US Office of Naval Research (ONR).
Read more from Madrid’s regional Ministry of Education and Research.
IMDEA Software Institute researcher Pavithra Prabhakar and her student Ratan Lal have published their work on analyzing parameterized linear systems in the International Conference on Embedded Software (EMSOFT). EMSOFT is a top-ranked conference in the field of embedded software and it will be held this year in Amsterdam, The Netherlands. The acceptance rate this year for the conference is 25%. The work focuses on the computation of bounded error approximations of the reachable set, and uses it for safety verification of an important class of dynamical systems, namely, parameterized linear systems. The authors have applied this techniques for analyzing aircraft collision avoidance protocols with several aircraft.
IMDEA Software Institute faculty member Pierre Yves Strub, and coauthors Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Jean Karim Zinzindohoue (INRIA), received the distinguished paper award at the 2015 IEEE Symposium on Security and Privacy (S&P ’15) for their research paper entitled “A Messy State of the Union: Taming the Composite State Machines of TLS”.
IMDEA Software Institute PhD student Antonio Nappa, along with researchers from the International Computer Science Institute in Berkeley CA and other researchers from Google Inc. received the distinguished practical paper award at the S&P ’15 for their practical contribution entitled “Ad Injection at Scale: Assessing Deceptive Advertisement Modifications”.
The official announcement is available here.
The first scientific meeting of the EU COST Action "Runtime Verification beyond Monitoring (ARVI)" has taken place in Valletta, Malta on April 9th and 10th. IMDEA Software Institute faculty member Cesar Sanchez is a member of the management committee and a workgroup leader, and a leader in the COST Action proposal’s elaboration.
Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications.
The main goals of the action are:
to create an infrastructure that supports comparing tools and reusing existing infrastructure in runtime verification,
to explore potential impactful applications of runtime verification to industrial settings like hardware, medical devices, cloud computing, and even human centric systems, and
to explore challenging application domains for monitoring and runtime verification, such as hybrid systems and distributed systems.
Given the importance of computer-based industries in Europe, novel applications of RV have a large impact in terms of the new class of designs enabled and their reliability and cost effectiveness.
This COST Action is funded for 4 years, until 2018.
The thesis presents a novel, tool-supported model-driven methodology for developing secure data-management applications. With the methodology defined, developers proceed by modeling three different views of the desired application: its data model, security model, and GUI model. These models formalize respectively the application's data domain, authorization policy, and its graphical interface together with its behavior. Afterwards a model-transformation function automatically lifts the policy specified by the security model to the GUI model. Finally, a code generator automatically generates a multi-tier application, along with all support for access control, from the security-aware GUI model. Miguel Ángel García de Dios was advised by IMDEA Software Institute faculty member Manuel Clavel and obtained his degree from Universidad Complutense de Madrid.
Four papers by IMDEA Software Institute researchers have been accepted for publication in the proceedings of the 27th International Conference on Computer Aided Verification, a top-ranked conference in this important field, held this year in San Francisco, CA. These four papers are among 68 selected for publication from over 250 submissions.
IMDEA Software Institute faculty member Cesar Sanchez has a paper on model checking “hyperproperties”, together with Bernd Finkbeiner and Markus Rabe from Saarland University, Germany. Their paper characterizes the precise complexity of the model checking problem for hyperproperties, and shows how to leverage existing state-of-the-art model checking tools to handle hyperproperty specifications, with applications to security, symmetry, and coding theory.
IMDEA Software Institute faculty member Boris Köpf has a paper together with Klaus von Gleissenthall ((TU Munich) and Andrey Rybalchenko (Microsoft Research) on verifying quantitative program properties, such as bounds on resource usage or information leaks. The core technical novelty is an SMT-based algorithm for synthesizing interpolants with cardinality constraints that relies on the theory of counting integer points in symbolic polytopes.
IMDEA Software Institute faculty member Michael Emmi’s contribution reports on the development of a tool for uncovering concurrency bugs in Android apps, a joint work with Burcu Kulahcioglu Ozkan and Serdar Tasiran of Koç University in Turkey.
IMDEA Software Institute faculty member Pierre Ganty has a paper on the automated verification of shared-memory asynchronous systems together with A. Durand-Gasselin, J. Esparza from TU Munich and R. Majumdar from Max Planck Institute for Software Systems, Germany. Their work classifies verification problems for liveness properties in shared-memory asynchronous systems from a computational point of view. These systems are characterized by a leader process and arbitrarily-many anonymous and identical contributors. Processes communicate through a shared, bounded-value register.
Find more information on the conference website.
IMDEA Software Institute faculty member John Gallagher and coauthor Bishoksan Kafle received the best paper award at the 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM ’15) for their paper entitled “Constraint Specialisation in Horn Clause Verification”.
The article appears in the ACM Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM ’15), edited by Kenichi Asai and Kostis Sagonas: DOI.
The second Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute took place April 9-10, 2015, at the IMDEA Software building in Madrid. The workshop was aimed at discussing collaborative work on chosen software projects and, where possible, to bring those advances to Microsoft's businesses.
The workshop focused on the following three projects:
It was organized by Judith Bishop and Cedric Fournet from Microsoft Research and by Manuel Hermenegildo and Alexey Gotsman from the IMDEA Software Institute.
These workshops bring together researchers and students to discuss their collaborative work on hot topics in software in order to advance the state of the art and, where possible, to bring those advances to market.
The 2-day workshop included the following keynote speakers:
Phil Bernstein is a distinguished scientist in the Database Group of Microsoft Research Redmond. Bernstein is also an affiliate professor at the University of Washington and frequent committee member or chair of conferences such as VLDB and SIGMOD. He won the SIGMOD Edgar F. Codd Innovations Award in 1994. Bernstein is a member of the National Academy of Engineering and an elected Fellow of the Association for Computing Machinery. Currently, he is working on a distributed systems programming framework, called Project Orleans: Distributed Virtual Actors for Programmability and Scalability.
Aleks Nanevski is an Assistant Research Professor at the IMDEA Software Institute which he joined in the Fall 2009. Prior to that, Nanevski was a postdoctoral researcher at Carnegie Mellon University under the supervision of Prof. Edmund Clarke, at Harvard University under the supervision of Prof. Greg Morrisett, and at Microsoft Research, Cambridge. Aleksandar holds a PhD degree in Computer Science from Carnegie Mellon University, which he obtained in August 2004. He is working on type systems and structured proofs for concurrent software verification.
The IMDEA Software Institute has published its 2014 Annual Report.
The IMDEA Software Institute has been awarded an Honorable Mention in the area of Public-Private Cooperation by the madri+d Foundation, for its cooperation with the Italian industrial group Reply and Dutch TNO on cyber attack detector engineering and its commercial exploitation.
This collaboration was supported in part by Cadence, an EIT ICT Labs innovation activity in the area of privacy, security, and trust, started in 2014, in which the IMDEA Software Institute, TNO, and Reply are applying novel anomaly detection technologies to the creation of specific innovative products and services for providing more secure ICT environments for both governments and businesses.
This Honorable Mention was awarded by the madri+d Prizes jury in the tenth annual edition of these awards, which recognize significant scientific and technological advances in solving industrial and societal challenges, the capacity for converting research projects and results into wealth and welfare in the Madrid Region, excellence in implementing collaborative research and development activities on the European level, and the generation and dissemination of knowledge.
IMDEA Software Institute faculty researcher Pierre Yves Strub, together with his colleagues at INRIA Rocquencourt, France and Microsoft Research have uncovered a vulnerability in the popular SSL encryption mechanism used widely on the Internet to access web pages securely. The flaw, dubbed “FREAK: Factoring RSA Export Keys” can be exploited to trick web browsers into interacting with malicious websites. The problem affects a large number of web servers and clients and has thus received major media impact.
This discovery was made within the ongoing SMACK TLS project, which is aimed at developing increasingly-secure Internet authentication software. Pierre Yves Strub and his colleagues have developed an automated technique to discover vulnerabilities in implementations of authentication protocols, and uncovered several vulnerabilities which, gone unnoticed, could be exploited by hackers to compromise Internet security.
The researchers focused on the family of authentication protocols know as “Transport Layer Security” (TLS), which is the increasingly-popular successor to the ubiquitous “Secure Sockets Layer” (SSL) protocol family. By building formally-verified reference implementations of TLS protocols, they were able to systematically generate inadmissible protocol responses, which should be disallowed by the protocol, and test whether any of those responses were in fact admitted by existing implementations. Inadmissible responses suggest potential vulnerabilities, and were to converted into exploits in actual TLS implementations. “FREAK” is one of the vulnerabilities discovered.
More details can be found here.
This work was performed in collaboration with Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, and Jean Karim Zinzindohoue of INRIA Rocquencourt, France, and Cedric Fournet and Markulf Kohleiss of Microsoft Research.
Last Wednesday, February 18th, Lorena Heras Sedano, responsible for the General Directorate for Universities and Research of the Madrid Regional Government visited the premises of the IMDEA Software Institute with Juan Ángel Botas Echevarría, Deputy Director for Research.
The visitors were given a guided tour of the premises and they met personally the Institute's research team. Several researchers presented the goals and some of the advances attained in the different research lines of the Institute and the ongoing research projects, as well as their practical applications and other industrial collaboration and technology transfer activities.
They also visited the Microsoft - IMDEA Software Joint Research Center and the Madrid Co-location Center of the ICT Labs KIC of the European Institute of Innovation and Technology. This co-location center is also the headquarters of this KIC in Spain, and it is coordinated by the IMDEA Software Institute and located in its premises.
More info can be found here.
It is our great pleasure to welcome Professor Ben Livshits as an IMDEA Software Institute visiting faculty member. Ben is a research scientist at Microsoft Research and an affiliate professor at the University of Washington, USA, and is known for his work in software reliability, especially tools to improve software security, with a primary focus on approaches to finding buffer overruns in C programs and a variety of security vulnerabilities (cross-site scripting, SQL injections, etc.) in Web-based applications. He is the author of several dozen academic papers and patents. Lately, he has been focusing on topics ranging from security and privacy to crowdsourcing an augmented reality.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 36th IEEE Symposium on Security and Privacy, a top-ranked conference in this important area, held in San Jose, CA. These four papers are among 55 papers selected for publication out of over 400 submissions to the conference.
IMDEA Software Institute faculty member Dario Fiore has a paper on privacy-preserving proofs, together with M. Backes (CISPA, Saarland University), M. Barbosa (HASLab – INESC TEC and Universidade do Minho), and R. M. Reischuk (ETH Zurich). Their work (whose title is "ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data") proposes a new system, called ADSNARK, that allows users to prove the correctness of computations while maintaining the privacy of the input data. The main novelty of ADSNARK is to work efficiently with authenticated inputs, a useful feature for applications such as smart metering and the emerging wearable computing paradigm.
Faculty member Juan Caballero and Ph.D. student Antonio Nappa have a paper on analyzing the lifecycle of software vulnerabilities in client applications (e.g., browsers, document editors). This work identifies several new threats presented by multiple installations of the same program and shared libraries. This work is collaboration with researchers at Symantec Research Labs and University of Maryland at College Park.
IMDEA Software Institute Ph.D student Antonio Nappa along with researchers from the International Computer Science Institute in Berkeley CA and other researchers from Google Inc. have a paper that presents a study on advertisement injection in browser session. They have developed a multi-staged pipeline that identifies ad injection in the wild and captures its distribution and revenue chains.
Faculty member Pierre Yves Strub has a paper on designing a generic, robust and verified state machine for the TLS protocol with Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Jean Karim Zinzindohoue (INRIA). Their work addresses the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes of TLS. They present the first verified implementation of a composite TLS state machine in C that can be embedded into OpenSSL and accounts for all its supported ciphersuites. They also discovered several critical security vulnerabilities that have lain hidden, for years, in popular open-source SSL libraries.
More information at SP 2015.
The first edition of the Itinerant Cryptography Seminars, a multi-institutional series aimed at promoting cryptography research, was hosted by IMDEA Software Institute on January 22, and organized by Dario Fiore.
More details can be found here.
The International Competition on Software Verification (SV-COMP) is a driving force for the invention of new methods, technologies, and tools for the automated verification of computer software. Software verification is an unarguably-important research area as society becomes more and more dependent on its correct functionality: software bugs can cost lives and great monetary loss. Though the goal of verified software has existed since the dawn of computer science, the technology enabling widespread use of software verifiers has been extremely challenging to develop, due to fundamental philosophical limitations, practical engineering obstacles, and the challenge in surmounting both simultaneously. SV-COMP aims to advance software verification technology by bringing together the top international minds.
This year marks the 4th annual installment of an increasingly-competitive event, in which 22 entries from top research institutions including New York University, Ecole Normale Supérieure (ENS) of Paris, University of Freiburg, Tsinghua University, Microsoft Research, and IMDEA Software Institute compete across 13 categories of software verification problems.
Each competition entry is a computer program called a “verifier”, and each “problem” is a computer program whose correctness must be verified by the verifier. The verifiers are submitted as executable code, and the problems are provided as source code written in the C programming language. The verifiers classify problems either as “correct”, “incorrect”, or “unknown”, within a time limit of 900 seconds per problem. Points are awarded according to the accuracy of classification. In each problem category, the three highest-scoring verifiers are awarded medals: gold, silver, and bronze.
In collaboration with the University of Utah and Microsoft Research, the IMDEA Software Institute’s competition entry, named SMACK+Corral, was awarded medals in four categories — two gold, one silver, and one bronze — placing it among the top-performing verifiers. Only one entry earned more gold medals, and only three entries earned more medals total.
Technically, SMACK+Corral is the fusion of two programs. SMACK is an open-source project led by Zvonimir Rakamaric of the University of Utah, and Michael Emmi of the IMDEA Software Institute. The role of SMACK is to translate the C-language verification problems into mathematical representations which can be more-easily processed by automated logical-reasoning engines known as “theorem provers”. Corral, developed by Microsoft Research, applies novel reasoning algorithms to decide whether the given mathematical representation should be classified as “correct”. Combined, the two function as a powerful verifier of C-language programs.
The SV-COMP 2015 post-competition event is being held on the week of April 13th, 2015, as part of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), in London, UK. The event includes a short presentation by the authors of each entry, and an official announcement of the competition results.
More information at SV-COMP 2015.
On December 18, 2014, five students who won the contest at the EIT ICT Labs Summer School in the field of Privacy, Security and Trust (PST) were invited to IMDEA Software Institute to present technological challenges and discuss their business ideas with the Institute's leading scientists. The students were:
The visit was organized and moderated by Jesús Contreras, EIT ICT Labs Business Developer at the Madrid CLC.
On 18 December 2014, the Madrid CLC of EIT ICT Labs at IMDEA Software Institute hosted the FI-PPP-Liaison Demo Day, with presentations from the three SMEs that have won prizes from the FI-PPP Liaison project for using FI-WARE technologies to bring innovative products and services to the market:
SmartTaxi, with a smart app that helps taxi drivers reduce waiting time and to increase their customer pick up rate.
WeCollect (Wellness Telecom), who developed the eGarbage system to improve waste collection management.
B-SEED (Pyro Fire Extinction), with a platform to incorporate smart cities technologies into the natural environment, in order to improve prevention and management of forest fires.
The FI-PPP Liaison project connects EIT ICT Labs activities in the field of future networking solutions with FI-WARE as a major European initiative in developing and promoting new generation cutting-edge Future Internet (FI) technologies and solutions based on Public-Private Partnership (PPP).
The three companies have been awarded EUR 25,000 each to develop pilot projects based on Internet-of-Things (IoT) FI-WARE technologies, from pool of 40 applicants and 10 short-listed contenders which were provided with training and coaching within the FI-PPP Liaison project.
The demo day was organized by IMDEA Software Institute in cooperation with partners from Technical University of Madrid (UPM), Spain and Telefonica I+D, and was attended by other major actors in the IoT arena, such as Ferrovial.
On December 17, 2014, the IMDEA Software Institute organized an outreach event at the EIT ICT Labs Madrid CLC to present the EIT ICT Labs Master School in ICT Innovation and its offer of post-graduate programs.
The Master School provides the highest level of international academic education in ICT with additional Innovation and Entrepreneurship (I&E) modules that enable the students to develop their own innovative ideas into new, marketable products and services. The overall goal is to boost EU entrepreneurship, and thus strengthen the basis of the innovation and technology-based economy.
Manuel Hermenegildo (Director of the IMDEA Software Institute and of the EIT ICT Labs Madrid Associate Node), and Juan José Moreno Navarro (UPM Vice-Rector for Graduate Studies and Deputy Director of the EIT ICT Labs Madrid Associate Node), hosted the event and explained the general guidelines of the Master programmes. UPM participates in the program as an affiliate university in Spain, together with another 19 top-level European technical universities.
The two-year Master programme is organized in eight technical majors, each executed by two distinct European universities. The programs are:
In addition to a full scholarship, summer school attendance, real professional experience in top IT companies, and mentoring for development of personal and team business projects and start-up creation, the graduates will receive a double degree from the implementing universities, and an official certificate in innovation and entrepreneurship from ICT Labs.
It is our great pleasure to welcome Alessandra Gorla as IMDEA Software Institute's newest Assistant Research Professor. Alessandra's doctoral dissertation from the Università della Svizzera Italiana, Lugano, Switzerland was awarded the Fritz Kutter Award for Best Industry-Related Thesis in Computer Science from a Swiss University in 2011. Her principal research interests are in malware detection for mobile applications, automatic software repair, and software testing and analysis.
The Joint EasyCrypt-F*-CryptoVerif School, which took place in Paris between 24 and 28 November 2014, attracted over 80 participants from Europe, North America and Japan. Easycrypt is the tool developed by researchers at IMDEA Software Institute led by faculty Gilles Barthe. The school was split between lectures, which introduced the formal foundations behind these tools, and exercises, where the participants used the tools to verify the security of representative cryptographic constructions.
See the full press release here.
It is our great pleasure to welcome Professor Roberto Giacobazzi of the University of Verona, Italy as an IMDEA Software Institute visiting faculty member. Roberto is best known for his extensive and foundational work on abstract interpretation: both in the general theory, and in its applications to program semantics, static program analysis, language-based security, digital asset protection, and malware analysis, among other things. Roberto is the author of over 100 publications in international journals and conferences, and serves on the steering committees of the ACM Symposium on Principles of Programming Languages (POPL) and the Static Analysis Symposium (SAS).
It is our great pleasure to welcome Professor Michael Ernst of the University of Washington, USA as an IMDEA Software Institute visiting faculty member. Michael is an ACM Fellow and author of over 100 publications spanning the spectrum from software engineering, to program analysis (both static and dynamic), to programming language design. His research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work.
Deadline: The deadline to submit proposals is July 31st, 2014.
In the last years the need for a more powerful, flexible, and resilient Internet has arisen, not only in the scientific community, but also within its users. The EC has initiated an RTD initiative, the FI-PPP (www.fi-ware.org), which aims at generating new Internet-related technologies and solutions to boost occupation and economy in Europe. This activity intends to establish mutually beneficial links between the FI-PPP and the EIT ICT Labs initiatives.
We expect to select, train, and support up to three start-ups or SMEs dealing with Future Internet and Internet-of-Things technologies. The selection process will be divided into two phases:
The following competences and experience are required:
The SME will take part in the FI-PPP Liaison activity from October 1st to December 31st, 2014. The allocated maximum budget amounts to EUR 25,000.00 per company with room for up to three companies. This shall cover all costs related to the project, including travel costs.
Responses shall include the following information in a maximum of 3 pages:
Please, for more information, contact
The IMDEA Software Institute has been awarded a Marie Curie Career Integraion Grant by the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme.
The project VeriStab lead by Pavithra Prabhakar will investigate formal verification of stability of embedded control systems. It addresses a very important property in control system design, namely, stability, and proposes novel algorithmic methods to verify stability of large scale embedded control systems. The project will run for a duration of 4 years and will promote the integration of the researcher with the host institute.
The IMDEA Software Institute has published its 2013 Annual Report.
Microsoft Research and the IMDEA Software Institute officially presented their new Joint Research Center.
The collaboration was formalized in late 2013 with the objective of framing and boosting the significant research collaborations between Microsoft Research and the IMDEA Software Institute in software science and technology. The new Joint Research Center sets the ground for a long-term collaboration aiming to advance the science and technology which will allow the cost-effective development of high-quality software products.
Among other relevant members of the public administration, industry, and the software research community, the presentation was chaired by Carles Grau, Public Sector Director at Microsoft Spain; Rocio Albert López-Ibor, General Director for Universities and Research, Regional Ministry for Education; Manuel Hermenegildo, Director of the IMDEA Software Institute; Judith Bishop, Director of Computer Science at Microsoft Research, and Jaime Puente, Director for Latin America at Microsoft Research.
More information at:
The first Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute took place April 2-4, 2014, at the IMDEA Software building in Madrid. The workshop was aimed at reinforcing the collaboration between these two institutions on the following topics:
The Workshop was the launch activity of the Center, at which researchers from both sides worked on topics of joint interest. It was organized by Judith Bishop and Georges Gonthier from Microsoft Research and by Gilles Barthe and Manuel Hermenegildo from the IMDEA Software Institute.
These workshops bring together researchers and students to discuss their collaborative work on hot topics in software in order to advance the state of the art and, where possible, to bring those advances to market. The focus of the first workshop is on verification (coordinated by Alexey Gotsman and Francesco Logozzo), programming languages (coordinated by Pierre Yves Strub and Georges Gonthier), and security (coordinated by Juan Caballero and Ben Livshits).
The 3-day workshop included the following keynote speakers:
Five papers by IMDEA Software Institute researchers have been accepted for publication at the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), a top-ranked conference in the area of programming languages and systems.
These five papers are among 51 papers selected for publication out of 220 submissions to the conference.
The president of the Autonomous Region of Madrid, Ignacio González González, presided over the official opening of the building of the Madrid Institute for Advanced Studies in Software Development Technologies (the IMDEA Software Institute), which took place on Monday July 8, 2013, at noon.
The president was accompanied by the Secretary of State for Research, Development, and Innovation of the Ministry for Economy and Competitiveness, Carmen Vela, the Rector of the Technical University of Madrid, Carlos Conde, and the Counselor for Education, Youth, and Sports, Lucía Figar, among other personalities form industry and science and research policy.
With more than 8000 m2, the Institute's new building includes offices, numerous spaces for interaction and collaboration, areas for project meetings and for scientific and industrial conferences and workshops, and powerful communications and computing infrastructures. The layout facilitates the setup of joint research labs with industry and academia. It is highly energy-efficient, through energy-conscious design, co-generation, and full automation.
The Institute is located within the Montegancedo International Campus of Excellence of the Technical University of Madrid, next to the UPM Computer Science department, research centers, and technology transfer facilities, including a company incubator.
The president presented the Institute as one of the instruments that the Madrid Region uses to create an environment that is favorable and confidence-inspiring for companies, that is attractive for innovators, and that helps Madrid boost two of its well-known advantages: its competitiveness and its modernity. Ignacio González concluded thanking everyone for their collaboration in a common project whose goal is to make Spain a country at the forefront, with a sustainable and competitive economy and, especially, to the researchers of the Institute for having selected Spain to develop their talent.European Institute of Innovation and Technology (EIT) ICT Labs (Information and Communication Technologies Labs), the EIT Knowledge and Innovation Community (KIC) in ICT. The goal of EIT ICT Labs is to drive European leadership in ICT innovation for economic growth and quality of life. The decision to admit the IMDEA Software Institute as an associate partner was made by the EIT ICT Labs Steering Committee on March 26, 2013. As the first Spanish EIT ICT Labs member, the IMDEA Software Institute is in charge of coordinating the new associate node (Associate Partner Group) in Spain, which includes as partners the following leading research, development, innovation and business development organizations in Spain: Telefónica, INDRA, Atos, Technical University of Madrid, and the Barcelona Supercomputing Center. The headquarters (Associate Partner Group Co-Location Center) are located in the new IMDEA Software Institute building. EIT ICT Labs currently has five nodes located in Berlin, Eindhoven, Helsinki, Paris, Stockholm, and Trento, and three associate nodes located in London, Budapest, and now Madrid. The purpose of each node is to catalyze knowledge and innovation development by involving outstanding research institutes, universities, and enterprises from the respective country, following an integrated approach based on a synergy between education, research, and business. Besides ICT Labs, other KICs operating within the EIT framework are concerned with climate and innovative energy solutions.
As part of the activities of the NESSoS Project, the IMDEA Software Institute has organized a one-day training course on the ActionGUI technology, with participation of representatives of ATOS Research & Innovation. IMDEA researchers and ATOS representatives also discussed in depth future extensions of the ActionGUI technology as well as the potential commercial impact of this technology.
Andrea Cerone (postdoctoral researcher at the IMDEA Software Institute) wins the best paper award at the 8th International Federated Conference on Distributed Computing Techniques, for the article Modeling Mac-layer Communications in Wireless Systems. The paper is co-authored by Matthew Hennessy (Trinity College Dublin) and Massimo Merro (Università degli Studi di Verona).
Juan Caballero gives an invited talk at the 38th annual meeting of the Messaging, Malware and Mobile Anti-Abuse Working Group (M3AAWG) in Vienna, Austria. M3AAWG is arguably the most important industry forum dealing with Internet security issues such as bot mitigation, spam, Web messaging abuse, and DNS abuse. The member roster of M3AAWG includes Apple, Google, AT&T, PayPal, Symantec, Time Warner, Facebook, Yahoo, France Telecom, and many other companies. Juan's talk happens on June 6th, and is one of two invited talks from academics in the three day event. His talk deals with the emergence of specialized services in the Malware ecosystem that help attackers monetize Internet-connected computers.
The IMDEA Software Institute has published its 2012 Annual Report.
Within its strategic framework for cooperation with industry, the IMDEA Software Institute has established together with Telefónica Digital, a special Joint Research Unit (JRU) in the area of cloud computing and its supporting infrastructures.
The creation of the JRU kernel started already in December 2012, and it presently includes specialists in the Java and OpenStack platforms, as well as specialists in the administration of virtual cloud resources. The focus of the JRU is on automated definition, deployment, and management of virtual machines, storage, and networks, all of which are the key components for executing cloud applications.
Gilles Barthe has given one of the two plenary Keynote addresses at ETAPS 2013, presenting his work on Computer-aided Cryptographic Proofs, developed at the IMDEA Software Institute. The EasyCrypt tool site provides additional information and references.
The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science. Established in 1998, it is a confederation of six main annual conferences (CC, ESOP, FASE, FOSSACS, TACAS and POST) accompanied by satellite workshops and other events.
Gilles Barthe , Juan Manuel Crespo , César Kunz , and Mark Marron , IMDEA Software researchers, win the best paper award at The 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'2013), for their article From Relational Verification to SIMD Loop Synthesis.
The paper is co-authored by Sumit Gulwani (Microsoft Research).
The IMDEA Software Institute has been awarded the AutoCrypt project, a joint project with Stanford University, University of Pennsylvania, and SRI. The project is funded by ONR and will run from July 2012 until July 2015.
AutoCrypt aims to use computer technology to provide mathematical guarantees that a cryptographic algorithm is secure, and that it is adequate for a given product, process, or service.
The IMDEA Software team will use EasyCrypt to develop a systematic classification of cryptographic algorithms and to create a cryptographic atlas that will be used by researchers and companies to choose the most suitable algorithm for their needs.
The AMAROUT-II program is now open for
new applications for fellowships. This EU Marie Curie (PEOPLE-COFUND)
program, coordinated by the IMDEA Software Institute, offers 152
fellowships during the next 4 years to experienced researchers to help
develop their individual research projects within any one of the
research institutes comprising the IMDEA network. Each fellowship
funds a researcher for up to three years. The call for applications
will remain open until September, 30 2015, with periodic closing
dates. For more information see AMAROUT-II. Contact:
Alexey Gotsman received the best paper award at The 23rd International Conference on Concurrency Theory (CONCUR 2012). The paper, "Linearizability with Ownership Transfer", was co-authored by Hongseok Yang (Oxford University).
Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. The paper generalizes this notion to the setting of common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection.
The IMDEA Software Institute has been granted the ``ENTRA (Whole-Systems Energy Transparency)'' EU project, which aims to promote the development of greener IT products by enabling "energy-aware" software development. Within the project, starting on October 1, 2012, researchers from the IMDEA Software Institute will create tools for advanced program analysis and modeling of energy consumption in computer systems which will facilitate predictions of energy consumption early in the software design phase. ENTRA is funded by the EU 7th Framework Programme, through the Future and Emerging Technologies (FET) scheme, and has an overall budget of 2.1 million Euro. Apart from the IMDEA Software Institute and Roskilde University, which coordinates the project, the consortium also includes XMOS Ltd. and the University of Bristol.
Local project contact: Pedro López-García
The IMDEA network of institutes has been granted AMAROUT-II, an EU Marie Curie (PEOPLE-COFUND) program that will offer 152 fellowships during the next 4 years to experienced researchers to help develop their individual research projects within any one of the research institutes comprising the IMDEA network. Each fellowship funds a researcher for up to three years. A permanent call for applications will be opened on October, 1 2012 and will run until September, 30 2015, with periodic closing dates. The program, prepared and coordinated by the IMDEA Software Institute, is designed to support transnational mobility of experienced researchers offering attractive working conditions and providing opportunities to deepen and widen their skills. AMAROUT-II is a continuation of AMAROUT, a highly successful COFUND program which is now closed for applications.
For more information see AMAROUT-II. Contact:
The IMDEA Software Institute has published its 2011 Annual Report.
Santiago Zanella, who completed his PhD at the IMDEA Software Institute under the supervision of Prof. Gilles Barthe, is the winner of the 2011 EAPLS Best Dissertation Award for his dissertation "Formal Certification of Game-Based Cryptographic Proofs" defended at the École Nationale Supérieure des Mines de Paris in 2010.
This award is given by the European Association on Programming Languages and Systems to the PhD student who has made the most original and influential contribution to the area of Programming Languages and Systems, and has graduated in the period up to November 2011 at a European academic institute. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole.The winner was selected by a committee of international experts. Details on the procedure can be found here. The candidate theses were judged on originality, impact, relevance, and quality of writing. With this award already two researchers associated with the IMDEA Software Institute have received this prestigious recognition.
IMDEA Software Institute researchers Alexey Gotsman and Mark Marron each got one of the 10 Microsoft Software Engineering Innovation Foundation (SEIF) Awards given by Microsoft Research in 2012.
Microsoft Research created these Awards to support research in software engineering technologies, tools, practices, and teaching methods. Out of more than 100 applications, only 8 other applicants, in addition to Alexey Gotsman and Mark Marron from the IMDEA Software Institute in Spain, obtained this prestigious award in 2011, 1 in Switzerland, 1 in Canada, and 6 in the United States.
Alexey Gotsman and Mark Marron will be publicly recognized at the new annual SEIF Day, to be held on 18th of July 2012, in Redmond, USA. This event is a new addition to the SEIF program and will be attended by previous and current SEIF winners, influential software engineering researchers, and researchers from Microsoft Research.
The paper Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations, co-authored by IMDEA Software Institute and UPM Researchers Dragan Ivanović, Manuel Carro, and Manuel Hermenegildo, was selected as the Best Paper Award at ICSOC 2011, the 9th International Conference on Service Computing held at the Paphos, Cyprus, Dec 5–8, 2011.
The paper presents and evaluates a technique to detect ahead of time whether there will be or not SLA violations in service orchestrations, and to determine under which conditions these will (or will not) happen. The technique uses a model of the process which can evolve as the process executes, thus making it possible to reflect dynamic changes. At every inspection point, the continuation of the process model is sent to the predictor which produces a constraint model by means of symbolic execution using a constraint-generating interpreter. The constraint system is fed into a Prolog-based constraint solver which is, additionally, given boundary conditions to represent scenarios of failure and non-failure. The results of the constraint solver indicate the cases under which these scenarios will or may occur. Evaluations under realistic conditions obtained using the Microsoft Workflow Engine indicate significant prediction capacity with very small numbers of false positives / negatives.
The paper Computer-Aided Security Proofs for the Working Cryptographer, co-authored by IMDEA Software Institute Researchers Gilles Barthe and Santiago Zanella with colleagues at INRIA, is the winner of the Best Paper Award at CRYPTO 2011, the 31st International Cryptology Conference held at the University of California, Santa Barbara, Aug 14–18, 2011.
You can see the presentation at CRYPTO'11 here:
The paper presents EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems which uses off-the-shelf SMT solvers and automated theorem provers. The tool is significantly easier to use than its predecessors and is arguably a plausible candidate for adoption by working cryptographers. The usefulness of the tool is illustrated through its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems.
The paper Measuring Pay-per-Install: The Commoditization of Malware Distribution, co-authored by IMDEA Software Institute Assistant Professor Juan Caballero, is the winner of an Outstanding Paper Award at the Usenix Security 2011 Symposium.
The paper reports on recent research by Caballero and colleagues from the University of California, Berkeley, suggesting that most malware in personal computers is covertly installed by enterprising hackers, who sell access to the compromised hosts to criminal gangs in an underground Pay-Per-Install (PPI) market. The article was recently the subject of a feature in MIT's Technology review.
Manuel Hermenegildo, Institute Director, was, with Professors Michael Leuschel (University of Düsseldorf) and Antonio Porto (University of Lisbon) part of the winning team of the 18th Prolog Programming Contest at the 27th International Conference on Logic Programming in Lexington, Kentucky, USA. Of course, this was done using Ciao which was duly declared "this year's Prolog system of choice." And all of this while having to endure being continuously referred to by the contest organizers as the "old boys" team...MIT's Techonology review reports recent research by researchers from the IMDEA Software Institute and University of California, Berkeley, suggesting that most malware in personal computers is covertly installed by enterprising hackers, who sell access to the compromised hosts to criminal gangs in an underground Pay-Per-Install (PPI) market.
Pavithra Prabhakar obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign in 2011, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India.
Pavithra joined the faculty of the IMDEA Software Institute in 2011. She took a one-year leave of absence (August 1 2011 to August 31 2012) at the California Insitute of Technology as a CMI (Center for Mathematics of Information) fellow. She has also spent several summers as an intern at Bell-Labs, Murray Hill, working on formal synthesis of web-services.
She is the recipient of the Sohaib and Sara Abbasi fellowship from UIUC and M.N.S Swamy medal from the Indian Institute of Science.
Her main area of research is in Formal Analysis of Cyber-Physical Systems. She has published widely in Hybrid Systems and Formal Methods conferences and her paper in HSCC has received an honorable mentions award.
The IMDEA Software Institute has published its 2010 Annual Report.
Alexey Gotsman, Assistant Professor at the IMDEA Software Institute, is the winner of the 2010 EAPLS Best Dissertation Award for his dissertation on "Logics and analyses for concurrent heap-manipulating programs" completed at the Computer Laboratory of the University of Cambridge.
This award is given by the European Association on Programming Languages and Systems to the PhD student who has made the most original and influential contribution to the area of Programming Languages and Systems, and has graduated in the period up to November 2010 at a European academic institute. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole.
The winner was selected by a committee of international experts. Details on the procedure can be found here. The candidate theses were judged on originality, impact, relevance, and quality of writing. The conclusions from the jury can be found here.
Laurent Mauborgne, Researcher at the IMDEA Software Institute, is one of the winners of the Intelligent Systems Best Paper Award for his article on "Static Analysis and Verification of Aerospace Software by Abstract Interpretation" presented at 2010 AAIA Infotech@Aerospace.
This award is given by the American Institute of Aeronautics and Astronautics.
John Gallagher has been granted a 3-year research project (2011-2013) by the Danish Natural Science Research Council (FNU). The project is entitled "NUSA: Numerical and Symbolic Abstractions for Software Model Checking". NUSA supports collaboration between Roskilde university and the IMDEA Software Institute, and also with Ben-Gurion University, Israel, IRISA/Univ. Rennes, France and K.U. Leuven, Belgium.
The IMDEA Institutes joined the Madrid events of Researchers Night, an EU-wide initiative bringing together the public at large and researchers once a year on the fourth Friday of September. The 2010 edition took place on 24 September in over 600 venues of 250 European cities in 33 countries. In Madrid there were several activities, including a round table with all the directors of the IMDEA Institutes.
Juan Caballero (Ph.D Carnegie Mellon University) has joined IMDEA Software as an Assistant Research Professor (tenure-track). Before joining IMDEA, he was Visiting Graduate Student at UC Berkeley.
The Counselor for Education of the Madrid Regional Government, Lucía Figar, visits the construction site of the building that will be the permanent location of the IMDEA Software Institute. Press release. Pictures.
Alexey Gotsman (Ph.D. University of Cambridge, 2009) has joined IMDEA Software as an Assistant Research Professor (tenure-track). He previously held a postdoctoral researcher position at the University of Cambridge, where he also obtained his Ph.D.
The IMDEA Software Institute has published its 2008-09 biennial report.
IMDEA Software has organized the ES_PASS Project Workshop on "Industrialization of Abstract Interpretation," held on October 28, 2009 in Madrid (Spain), a succesful experience where the results of the ES_PASS project have been presented to a wide and varied audience of mostly industrial and also some academic participants, and where new contacts and synergies among such participants have been established.
ES_PASS (Embedded Software Product-based Assurance) is an EU ITEA2 project that aims at improving and integrating state-of-the-art software verification techniques based on static analysis into existing industrial engineering processes in the domain of safety-critical embedded systems.
The project consortium includes industrial participants such as Airbus France, AbsInt, CS Systèmes d'Information, Continental Automotive France SAS, Thales Avionics, Daimler AG, Esterel Technologies, PSA Peugeot Citroen, Siemens VDO Automotive, EADS Astrium, GTD Barcelona, Onera, PolySpace Technologies, Thales Transportation, ALCATEL TSD and IFB Berlin, as well as a number of research laboratories and institutes.
Local project coordination and workshop organization: Pedro López-García .
Laurent Mauborgne has joined the Institute in a Researcher position. Laurent was previously assistant professor at École normale superieure and part-time professor at École polytechnique, France. He received his Ph.D. in Computer Science from École Polytechnique, in 1999, and an habilitation à diriger les recherches from University Paris-Dauphine (France) in 2007. His research focuses on static analysis of programs and abstract interpretation. The goal is to develop theoretical as well as practical tools to analyze the behaviors of programs. He is one of the authors of the Astrée analyzer, a tool that proves the absence of run-time errors in critical avionic code.
John Gallagher (jointly with Henning Christiansen) wins the Best Paper Award at the International Conference on Logic Programming 2009 in Pasadena, CA, USA, for the paper "Non-Discriminating Arguments and Their Uses". The award is given by the Association for Logic Programming.
Gilles Barthe, Manuel Hermenegildo, and Manuel Clavel attended the HATS kick-off meeting, held in Bologna, Italy, on March 9-11, 2009. HATS is a recently approved FP7 IP project which focuses on the rigorous development of software product families (SWPF). The technical core of the project is an Abstract Behavioral Specification language which will allow precise description of SWPF features and components and their instances. IMDEA Software is part of the HATS consortium, in collaboration with UPM, along with 7 other academic partners, 2 research institutes, and 1 SME.
The IMDEA Institutes network granted a 7FP (PEOPLE-COFUND) Marie-Curie Action for researcher mobility. The program, called AMAROUT, co-finances for one year (renewable for two or three) the integration of more than 130 researchers in the IMDEA network of institutes. The duration of the AMAROUT program is 4 years, beginning on March 1st, 2009. IMDEA Software is the proposer and coordinator of the AMAROUT program.
Building designs from six renowned architects were received in response to our call for design ideas for a new building to be the permanent location of the Institute. In november 2008 a committee formed by members of IMDEA Software, the Madrid Regional Government, and external experts chose the winning design, presented by Estudio Lamela. Construction of this new building will begin shortly and will be ready when the Institute outgrows its current temporary location in a floor of the UPM CS Department.