https://simplecast.com Building Better Systems Exploring tools and approaches that make us more effective engineers and make our systems safe and reliable. Join us for discussions on recent developments in topics such as best practices in reliability and security, applied formal methods, encryption, and safe and secure hardware. en Tue, 9 Aug 2022 23:25:12 +0000 Tue, 9 Aug 2022 23:25:23 +0000 https://building-better-systems.simplecast.com Building Better Systems https://image.simplecastcdn.com/images/ecc890e5-273f-482c-b857-104c82b15493/68d510da-7868-4c7d-9005-9de002599df4/3000x3000/bbs-logo-for-simplecast2.jpg?aid=rss_feed https://building-better-systems.simplecast.com episodic Exploring tools and approaches that make us more effective engineers and make our systems safe and reliable. Join us for discussions on recent developments in topics such as best practices in reliability and security, applied formal methods, encryption, and safe and secure hardware. Galois, Joey Dodds, Shpat Morina no https://feeds.simplecast.com/JdJ0jEHv Galois Inc. marketing@galois.com c655c73e-d1c6-4144-8edb-61bb52a5043d Episode #22: Eric Daimler — Guaranteeing the Integrity of Data Models with Category Theory In this episode, we're joined by Eric Daimler, CEO & co-founder of Conexus AI, Inc, an MIT spin out. We discuss the Conexus software platform, which is built on top of breakthroughs in the mathematics of Category Theory, and how it guarantees the integrity of universal data models. Eric shares real-world examples of applying this approach to various complex industries, such as transportation and logistics, avionics, and energy.

Listen to this episode wherever you listen to podcasts. 

Eric Daimler: https://www.linkedin.com/in/ericdaimler/ 

Joey Dodds: https://www.linkedin.com/in/joey-dodds-4b462a41/ 

Rob Dockins: https://galois.com/team/robert-dockins/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Tue, 9 Aug 2022 23:25:12 +0000 marketing@galois.com (Rob Dockins, Eric Daimler, Joey Dodds) https://building-better-systems.simplecast.com/episodes/episode-22-eric-daimler-guaranteeing-the-integrity-of-data-models-with-category-theory-LNd7Nvrp In this episode, we're joined by Eric Daimler, CEO & co-founder of Conexus AI, Inc, an MIT spin out. We discuss the Conexus software platform, which is built on top of breakthroughs in the mathematics of Category Theory, and how it guarantees the integrity of universal data models. Eric shares real-world examples of applying this approach to various complex industries, such as transportation and logistics, avionics, and energy.

Listen to this episode wherever you listen to podcasts. 

Eric Daimler: https://www.linkedin.com/in/ericdaimler/ 

Joey Dodds: https://www.linkedin.com/in/joey-dodds-4b462a41/ 

Rob Dockins: https://galois.com/team/robert-dockins/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Episode #22: Eric Daimler — Guaranteeing the Integrity of Data Models with Category Theory Rob Dockins, Eric Daimler, Joey Dodds 00:37:50 In this episode, we're joined by Eric Daimler, CEO & co-founder of Conexus AI, Inc, an MIT spin out. We discuss the Conexus software platform, which is built on top of breakthroughs in the mathematics of Category Theory, and how it guarantees the integrity of universal data models. Eric shares real-world examples of applying this approach to various complex industries, such as transportation and logistics, avionics, and energy. Listen to this episode wherever you listen to podcasts. Eric Daimler: https://www.linkedin.com/in/ericdaimler/ Joey Dodds: https://www.linkedin.com/in/joey-dodds-4b462a41/ Rob Dockins: https://galois.com/team/robert-dockins/ Galois, Inc.: https://galois.com/ Contact us: podcast@galois.com In this episode, we're joined by Eric Daimler, CEO & co-founder of Conexus AI, Inc, an MIT spin out. We discuss the Conexus software platform, which is built on top of breakthroughs in the mathematics of Category Theory, and how it guarantees the integrity of universal data models. Eric shares real-world examples of applying this approach to various complex industries, such as transportation and logistics, avionics, and energy. Listen to this episode wherever you listen to podcasts. Eric Daimler: https://www.linkedin.com/in/ericdaimler/ Joey Dodds: https://www.linkedin.com/in/joey-dodds-4b462a41/ Rob Dockins: https://galois.com/team/robert-dockins/ Galois, Inc.: https://galois.com/ Contact us: podcast@galois.com no full 22 b3ca86e4-d7e1-40af-b7da-14c30b548271 Episode #21: Nikhil Swamy — Fully In Bed With Dependent Types Today we're joined by Nikhil Swamy, Senior Principal Researcher in the RiSE group at Microsoft Research. We are very excited to hear about what he's been working on. In particular, we're going discuss a language that he's co-created and continually develops called F* (pronounced F star). F* is a dependently typed language that you can both program and prove things about the programs that you write. We'll talk about what makes that language special and unique from other similar languages, as well as some of the applications of F*.

 

Watch all our episodes on the Building Better Systems YouTube channel

Nikhil Swamy: https://www.microsoft.com/en-us/research/people/nswamy/

F*: https://www.fstar-lang.org/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

 

]]> Fri, 10 Jun 2022 21:26:55 +0000 marketing@galois.com (Nikhil Swamy, Shpat Morina, Joey Dodds, Galois) https://building-better-systems.simplecast.com/episodes/episode-21-nikhil-swamy-fully-in-bed-with-dependent-types-XMvzzyHf Today we're joined by Nikhil Swamy, Senior Principal Researcher in the RiSE group at Microsoft Research. We are very excited to hear about what he's been working on. In particular, we're going discuss a language that he's co-created and continually develops called F* (pronounced F star). F* is a dependently typed language that you can both program and prove things about the programs that you write. We'll talk about what makes that language special and unique from other similar languages, as well as some of the applications of F*.

 

