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...