IMDEA initiative
Abstract: It is well known that various scalability issues affect automated formal verification, and thus some approaches need to ...
Abstract: CAPTCHA systems have been widely deployed to identify and block fraudulent bot traffic. However, current solutions, such...
Abstract: Embedded software plays a steadily increasing role in all industrial sectors, and in several such sectors software is re...
Abstract: Model-based testing (MBT) is a systematic way of black-box testing of a system under test (SUT) with respect to behaviou...
Abstract: Despite the recent improvements in automatic test case generation, test case generators do not yet handle well programs ...
Abstract: Post-quantum cryptography is public-key cryptography resistant to future quantum computers. In this talk we will talk ab...
Abstract: In this position talk we briefly retrace the historic and evolutionary context that led to AI’s results not necess...
Abstract: Multiparty Computation (MPC) protocols allow a set of mutually distrustful parties to compute a program without revealin...
Abstract: We present a Bounded Model Checking technique for higher-order programs based on defunctionalization and points-to analy...
Abstract: Offchain protocols aim at bypassing the scalability and privacy limitations of classic blockchains by allowing a subset ...
Abstract: Replicated data stores provide highly available, low-latency access to data at the expense of consistency, i.e., observe...
Abstract: Transaction commit protocols play a pivotal role in supporting scalability and availability guarantees of today’s ...
Abstract: Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or auto...
Abstract: Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is...
Abstract: Trusted hardware is one of the most complex and desired components of modern computers. For example, almost all mobile p...
Abstract: Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed p...
Abstract: In this talk, we introduce proof-relevant resolution, a framework for constructive proof automation. The intended applic...
Abstract: Secure multiparty computation studies deals with privacy-preserving computation, where several parties, some of them hol...
Abstract: In this talk, I will present pretend synchrony, a new approach to verifying distributed systems, based on the observatio...
Abstract: Modern CPUs employ speculative execution to avoid expensive pipeline stalls by predicting the outcome of branching (and ...
Abstract: The practical successes of Machine Learning (ML) in different settings motivates the ability of computing small explanat...
Abstract: Many artifacts that software developers produce are written in natural language: code comments, commit messages, text in...
Abstract: Etherum smart contracts written in higher level programming languages like Solidity or Viper are compiled to bytecode, w...
Abstract: Verifying a program consist of proving that a given program meets its specification. Various frameworks have been studie...
Abstract: Fabric is a modular and extensible open-source system for deploying and operating permissioned blockchains and one of th...
Abstract: Few technological advances have affected as many aspects of science, economy, and society in general as the ability to c...
Abstract: For decades, programmers have interacted with persistent storage via a well-defined block-based API, namely, that of the...
Abstract: Modern-day software is increasingly complex and software engineering is commonly accepted as a challenging, error-prone ...
Abstract: The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other syst...
Abstract: Security often fails in practice due to a lack of understanding of the nuances in real-world systems. For example, users...
Abstract: Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by...
Abstract: Today’s online services must meet strict availability and performance requirements. State machine replication, one of th...
Abstract: Parsing is sometimes thought of as a solved problem. However, recent advances show that there is still much to be discov...
Abstract: Decision trees with hard decision nodes stand apart from other machine learning models in their interpretability, fast i...
Abstract: Security auditing, i.e., the examination of the source code for the purpose of detecting vulnerabilities, helps to detec...