Watch all our episodes on the Building Better Systems YouTube channel

Nikhil Swamy: https://www.microsoft.com/en-us/research/people/nswamy/

F*: https://www.fstar-lang.org/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

 

]]> Episode #21: Nikhil Swamy — Fully In Bed With Dependent Types Nikhil Swamy, Shpat Morina, Joey Dodds, Galois 00:48:45 Today we're joined by Nikhil Swamy, Senior Principal Researcher in the RiSE group at Microsoft Research. We are very excited to hear about what he's been working on. In particular, we're going discuss a language that he's co-created and continually develops called F* (pronounced F star). F* is a dependently typed language that you can both program and prove things about the programs that you write. We'll talk about what makes that language special and unique from other similar languages, as well as some of the applications of F*. Today we're joined by Nikhil Swamy, Senior Principal Researcher in the RiSE group at Microsoft Research. We are very excited to hear about what he's been working on. In particular, we're going discuss a language that he's co-created and continually develops called F* (pronounced F star). F* is a dependently typed language that you can both program and prove things about the programs that you write. We'll talk about what makes that language special and unique from other similar languages, as well as some of the applications of F*. no full 21 d13d265a-6080-4c6e-a975-93352f6619b4 Episode #20: Ankush Desai — P: The Modeling Language That Could Joey and Shpat talk with Ankush Desai, a Senior Applied Scientist at AWS and one of the primary developers behind the P language. They dig into uses for P, bug finding, and what it takes for formal methods researchers to build useful tools for applied engineers. 

Watch all our episodes on the Building Better Systems youtube channel.

Ankush Desai: https://www.linkedin.com/in/ankush-desai/ 

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

 

 

]]> Thu, 28 Apr 2022 17:21:54 +0000 marketing@galois.com (Ankush Desai, Shpat Morina, Joey Dodds, Galois) https://building-better-systems.simplecast.com/episodes/episode-20-ankush-desai-p-the-language-that-could-SAQf9LS8 Joey and Shpat talk with Ankush Desai, a Senior Applied Scientist at AWS and one of the primary developers behind the P language. They dig into uses for P, bug finding, and what it takes for formal methods researchers to build useful tools for applied engineers. 

Watch all our episodes on the Building Better Systems youtube channel.

Ankush Desai: https://www.linkedin.com/in/ankush-desai/ 

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

 

 

]]> Episode #20: Ankush Desai — P: The Modeling Language That Could Ankush Desai, Shpat Morina, Joey Dodds, Galois 00:46:12 Joey and Shpat talk with Ankush Desai, a Senior Applied Scientist at AWS and one of the primary developers behind the P language. They dig into uses for P, bug finding, and what it takes for formal methods researchers to build useful tools for applied engineers. Joey and Shpat talk with Ankush Desai, a Senior Applied Scientist at AWS and one of the primary developers behind the P language. They dig into uses for P, bug finding, and what it takes for formal methods researchers to build useful tools for applied engineers. no full 20 6203fdf9-7cb2-4133-bbed-385529efbdd6 #19: Steve Weis — Security Shouldn't Be the Last Check Box In this episode, we talk with Steve Weis, a Senior Staff Security Engineer at Databricks with extensive knowledge of security, cryptography, and software engineering. Steve shares his experience working for large companies like Google and Facebook and how their security needs differ from start-ups and companies trying to scale. He talks about why he thinks companies should share more about how they design their infrastructure and how they can develop a “security mindset” so even non-security-related roles can contribute to building secure systems. 

Watch all our episodes on the Building Better Systems youtube channel.

Steve Weis: https://www.linkedin.com/in/stephenweis/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Thu, 14 Apr 2022 21:40:10 +0000 marketing@galois.com (Galois Inc.) https://building-better-systems.simplecast.com/episodes/19-steve-weis-security-cant-be-the-last-check-box-Jpoi2DdX In this episode, we talk with Steve Weis, a Senior Staff Security Engineer at Databricks with extensive knowledge of security, cryptography, and software engineering. Steve shares his experience working for large companies like Google and Facebook and how their security needs differ from start-ups and companies trying to scale. He talks about why he thinks companies should share more about how they design their infrastructure and how they can develop a “security mindset” so even non-security-related roles can contribute to building secure systems. 

Watch all our episodes on the Building Better Systems youtube channel.

Steve Weis: https://www.linkedin.com/in/stephenweis/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #19: Steve Weis — Security Shouldn't Be the Last Check Box Galois Inc. 00:41:36 In this episode, we talk with Steve Weis, a Senior Staff Security Engineer at Databricks with extensive knowledge of security, cryptography, and software engineering. Steve shares his experience working for large companies like Google and Facebook and how their security needs differ from start-ups and companies trying to scale. He talks about why he thinks companies should share more about how they design their infrastructure and how they can develop a “security mindset” so even non-security-related roles can contribute to building secure systems. In this episode, we talk with Steve Weis, a Senior Staff Security Engineer at Databricks with extensive knowledge of security, cryptography, and software engineering. Steve shares his experience working for large companies like Google and Facebook and how their security needs differ from start-ups and companies trying to scale. He talks about why he thinks companies should share more about how they design their infrastructure and how they can develop a “security mindset” so even non-security-related roles can contribute to building secure systems. no full 19 c565ce54-306e-4c83-9872-956440548d48 #18: Jordan Kyriakidis — Helping People Write More Useful Requirements In episode #18, we chat with Jordan Kyriakidis, co-founder and CEO of QRA Corp. QRA is developing QVScribe, a product that helps engineers write requirements and analyze those requirements to gauge whether they are framed well and capture the writer's intent.

