Software Seminar Series (S3)
Tuesday, November 25, 2014
Alejandro Sánchez, PhD Student, IMDEA Software InstituteInvariant Generation for Parametrized Systems using Self-Reflection
Abstract: We examine the problem of inferring invariants for parametrized systems. Parametrized systems are concurrent systems con...
Tuesday, November 18, 2014
Michael Ernst, Faculty (visiting), IMDEA Software InstituteCollaborative verification of information flow for a high-assurance app store
Abstract: Malware is a serious problem on mobile devices. Our vision is a verified app store in which each application has been fo...
Tuesday, November 11, 2014
Joaquín Arias, PhD Student, IMDEA Software InstituteFailure Tabled Constraint Logic Programming by Interpolation
Abstract: In this talk we present the framework Failure Tabled Constraint Logic Programming by Interpolation, FTCLP (Gange et al. ...
Tuesday, November 4, 2014
Remy Haemmerle, Post-doctoral Researcher, IMDEA Software InstituteInductive Proofs over CLP as Commutation Proofs
Abstract: In this talk we present a constraint logic framework that combines backward and forward chaining. Concretely in this fra...
Tuesday, October 28, 2014
Dragan Ivanović, Post-doctoral Researcher, IMDEA Software InstituteTransforming Service Compositions Into Cloud-Friendly Actor Networks
Abstract: In Service-Oriented Architecture (SOA), service compositions provide the key tool for building complex, flexible, distri...
Tuesday, October 21, 2014
Germán Delbianco, PhD Student, IMDEA Software InstituteConcurrent Hoare-style Reasoning, deconstructed
Abstract: Most logics for stateful reasoning in a concurrent setting are designed around a parallel composition operator ||. Given...
Monday, October 13, 2014
Viktor Vafeiadis, Faculty (tenure-track), Max Planck Institute for Software Systems, GermanyReasoning about the C/C++ weak memory model
Abstract: The talk will introduce the C11 weak memory model that defines the semantics of concurrent C/C++ programs, and will answ...
Tuesday, October 7, 2014
Pierre-Yves Strub, Researcher, IMDEA Software InstituteA Formal Library for Elliptic Curves in the Coq Proof Assistant
Abstract: I will present in this talk some insights about the formalization of mathematics, using the case study of a formal devel...
Tuesday, September 23, 2014
Carolina Dania, PhD Student, IMDEA Software InstituteAnalysis of OCL properties on static and dynamic UML models
Abstract: I will present a mapping from OCL (Object Constraint Language) to first-order logic. This mapping allows us to reason on...
Tuesday, June 17, 2014
Miriam Garcia, PhD Student, IMDEA Software InstituteCounterexample guided abstraction refinement for stability analysis of hybrid systems
Abstract: Hybrid systems refer to dynamical systems exhibiting a mixed discrete and continuous behaviours. Such behaviors appear n...
Tuesday, June 10, 2014
Julian Samborski-Forlese, PhD Student, IMDEA Software InstituteBounded Model Checking of Regular Linear Temporal Logic
Abstract: Bounded model checking (BMC) is an effective algorithmic method for the verification of finite state systems against tem...
Tuesday, May 27, 2014
Nataliia Stulova, PhD Student, IMDEA Software InstituteAssertion-based Debugging of Higher-Order (C)LP Programs
Abstract: Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactical...
Tuesday, May 13, 2014
Ilya Sergey, Post-doctoral Researcher, IMDEA Software InstituteHoare-Style Reasoning about Non-Blocking Concurrent Algorithms
Abstract: How would one specify a correct behaviour of an optimistic fine-grained concurrent data structure? For more than twenty ...
Tuesday, May 6, 2014
Burcu Kulahcioglu Ozkan, PhD Student, Koç UniversityExploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs
Abstract: As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming er...
Tuesday, April 29, 2014
Zorana Bankovic, Post-doctoral Researcher, IMDEA Software InstituteStochastic vs. Deterministic Scheduling and Allocation. Case study: Optimal Energy-aware Scheduling for XMOS Chips
Abstract: The most common approach for solving the problem of optimal task scheduling is to use expected values of the variables t...
Tuesday, April 8, 2014
Andrea Cerone, Post-doctoral Researcher, IMDEA Software InstituteParametrised Linearisability
Abstract: Many concurrent libraries are parameterised, meaning that they implement generic algorithms that take another library as...
Tuesday, February 18, 2014
Marek Zawirski, PhD Student, INRIAFrom Large-Scale to Extreme-Scale : Extending Causal+ Consistency to Client Nodes
Abstract: Modern web applications are backed by geo-replicated data stores that offer highly available and low latency data access...