Viewing Results for Category: Tech Talks (1 of 18 Pages)

Tech talk: Adversarial Machine Learning, Privacy, and Cybersecurity in the Age of Data Science

abstract: Due to the exponential growth of our ability to collect, centralize, and share data in recent years we have been able tackle problems previously assumed to be insurmountable. Ubiquitous sensors, fast and efficient machine learning, and affordable commercial-off-the-shelf technologies have not only deepened our understanding of our world, but also democratized these capabilities. As […]

Read More

Tech talk: Toward Extracting Monadic Programs from Proofs

abstract: The Curry-Howard Isomorphism motivates the well known proofs-as-programs interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a -> (a -> M b) -> […]

Read More

Tech talk: Designing a practical dependently typed language

abstract: The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In […]

Read More

Tech talk: Evidence-based Trust of Symbolic Execution-based Verification

abstract: Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in […]

Read More

Tech Talk: Viper: Verification Infrastructure for Permission-based Reasoning

abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from […]

Read More

Tech talk: A Brief History of Verifiable Elections

abstract: Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that […]

Read More