We discuss the impact of writing good, early-stage design requirements, how they impact your system, how to write better requirements, the state of natural language processing, and machine learning for this use case. We also talk about applying those in situations where you need explainability and where ambiguity is unacceptable.

Watch all our episodes on the Building Better Systems youtube channel.

Jordan Kyriakidis: https://www.linkedin.com/in/jordankyriakidis/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Wed, 9 Mar 2022 16:47:13 +0000 marketing@galois.com (Joey Dodds, Shpat Morina, Galois, Jordan Kyriakidis) https://building-better-systems.simplecast.com/episodes/18-jordan-kyriakidis-helping-people-write-more-useful-requirements-EMUjaRoL In episode #18, we chat with Jordan Kyriakidis, co-founder and CEO of QRA Corp. QRA is developing QVScribe, a product that helps engineers write requirements and analyze those requirements to gauge whether they are framed well and capture the writer's intent.

We discuss the impact of writing good, early-stage design requirements, how they impact your system, how to write better requirements, the state of natural language processing, and machine learning for this use case. We also talk about applying those in situations where you need explainability and where ambiguity is unacceptable.

Watch all our episodes on the Building Better Systems youtube channel.

Jordan Kyriakidis: https://www.linkedin.com/in/jordankyriakidis/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #18: Jordan Kyriakidis — Helping People Write More Useful Requirements Joey Dodds, Shpat Morina, Galois, Jordan Kyriakidis 00:47:19 In episode #18, we chat with Jordan Kyriakidis, co-founder and CEO of QRA Corp. QRA is developing QVScribe, a product that helps engineers write requirements and analyze those requirements to gauge whether they are framed well and capture the writer's intent. We discuss the impact of writing good, early-stage design requirements, how they impact your system, how to write better requirements, the state of natural language processing, and machine learning for this use case. We also talk about applying those in situations where you need explainability and where ambiguity is unacceptable. In episode #18, we chat with Jordan Kyriakidis, co-founder and CEO of QRA Corp. QRA is developing QVScribe, a product that helps engineers write requirements and analyze those requirements to gauge whether they are framed well and capture the writer's intent. We discuss the impact of writing good, early-stage design requirements, how they impact your system, how to write better requirements, the state of natural language processing, and machine learning for this use case. We also talk about applying those in situations where you need explainability and where ambiguity is unacceptable. no full 18 756d2e93-f42d-4d17-9868-4b93aa94f3a2 #17: Iain Whiteside — The Twists and Turns of Validating Neural Networks for Autonomous Driving (Part 2) In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise.

Watch all our episodes on the Building Better Systems youtube channel.

Iain Whiteside: https://www.linkedin.com/in/iainjw

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Wed, 9 Feb 2022 17:12:49 +0000 marketing@galois.com (Galois, Joey Dodds, Shpat Morina, Iain Whiteside) https://building-better-systems.simplecast.com/episodes/17-iain-whiteside-validating-neural-networks-for-autonomous-driving-part-2-aTpBjgPd In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise.

Watch all our episodes on the Building Better Systems youtube channel.

Iain Whiteside: https://www.linkedin.com/in/iainjw

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #17: Iain Whiteside — The Twists and Turns of Validating Neural Networks for Autonomous Driving (Part 2) Galois, Joey Dodds, Shpat Morina, Iain Whiteside 00:28:38 In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise. In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise. no full 17 87d381ff-96c5-495c-b647-f734e737453c #16: Iain Whiteside – Autonomous Driving: Reasoning About the Rules of the Road (Part 1) In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise.

Watch all our episodes on the Building Better Systems youtube channel.

Iain Whiteside: https://www.linkedin.com/in/iainjw

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Wed, 9 Feb 2022 17:12:31 +0000 marketing@galois.com (Galois, Joey Dodds, Shpat Morina, Iain Whiteside) https://building-better-systems.simplecast.com/episodes/16-iain-whiteside-autonomous-driving-reasoning-about-the-rules-of-the-road-QXtb5tNb In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise.

Watch all our episodes on the Building Better Systems youtube channel.

Iain Whiteside: https://www.linkedin.com/in/iainjw

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #16: Iain Whiteside – Autonomous Driving: Reasoning About the Rules of the Road (Part 1) Galois, Joey Dodds, Shpat Morina, Iain Whiteside 00:56:25 In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise. In this two-part episode, we speak with Iain Whiteside about the challenges and some of the more novel solutions to make autonomous vehicles safer and easier to program. In part 1, we discuss how Ian and his team formalize and check the different actions and situations that a car finds itself in while on the road. In part 2, we discuss how you might validate the accuracy of neural networks that sense the world, and how to mitigate issues that might arise. no full 16 a5bdab02-7ea4-43f3-bff4-a4bd923042b9 #15: Dr. Kathleen Fisher – Sparking the New Age of Formal Verification at DARPA In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf!

Watch all our episodes on the Building Better Systems youtube channel.

Dr. Kathleen Fisher: https://www.darpa.mil/staff/dr-kathleen-fisher 

