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) programme, 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. Coordinator contact: Marta Sedano.
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
Website: ENTRA
The IMDEA Network of institutes have been granted AMAROUT-II, an EU Marie Curie (PEOPLE-COFUND) programme 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, 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 researcher skills. AMAROUT-II is a continuation of AMAROUT, a highly successful COFUND programme which is now closed for applications.
For more information see AMAROUT-II. Coordinator contact: Marta Sedano.
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...
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.
Manuel Hermenegildo, Director of IMDEA Software, has been elected to the Academia Europaea.
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 received approval for a 7FP (PEOPLE-COFUND) Marie-Curie Action for researcher mobility called AMAROUT. The programme co-finances for one year (renewable for two or three) the incorporation of more than 130 researchers into the IMDEA network of institutes. The duration of the AMAROUT programme is 4 years, beginning on March 1st, 2009. IMDEA Software is the coordinator of the AMAROUT programme.
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.