Presentation: Logic-Based Automated Reasoning

Track: Modern CS in the Real World

Location: Pacific DEKJ

Duration: 2:55pm - 3:45pm

Day of week: Wednesday

Level: Advanced

Persona: Developer

Abstract

Developing efficient and scalable software analysis tools is a tedious and very difficult task. First, due to the undecidability of the verification problem, tools, must be highly tuned and engineered to provide reasonable efficiency and precision trade-offs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. In this talk, I will present SeaHorn — an open source automated logic-based reasoning tool built on top of LLVM -- an industrial compiler infrastructure. SeaHorn combines traditional and advanced automated reasoning algorithms based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is a versatile and highly customizable tool which allows developers to easily build or experiment with new verification techniques.

Speaker: Temesghen Kahsai

Software Engineer, previously Research Scientist @NASAAmes

Temesghen works as a software engineer. His primary role at his current company is to develop automated logic-based verification tools for cloud security. Previously, he was a research scientist in the Robust Software Engineering group at NASA Ames, working on software verification tools for mission critical systems. During his tenure at NASA, he was also affiliated as a senior system scientist at Carnegie Mellon University (Cylab) where he led three research projects funded by NASA, NSF and DARPA. Temesghen holds a PhD in computer science from the University of Wales in Swansea.

Find Temesghen Kahsai at

.

Tracks

  • 21st Century Languages

    Compile to Native, Microservices, Machine learning... tailor-made languages solving modern challenges, featuring use cases around Go, Rust, C#, and Elm.

  • Architectures You've Always Wondered About

    Architectural practices from the world's most well-known properties, featuring startups, massive scale, evolving architectures, and software tools used by nearly all of us.

  • Beyond Being an Individual Contributor

    Beyond being an individual contributor. Building and Evolving managers and tech leadership.

  • DevOps: You Build It, You Run It

    Pushing DevOps beyond adoption into cultural change. Hear about designing resilience, managing alerting, CI/CD lessons, & security. Features lessons from open source, Linkedin, Netflix, Financial Times, & more. 

  • Performance Mythbusting

    Real world, applied performance proofs across stacks. Hear performance consideratiosn for .NET, Python, & Java. Learn performance use cases with OpenJ9, Instagram, and Netflix. 

  • The Practice & Frontiers of AI

    Learn about machine learning in practice and on the horizon. Learn about ML at Quora, Uber's Michelangelo, ML workflow with Netflix Meson and topics on Bots, Conversational interfaces, automation, and deployment practices in the space.

  • Going Serverless

    Learn about the state of Serverless & how to successfully leverage it! Lessons learned in the track hit on security, scalability, IoT, and offer warnings to watch out for.

  • Microservices: Patterns and Practices

    Stories of success and failure building modern Microservices, including event sourcing, reactive, decomposition, & more.

  • Evolving Java

    Java continues to evolve & change. Track covers Spring 5, async, Kotlin, serverless, the 6-month cadence plans, & AI/ML use cases.

  • The Art of Chaos Engineering

    Failure is going to happen - Are you ready? Chaos engineering is an emerging discipline - What is the state of the art?

  • Security: Attacking and Defending

    Offense and defensive security evolution that application developers should know about including SGX Enclaves, effects of AI, software exploitation techniques, & crowd defense

  • Stream Processing In The Modern Age

    Compelling applications of stream processing using Flink, Beam, Spark, Strymon & recent advances in the field, including Custom Windowing, Stateful Streaming, SQL over Streams.  

Conference for Professional Software Developers