HACMS: https://www.darpa.mil/program/high-assurance-cyber-military-systems PADS: https://pads.cs.tufts.edu/about.html 

From Dirt to Shovels paper: https://www.cs.princeton.edu/~dpw/papers/learningpopl08-final.pdf 

Hancock: https://dl.acm.org/doi/abs/10.1145/331960.331981

PLMW: http://sigplan.org/Conferences/PLMW/ CRAW: https://cra.org/cra-wp/ 

NSF Broadening Participation in Computing: https://beta.nsf.gov/funding/opportunities/broadening-participation-computing-bpc-0 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Mon, 10 Jan 2022 16:44:42 +0000 marketing@galois.com (Joey Dodds, Shpat Morina, Kathleen Fisher, Galois) https://building-better-systems.simplecast.com/episodes/episode-15-dr-kathleen-fisher-sparking-the-new-age-of-formal-verification-at-darpa-6CwIhSkC In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf!

Watch all our episodes on the Building Better Systems youtube channel.

Dr. Kathleen Fisher: https://www.darpa.mil/staff/dr-kathleen-fisher 

HACMS: https://www.darpa.mil/program/high-assurance-cyber-military-systems PADS: https://pads.cs.tufts.edu/about.html 

From Dirt to Shovels paper: https://www.cs.princeton.edu/~dpw/papers/learningpopl08-final.pdf 

Hancock: https://dl.acm.org/doi/abs/10.1145/331960.331981

PLMW: http://sigplan.org/Conferences/PLMW/ CRAW: https://cra.org/cra-wp/ 

NSF Broadening Participation in Computing: https://beta.nsf.gov/funding/opportunities/broadening-participation-computing-bpc-0 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #15: Dr. Kathleen Fisher – Sparking the New Age of Formal Verification at DARPA Joey Dodds, Shpat Morina, Kathleen Fisher, Galois 00:55:52 In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf! In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf! kathleen fisher, darpa, formal methods no full 15 0c10b224-6e17-46a7-8ce0-73087eb8f297 #14: Leo de Moura — Combining the Worlds of Automated and Interactive Theorem Proving In Lean In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Leo de Moura: https://www.microsoft.com/en-us/research/people/leonardo/

Galois, Inc.: https://galois.com/

Contact us: podcast@galois.com

]]> Fri, 3 Dec 2021 21:44:07 +0000 marketing@galois.com (Leo de Moura, Joey Dodds, Galois, Shpat Morina) https://building-better-systems.simplecast.com/episodes/14-leo-de-moura-combining-the-worlds-of-automated-and-interactive-theorem-proving-in-lean-p7ypyYNF In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Leo de Moura: https://www.microsoft.com/en-us/research/people/leonardo/

Galois, Inc.: https://galois.com/

Contact us: podcast@galois.com

]]> #14: Leo de Moura — Combining the Worlds of Automated and Interactive Theorem Proving In Lean Leo de Moura, Joey Dodds, Galois, Shpat Morina 00:45:35 In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert no full 14 080f8417-0a4d-40f3-bfb0-fe9291eed677 #13: Rod Chapman – It's Either Automated or It's Wrong Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Rod Chapman: linkedin.com/in/rod-chapman-7b60266

https://github.com/rod-chapman/SPARKNaCl

Galois, Inc.: https://galois.com/

Contact us: podcast@galois.com

]]> Fri, 24 Sep 2021 19:18:09 +0000 marketing@galois.com (Galois Inc.) https://building-better-systems.simplecast.com/episodes/13-rod-chapman-its-either-automated-or-its-wrong-Ia91t7Z_ Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Rod Chapman: linkedin.com/in/rod-chapman-7b60266

https://github.com/rod-chapman/SPARKNaCl

Galois, Inc.: https://galois.com/

Contact us: podcast@galois.com

]]> #13: Rod Chapman – It's Either Automated or It's Wrong Galois Inc. 00:44:03 Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations. Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations. no full 13 37526e69-7275-4c53-bbed-b0e883a959d4 #12: Alex Malozemoff & Marc Rosen – Censorship Circumvention with ROCKY Balboa We chat with Alex Malozemoff and Marc Rosen about a recently published paper on a novel system for censorship circumvention, and it's corresponding implementation. The paper authors also include James Parker.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Alex Malozemoff: https://galois.com/team/alex-malozemoff/

Marc Rosen: https://galois.com/team/marc-rosen/ 

Paper referenced: Balboa: Bobbing and Weaving Around Network Censorship: https://arxiv.org/abs/2104.05871

]]> Thu, 12 Aug 2021 17:45:19 +0000 marketing@galois.com (Shpat Morina, Joey Dodds, Galois, Alex Malozemoff, Marc Rosen) https://building-better-systems.simplecast.com/episodes/12-alex-malozemoff-marc-rosen-censorship-circumvention-with-rocky-balboa-P7JseXJ9 We chat with Alex Malozemoff and Marc Rosen about a recently published paper on a novel system for censorship circumvention, and it's corresponding implementation. The paper authors also include James Parker.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Alex Malozemoff: https://galois.com/team/alex-malozemoff/

Marc Rosen: https://galois.com/team/marc-rosen/ 

