Atlas Computing
@atlascomputing.bsky.social
Atlas Computing is a tech non-profit empowering humans to have more control over AI capabilities.
Son Ho with an update on Aeneas : Formal verification of Rust program by functional translation, a tool developed from combined efforts of Microsoft Azure and Inria Paris youtu.be/24Wt5FvmcHM
2025 Atlas Computing Symposium : Rust in Ottawa #rustlang
2025 Atlas Computing Symposium : Rust in Ottawa #rustlang
Atlas Computing Symposium Rust Ottawa 2025 - Aeneas
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 5:10 PM
Son Ho with an update on Aeneas : Formal verification of Rust program by functional translation, a tool developed from combined efforts of Microsoft Azure and Inria Paris youtu.be/24Wt5FvmcHM
2025 Atlas Computing Symposium : Rust in Ottawa #rustlang
2025 Atlas Computing Symposium : Rust in Ottawa #rustlang
Everett Hildenbrandt with a demo by Daniel Cumming and Jost Berthold on Formal Verification of Rust programs using stable MIR and the K framework at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/VPkTZEf4ks8
youtu.be/VPkTZEf4ks8
Atlas Computing Symposium Rust Ottawa 2025 - Symbolic Execution of Rust code via Stable MIR
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 5:02 PM
Everett Hildenbrandt with a demo by Daniel Cumming and Jost Berthold on Formal Verification of Rust programs using stable MIR and the K framework at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/VPkTZEf4ks8
youtu.be/VPkTZEf4ks8
Guillaume Claret from Formal Land presenting Formal Verification for Rust in Rocq at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/2TsA_xJn7yU
youtu.be/2TsA_xJn7yU
Atlas Computing Symposium Rust Ottawa 2025 - Coq-of-Rust
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 4:57 PM
Guillaume Claret from Formal Land presenting Formal Verification for Rust in Rocq at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/2TsA_xJn7yU
youtu.be/2TsA_xJn7yU
Zyad Hassan, Senior Applied Scientist @AWS, presenting the Contract-based verification in Kani at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/6eqJZmU04b8
youtu.be/6eqJZmU04b8
Atlas Computing Symposium Rust Ottawa 2025 - Contract-based verification in Kani
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 4:53 PM
Zyad Hassan, Senior Applied Scientist @AWS, presenting the Contract-based verification in Kani at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/6eqJZmU04b8
youtu.be/6eqJZmU04b8
Aymeric Fromherz from Inria (Paris) presenting an update on Charon at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/jYX-wgLP1MU
youtu.be/jYX-wgLP1MU
Atlas Computing Symposium Rust Ottawa 2025 - Charon
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 4:50 PM
Aymeric Fromherz from Inria (Paris) presenting an update on Charon at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/jYX-wgLP1MU
youtu.be/jYX-wgLP1MU
Remi Delmas, Principal Applied Scientist @awscloud.bsky.social presenting the Harness-based verification in Kani at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/QW2R4z7WPMU
youtu.be/QW2R4z7WPMU
Atlas Computing Symposium Rust Ottawa 2025 - Harness-based verification in Kani
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 4:47 PM
Remi Delmas, Principal Applied Scientist @awscloud.bsky.social presenting the Harness-based verification in Kani at the 2025 Atlas Computing Symposium : Rust in Ottawa
youtu.be/QW2R4z7WPMU
youtu.be/QW2R4z7WPMU
Xavier Denis from ETH Zurich giving an update on Creusot at the Atlas Computing Symposium Rust Ottawa 2025
youtu.be/CMGgk08p2SA
youtu.be/CMGgk08p2SA
Atlas Computing Symposium Rust Ottawa 2025 - Creusot
YouTube video by Atlas Computing
youtu.be
May 8, 2025 at 4:41 PM
Xavier Denis from ETH Zurich giving an update on Creusot at the Atlas Computing Symposium Rust Ottawa 2025
youtu.be/CMGgk08p2SA
youtu.be/CMGgk08p2SA
All the videos from the Atlas Computing Symposium on Formal Methods for Rust at @icseconf.bsky.social 2025 are out. bit.ly/3GJ55e9
This has been a great combo of industry and academic talks with participation from AWS, Microsoft, Inria, ETH Zurich, Formal Land, and Runtime Verification.
#rustlang
This has been a great combo of industry and academic talks with participation from AWS, Microsoft, Inria, ETH Zurich, Formal Land, and Runtime Verification.
#rustlang
YouTube
Share your videos with friends, family, and the world.
bit.ly
May 8, 2025 at 3:52 PM
All the videos from the Atlas Computing Symposium on Formal Methods for Rust at @icseconf.bsky.social 2025 are out. bit.ly/3GJ55e9
This has been a great combo of industry and academic talks with participation from AWS, Microsoft, Inria, ETH Zurich, Formal Land, and Runtime Verification.
#rustlang
This has been a great combo of industry and academic talks with participation from AWS, Microsoft, Inria, ETH Zurich, Formal Land, and Runtime Verification.
#rustlang
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Sponsor highlight: The Automated Reasoning Group at Amazon Web Services is focusing on the automation of formal logical reasoning to raise the bar on security, durability, availability, and quality.
Sponsor highlight: The Automated Reasoning Group at Amazon Web Services is focusing on the automation of formal logical reasoning to raise the bar on security, durability, availability, and quality.
April 23, 2025 at 8:51 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Sponsor highlight: The Automated Reasoning Group at Amazon Web Services is focusing on the automation of formal logical reasoning to raise the bar on security, durability, availability, and quality.
Sponsor highlight: The Automated Reasoning Group at Amazon Web Services is focusing on the automation of formal logical reasoning to raise the bar on security, durability, availability, and quality.
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Zyad Hassan is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services (AWS), where he works on the Kani Rust Verifier.
Speaker highlight: Zyad Hassan is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services (AWS), where he works on the Kani Rust Verifier.
April 23, 2025 at 8:47 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Zyad Hassan is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services (AWS), where he works on the Kani Rust Verifier.
Speaker highlight: Zyad Hassan is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services (AWS), where he works on the Kani Rust Verifier.
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Rémi Delmas is a Principal Applied Scientist at Amazon Web Services (AWS) Automated Reasoning Group in Boston. #rustlang
Speaker highlight: Rémi Delmas is a Principal Applied Scientist at Amazon Web Services (AWS) Automated Reasoning Group in Boston. #rustlang
April 23, 2025 at 8:45 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Rémi Delmas is a Principal Applied Scientist at Amazon Web Services (AWS) Automated Reasoning Group in Boston. #rustlang
Speaker highlight: Rémi Delmas is a Principal Applied Scientist at Amazon Web Services (AWS) Automated Reasoning Group in Boston. #rustlang
Reposted by Atlas Computing
Breaking News: Google acted illegally to maintain a monopoly in some online advertising technology, a federal judge ruled.
Google Is a Monopolist in Online Advertising Tech, Judge Says
The ruling was the second time in a year that a federal court had found that Google had acted illegally to maintain its dominance.
www.nytimes.com
April 17, 2025 at 2:54 PM
Breaking News: Google acted illegally to maintain a monopoly in some online advertising technology, a federal judge ruled.
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Guillaume Claret is a security researcher and the founder of @formalland.bsky.social, a company specializing in the application of formal methods to critical code. #rustlang
Speaker highlight: Guillaume Claret is a security researcher and the founder of @formalland.bsky.social, a company specializing in the application of formal methods to critical code. #rustlang
April 18, 2025 at 12:32 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Guillaume Claret is a security researcher and the founder of @formalland.bsky.social, a company specializing in the application of formal methods to critical code. #rustlang
Speaker highlight: Guillaume Claret is a security researcher and the founder of @formalland.bsky.social, a company specializing in the application of formal methods to critical code. #rustlang
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Daniel Cumming has been a verification engineer for Runtime Verification Inc. for over 2 years, nearly exclusively working with #Rust code.
Speaker highlight: Daniel Cumming has been a verification engineer for Runtime Verification Inc. for over 2 years, nearly exclusively working with #Rust code.
April 17, 2025 at 1:34 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Daniel Cumming has been a verification engineer for Runtime Verification Inc. for over 2 years, nearly exclusively working with #Rust code.
Speaker highlight: Daniel Cumming has been a verification engineer for Runtime Verification Inc. for over 2 years, nearly exclusively working with #Rust code.
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Aymeric Fromherz is a researcher in the Prosecco team at Inria Paris. He received his PhD from Carnegie Mellon University in 2021.
Speaker highlight: Aymeric Fromherz is a researcher in the Prosecco team at Inria Paris. He received his PhD from Carnegie Mellon University in 2021.
April 17, 2025 at 1:29 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Aymeric Fromherz is a researcher in the Prosecco team at Inria Paris. He received his PhD from Carnegie Mellon University in 2021.
Speaker highlight: Aymeric Fromherz is a researcher in the Prosecco team at Inria Paris. He received his PhD from Carnegie Mellon University in 2021.
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Son Ho is a post-doc working on program verification at Azure Research after completing his PhD at Inria Paris. #Rust
Speaker highlight: Son Ho is a post-doc working on program verification at Azure Research after completing his PhD at Inria Paris. #Rust
April 17, 2025 at 1:25 PM
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc
Speaker highlight: Son Ho is a post-doc working on program verification at Azure Research after completing his PhD at Inria Paris. #Rust
Speaker highlight: Son Ho is a post-doc working on program verification at Azure Research after completing his PhD at Inria Paris. #Rust
Attending #ICSE2025 in Ottawa? Join us at the Rust Symposium (Friday, May 2, 9am-5pm) for a full day of cutting-edge tools and research. Featuring speakers from AWS, ETH Zurich, Formal Land, Inria, Microsoft, and Runtime Verification. #RustLang
Registration here lu.ma/umi3g2wc
Registration here lu.ma/umi3g2wc
April 14, 2025 at 3:12 PM
Attending #ICSE2025 in Ottawa? Join us at the Rust Symposium (Friday, May 2, 9am-5pm) for a full day of cutting-edge tools and research. Featuring speakers from AWS, ETH Zurich, Formal Land, Inria, Microsoft, and Runtime Verification. #RustLang
Registration here lu.ma/umi3g2wc
Registration here lu.ma/umi3g2wc
Attending the GovAI Summit was great, but there is so much work to do, as very few understand the AI space. Gov AI is all about risk management, regulation, and regulatory compliance. Synthetic data, data poisoning, ownership, and protection are very close to top priorities.
November 1, 2024 at 2:21 PM
Attending the GovAI Summit was great, but there is so much work to do, as very few understand the AI space. Gov AI is all about risk management, regulation, and regulatory compliance. Synthetic data, data poisoning, ownership, and protection are very close to top priorities.
If you are in Singapore next week, Atlas Computing CEO Dr. Evan Miyazono will also be there for a few MDDI meetings and a SICW talk.
www.sicw.gov.sg/speakers/dr-...
www.sicw.gov.sg/speakers/dr-...
October 11, 2024 at 7:57 PM
If you are in Singapore next week, Atlas Computing CEO Dr. Evan Miyazono will also be there for a few MDDI meetings and a SICW talk.
www.sicw.gov.sg/speakers/dr-...
www.sicw.gov.sg/speakers/dr-...
On October 3rd, meet Evan Miyazono, the CEO of Atlas Computing, at the upcoming 2024 Desmarais Global Finance Lectures: Navigating the (Responsible) Uses of AI in Finance in Montreal at McGill University Innovation Fund. tinyurl.com/ytyh3z9f
September 26, 2024 at 6:35 PM
On October 3rd, meet Evan Miyazono, the CEO of Atlas Computing, at the upcoming 2024 Desmarais Global Finance Lectures: Navigating the (Responsible) Uses of AI in Finance in Montreal at McGill University Innovation Fund. tinyurl.com/ytyh3z9f