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