Paper referenced: Balboa: Bobbing and Weaving Around Network Censorship: https://arxiv.org/abs/2104.05871

]]> #12: Alex Malozemoff & Marc Rosen – Censorship Circumvention with ROCKY Balboa Shpat Morina, Joey Dodds, Galois, Alex Malozemoff, Marc Rosen 00:30:58 We chat with Alex Malozemoff and Marc Rosen about a recently published paper, "Balboa: Bobbing and Weaving Around Network Censorship," on a novel system for censorship circumvention and its corresponding implementation. The paper authors also include James Parker. We chat with Alex Malozemoff and Marc Rosen about a recently published paper, "Balboa: Bobbing and Weaving Around Network Censorship," on a novel system for censorship circumvention and its corresponding implementation. The paper authors also include James Parker. no full 12 bb9e5b15-a195-45cf-a9ed-ec2c9712e1d0 #11: Alastair Reid – Meeting Developers Where They Are Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Alastair Reid's paper project: https://alastairreid.github.io/RelatedWork/papers/

Rust verification tools: https://github.com/project-oak/rust-verification-tools

Meeting Developers Where They Are paper: https://arxiv.org/abs/2010.16345

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Fri, 23 Jul 2021 18:47:10 +0000 marketing@galois.com (Galois Inc.) https://building-better-systems.simplecast.com/episodes/11-alastair-reid-meeting-developers-where-they-are-TSRN2M5n Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Alastair Reid's paper project: https://alastairreid.github.io/RelatedWork/papers/

Rust verification tools: https://github.com/project-oak/rust-verification-tools

Meeting Developers Where They Are paper: https://arxiv.org/abs/2010.16345

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #11: Alastair Reid – Meeting Developers Where They Are Galois Inc. 00:36:18 Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust. Alastair Reid describes Google's efforts to bring formal methods to developers so that they can be useful today. We cover a recent publication describing their approach, Alastair's project to document all of the papers he read for a year, and a prototype tool that they've been building to demonstrate formal verification tools in rust. no full 11 a97f56bb-0824-4eee-b9af-36685b9e46f8 #10: Gregory Malecha – Formal Methods and Systems Programmers Working Together Gregory Malecha talks with Joey and Shpat about Bedrock, a startup bringing systems engineers together with formal methods engineers to build some of the most secure and correct systems in the world. 

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Gregory Malecha: https://www.linkedin.com/in/gregory-malecha-91a71469/

https://gmalecha.github.io/

Formal Methods for the  Informal Engineer: https://fmie2021.github.io/agenda.html 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Fri, 11 Jun 2021 18:47:05 +0000 marketing@galois.com (Galois, Gregory Malecha, Joey Dodds, Shpat Morina) https://building-better-systems.simplecast.com/episodes/10-gregory-malecha-formal-methods-and-systems-programmers-working-together-ctKi_vLT Gregory Malecha talks with Joey and Shpat about Bedrock, a startup bringing systems engineers together with formal methods engineers to build some of the most secure and correct systems in the world. 

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Gregory Malecha: https://www.linkedin.com/in/gregory-malecha-91a71469/

https://gmalecha.github.io/

Formal Methods for the  Informal Engineer: https://fmie2021.github.io/agenda.html 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #10: Gregory Malecha – Formal Methods and Systems Programmers Working Together Galois, Gregory Malecha, Joey Dodds, Shpat Morina 00:43:41 Gregory Malecha talks with Joey and Shpat about Bedrock, a startup bringing systems engineers together with formal methods engineers to build some of the most secure and correct systems in the world. Gregory Malecha talks with Joey and Shpat about Bedrock, a startup bringing systems engineers together with formal methods engineers to build some of the most secure and correct systems in the world. no full 10 ed7d69bf-64eb-4f0f-8945-35f76f9b1362 #9: Tycho Andersen – Commit Log Spelunking Tycho Andersen shares lessons that Linux kernel developers have learned from decades of open-source interactions. We discuss how the open-source community works together to make the Linux kernel better for everyone, and also what it's like to work debugging the kernel.

Watch all our episodes on the Building Better Systems Youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Tycho Andersen: https://tycho.pizza/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Thu, 13 May 2021 19:42:08 +0000 marketing@galois.com (Galois, Shpat Morina, Tycho Andersen, Joey Dodds) https://building-better-systems.simplecast.com/episodes/9-tycho-andersen-commit-log-spelunking-oYFegiV8 Tycho Andersen shares lessons that Linux kernel developers have learned from decades of open-source interactions. We discuss how the open-source community works together to make the Linux kernel better for everyone, and also what it's like to work debugging the kernel.

Watch all our episodes on the Building Better Systems Youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Tycho Andersen: https://tycho.pizza/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #9: Tycho Andersen – Commit Log Spelunking Galois, Shpat Morina, Tycho Andersen, Joey Dodds 00:42:34 Tycho Andersen shares lessons that Linux kernel developers have learned from decades of open-source interactions. We discuss how the open-source community works together to make the Linux kernel better for everyone, and also what it's like to work debugging the kernel. Tycho Andersen shares lessons that Linux kernel developers have learned from decades of open-source interactions. We discuss how the open-source community works together to make the Linux kernel better for everyone, and also what it's like to work debugging the kernel. no full 9 c9dd9dc0-54ad-4a47-9153-a1db11451cc2 #8: Eric Davis – Building Better Data Models Dr. Eric Davis walks us through what it means for a data model to be trustworthy, what common pitfalls predictive models run into, reproducibility issues, and what can be done. We chat about how subject area experts are expected to be many things: statisticians, computer scientists, and mathematicians, and how that can sometimes lead to mistakes. We also look at the COVID-19 pandemic and how data models affect decision-making.

https://www.imagwiki.nibib.nih.gov/ https://www.imagwiki.nibib.nih.gov/content/committee-credible-practice-modeling-simulation-healthcare-description https://www.biorxiv.org/content/10.1101/2020.08.07.239855v1 https://www.imagwiki.nibib.nih.gov/content/10-simple-rules-conformance-rubric

You can watch this episode on our Youtube Channel:  https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Eric Davis: https://galois.com/team/eric-davis/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

]]> Thu, 15 Apr 2021 15:00:00 +0000 marketing@galois.com (Joey Dodds, Eric Davis, Shpat Morina, Galois) https://building-better-systems.simplecast.com/episodes/8-eric-davis-building-better-data-models-bCCdeHdQ Dr. Eric Davis walks us through what it means for a data model to be trustworthy, what common pitfalls predictive models run into, reproducibility issues, and what can be done. We chat about how subject area experts are expected to be many things: statisticians, computer scientists, and mathematicians, and how that can sometimes lead to mistakes. We also look at the COVID-19 pandemic and how data models affect decision-making.

https://www.imagwiki.nibib.nih.gov/ https://www.imagwiki.nibib.nih.gov/content/committee-credible-practice-modeling-simulation-healthcare-description https://www.biorxiv.org/content/10.1101/2020.08.07.239855v1 https://www.imagwiki.nibib.nih.gov/content/10-simple-rules-conformance-rubric

You can watch this episode on our Youtube Channel:  https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Eric Davis: https://galois.com/team/eric-davis/ 

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

 

]]> #8: Eric Davis – Building Better Data Models Joey Dodds, Eric Davis, Shpat Morina, Galois 00:34:28 Dr. Eric Davis walks us through what it means for a data model to be trustworthy, what common pitfalls predictive models run into, reproducibility issues, and what can be done. We chat about how subject area experts are expected to be many things: statisticians, computer scientists, and mathematicians, and how that can sometimes lead to mistakes. We also look at the COVID-19 pandemic and how data models affect decision-making. Dr. Eric Davis walks us through what it means for a data model to be trustworthy, what common pitfalls predictive models run into, reproducibility issues, and what can be done. We chat about how subject area experts are expected to be many things: statisticians, computer scientists, and mathematicians, and how that can sometimes lead to mistakes. We also look at the COVID-19 pandemic and how data models affect decision-making. no full 8 a7e090e1-e3ff-4e7d-8f96-9b6438fe27ef #7: Aditya Thakur – “If it goes too slow, they'll turn it off”: Analysis Tools That Work Dr. Aditya Thakur, a computer science professor at U.C. Davis, walks us through his work on developing analysis tools that he wished he had while working in industry at places like Google. Aside from program analysis, we talk about making a research group successful by exposing them to industry. Towards the end, he shares his work on techniques and tools for repairing a trained deep neural network once a mistake has been discovered. Along the way, we learn about things like abstract interpretation, non-determinism, the trickiness of parallelism, and other concepts pertinent to analysis in an approachable way.

You can watch this episode on our Youtube Channel:  https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Aditya Thakur: http://thakur.cs.ucdavis.edu/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Thu, 1 Apr 2021 22:30:39 +0000 marketing@galois.com (Joey Dodds, Aditya Thakur, Shpat Morina) https://building-better-systems.simplecast.com/episodes/aditya-thakur-if-it-goes-too-slow-theyll-turn-it-off-analysis-tools-that-work-2qmXVqSx Dr. Aditya Thakur, a computer science professor at U.C. Davis, walks us through his work on developing analysis tools that he wished he had while working in industry at places like Google. Aside from program analysis, we talk about making a research group successful by exposing them to industry. Towards the end, he shares his work on techniques and tools for repairing a trained deep neural network once a mistake has been discovered. Along the way, we learn about things like abstract interpretation, non-determinism, the trickiness of parallelism, and other concepts pertinent to analysis in an approachable way.

You can watch this episode on our Youtube Channel:  https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Aditya Thakur: http://thakur.cs.ucdavis.edu/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #7: Aditya Thakur – “If it goes too slow, they'll turn it off”: Analysis Tools That Work Joey Dodds, Aditya Thakur, Shpat Morina 01:13:38 Dr. Aditya Thakur, a computer science professor at U.C. Davis, walks us through his work on developing analysis tools that he wished he had while working in industry at places like Google. Aside from program analysis, we talk about making a research group successful by exposing them to industry. Towards the end, he shares his work on techniques and tools for repairing a trained deep neural network once a mistake has been discovered. Along the way, we learn about things like abstract interpretation, non-determinism, the trickiness of parallelism, and other concepts pertinent to analysis in an approachable way. Dr. Aditya Thakur, a computer science professor at U.C. Davis, walks us through his work on developing analysis tools that he wished he had while working in industry at places like Google. Aside from program analysis, we talk about making a research group successful by exposing them to industry. Towards the end, he shares his work on techniques and tools for repairing a trained deep neural network once a mistake has been discovered. Along the way, we learn about things like abstract interpretation, non-determinism, the trickiness of parallelism, and other concepts pertinent to analysis in an approachable way. yes full 7 a78fe91f-3942-4382-acfc-7fe2c24b8d50 #6: Dan Guido – What the hell are the blockchain people doing, and why isn't it a dumpster fire? Dan Guido, CEO of Trail of Bits, walks us through how they work with customers to make long-term improvements in security and software quality. He also describes what blockchain has done right, and how the rest of the software world should learn from them.

You can watch this episode on our Youtube Channel. 

https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Dan Guido: https://www.linkedin.com/in/danguido/

Trail of Bits blog: https://blog.trailofbits.com/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> Thu, 4 Feb 2021 20:33:11 +0000 marketing@galois.com (Joey Dodds, Dan Guido, Shpat Morina) https://building-better-systems.simplecast.com/episodes/6-dan-guido-what-the-hell-are-the-blockchain-people-doing-and-why-isnt-it-a-dumpster-fire-DkKPy3QA Dan Guido, CEO of Trail of Bits, walks us through how they work with customers to make long-term improvements in security and software quality. He also describes what blockchain has done right, and how the rest of the software world should learn from them.

You can watch this episode on our Youtube Channel. 

https://youtube.com/c/BuildingBetterSystemsPodcast

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/  

Dan Guido: https://www.linkedin.com/in/danguido/

Trail of Bits blog: https://blog.trailofbits.com/

Galois, Inc.: https://galois.com/ 

Contact us: podcast@galois.com

]]> #6: Dan Guido – What the hell are the blockchain people doing, and why isn't it a dumpster fire? Joey Dodds, Dan Guido, Shpat Morina 01:01:05 Dan Guido, CEO of Trail of Bits, walks us through how they work with customers to make long-term improvements in security and software quality. He also describes what blockchain has done right, and how the rest of the software world should learn from them. Dan Guido, CEO of Trail of Bits, walks us through how they work with customers to make long-term improvements in security and software quality. He also describes what blockchain has done right, and how the rest of the software world should learn from them. trail of bits, galois, formal verification, blockchain, security, software correctness no full 6 99babb00-f3f5-48f8-bda5-782b8ffd3fb4 #5: Talia Ringer – Proof Engineering for the People Talia Ringer, a Ph.D. candidate at University of Washington, explains how they do deep people-centric PL research. We discuss proof repair, UX for software correctness, and how to ask users of tools for feedback to react to.

You can watch this episode on our Youtube Channel. 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Talia Ringer: https://dependenttyp.es/ 

Contact us: podcast@galois.com 

Galois, Inc.: https://galois.com/ 
 

]]> Mon, 11 Jan 2021 21:05:53 +0000 marketing@galois.com (Galois Inc.) https://building-better-systems.simplecast.com/episodes/5-talia-ringer-proof-engineering-for-the-people-q8KcL5DS Talia Ringer, a Ph.D. candidate at University of Washington, explains how they do deep people-centric PL research. We discuss proof repair, UX for software correctness, and how to ask users of tools for feedback to react to.

You can watch this episode on our Youtube Channel. 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Talia Ringer: https://dependenttyp.es/ 

Contact us: podcast@galois.com 

Galois, Inc.: https://galois.com/ 
 

]]> #5: Talia Ringer – Proof Engineering for the People Galois Inc. 00:30:17 Talia Ringer, a Ph.D. candidate at University of Washington, explains how they do deep people-centric PL research. We discuss proof repair, UX for software correctness, and how to ask users of tools for feedback to react to. Talia Ringer, a Ph.D. candidate at University of Washington, explains how they do deep people-centric PL research. We discuss proof repair, UX for software correctness, and how to ask users of tools for feedback to react to. galois, pl research, formal methods, proof engineering, software correctness no full 5 2595967a-155e-40ea-b4d6-f9698abbd525 #4: Alex Malozemoff – New attack on homomorphic encryption libraries: what does it mean? Principal Researcher, Alex Malozemoff, walks us through what homomorphic encryption is, what CKKS is, and how a recent new attack on CKKS will impact progress on homomorphic encryption.

You can watch this episode on our Youtube channel.

Galois, Inc.

Joey Dodds

Shpat Morina

Alex Malozemoff

On the Security of Homomorphic Encryption on Approximate Numbers by Baiyu Li and Daniele Micciancio

Contact us: podcast@galois.com

 

]]> Tue, 15 Dec 2020 14:00:00 +0000 marketing@galois.com (Galois Inc.) https://building-better-systems.simplecast.com/episodes/4-alex-malozemoff-new-attack-on-homomorphic-encryption-libraries-what-does-it-mean-CtWPUbUs Principal Researcher, Alex Malozemoff, walks us through what homomorphic encryption is, what CKKS is, and how a recent new attack on CKKS will impact progress on homomorphic encryption.

You can watch this episode on our Youtube channel.

Galois, Inc.

Joey Dodds

Shpat Morina

Alex Malozemoff

On the Security of Homomorphic Encryption on Approximate Numbers by Baiyu Li and Daniele Micciancio

Contact us: podcast@galois.com

 

]]> #4: Alex Malozemoff – New attack on homomorphic encryption libraries: what does it mean? Galois Inc. 00:17:04 Principal Researcher, Alex Malozemoff, walks us through what homomorphic encryption is, what CKKS is, and how a recent new attack on CKKS will impact progress on homomorphic encryption. Principal Researcher, Alex Malozemoff, walks us through what homomorphic encryption is, what CKKS is, and how a recent new attack on CKKS will impact progress on homomorphic encryption. no full 4 37a926b3-81f8-4832-8f2e-2d52a390b50f #3: Stephen Magill & Tom DuBuisson – Musing on continuous code analysis The founders of MuseDev discuss making modern static analysis usable and leveraging the latest promising research for automatic bug finding. MuseDev is a spin-off of Galois. 

Video of this podcast can be found on our Youtube channel: 

Galois, Inc.: https://galois.com/ 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/ 

Muse.dev 

Tom Dubuisson: https://www.linkedin.com/in/thomas-dubuisson-62910453/ 

Stephen Magill, https://www.linkedin.com/in/stephen-magill-2070a096/

Continuous Reasoning: Scaling the impact of formal methods by Peter W. O’Hearn https://bit.ly/2I0TJEs

Contact us: podcast@galois.com 

]]> Thu, 3 Dec 2020 18:07:38 +0000 marketing@galois.com (Joey Dodds, Shpat Morina) https://building-better-systems.simplecast.com/episodes/3-stephen-magill-tom-dubuisson-musing-on-continuous-code-analysis-T0GdX8YQ The founders of MuseDev discuss making modern static analysis usable and leveraging the latest promising research for automatic bug finding. MuseDev is a spin-off of Galois. 

Video of this podcast can be found on our Youtube channel: 

Galois, Inc.: https://galois.com/ 

Joey Dodds: https://galois.com/team/joey-dodds/ 

Shpat Morina: https://galois.com/team/shpat-morina/ 

Muse.dev 

Tom Dubuisson: https://www.linkedin.com/in/thomas-dubuisson-62910453/ 

Stephen Magill, https://www.linkedin.com/in/stephen-magill-2070a096/

Continuous Reasoning: Scaling the impact of formal methods by Peter W. O’Hearn https://bit.ly/2I0TJEs

Contact us: podcast@galois.com 

]]> #3: Stephen Magill & Tom DuBuisson – Musing on continuous code analysis Joey Dodds, Shpat Morina 01:00:50 The founders of MuseDev discuss making modern static analysis usable and leveraging the latest promising research for automatic bug finding. MuseDev is a spin-off of Galois. The founders of MuseDev discuss making modern static analysis usable and leveraging the latest promising research for automatic bug finding. MuseDev is a spin-off of Galois. cybersecurity, reliability, code analysis, open source, static analysis, continuous assurance, assurance software, devops no full 3 4b3beac3-50f8-4abf-b07c-6a9ad5e28af7 #2: Jean Yang – "Formal" Methods? How about "Business Casual" Methods? Part 2 Video of this podcast can be found on our Youtube channel

Jean Yang: https://www.linkedin.com/in/jean-yang-96575030/

Akita Software: https://www.akitasoftware.com/

Galois, Inc.: https://galois.com/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina:  https://galois.com/team/shpat-morina/

Contact us: marketing@galois.com

]]> Wed, 28 Oct 2020 05:09:27 +0000 marketing@galois.com (Joey Dodds, Shpat Morina) https://building-better-systems.simplecast.com/episodes/2-jean-yang-formal-methods-how-about-business-casual-methods-part-2-5nXW1ykT Video of this podcast can be found on our Youtube channel

Jean Yang: https://www.linkedin.com/in/jean-yang-96575030/

Akita Software: https://www.akitasoftware.com/

Galois, Inc.: https://galois.com/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina:  https://galois.com/team/shpat-morina/

Contact us: marketing@galois.com

]]> #2: Jean Yang – "Formal" Methods? How about "Business Casual" Methods? Part 2 Joey Dodds, Shpat Morina 00:35:28 Jean Yang, Founder and CEO of Akita Software, walks us through what makes API analysis an effective approach to finding critical issues in your systems, and what it takes to get a new company started. As a bonus, you'll learn about what formal methods and fashion design have in common. This is part two of a two-part episode. Please make sure to check out part one. Jean Yang, Founder and CEO of Akita Software, walks us through what makes API analysis an effective approach to finding critical issues in your systems, and what it takes to get a new company started. As a bonus, you'll learn about what formal methods and fashion design have in common. This is part two of a two-part episode. Please make sure to check out part one. cybersecurity, assurance, software, reliability, formal methods, verification no full 2 1fdaf9d6-7290-49d0-956a-99c096d8b17a #1: Jean Yang – "Formal" Methods? How about "Business Casual" Methods? Part 1 Video of this podcast can be found on our Youtube channel. 

Jean Yang: https://www.linkedin.com/in/jean-yang-96575030/

Akita Software: https://www.akitasoftware.com/

Galois, Inc.: https://galois.com/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina:  https://galois.com/team/shpat-morina/

Contact us: marketing@galois.com

]]> Fri, 23 Oct 2020 21:18:52 +0000 marketing@galois.com (Shpat Morina, Joey Dodds) https://building-better-systems.simplecast.com/episodes/1-jean-yang-formal-methods-how-about-business-casual-methods-46o_lh1e Video of this podcast can be found on our Youtube channel. 

Jean Yang: https://www.linkedin.com/in/jean-yang-96575030/

Akita Software: https://www.akitasoftware.com/

Galois, Inc.: https://galois.com/

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina:  https://galois.com/team/shpat-morina/

Contact us: marketing@galois.com

]]> #1: Jean Yang – "Formal" Methods? How about "Business Casual" Methods? Part 1 Shpat Morina, Joey Dodds 00:29:39 Jean Yang, Founder and CEO of Akita Software, walks us through what makes API analysis an effective approach to finding critical issues in your systems, and what it takes to get a new company started. As a bonus, you'll learn about what formal methods and fashion design have in common. This is part one of a two-part episode. Please make sure to check out part two. Jean Yang, Founder and CEO of Akita Software, walks us through what makes API analysis an effective approach to finding critical issues in your systems, and what it takes to get a new company started. As a bonus, you'll learn about what formal methods and fashion design have in common. This is part one of a two-part episode. Please make sure to check out part two. cybersecurity, assurance, software, formal verification, reliability, formal methods, verification no full 1