From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019) — различия между версиями

Материал из 0x1.tv

 
{{LinksSection}}
<!-- * [ Talks page on site] -->
<!-- <blockquote>[©]</blockquote> -->

{{vklink|1524}}                                          
<references/>





<!-- topub -->

[[Категория:ISPRASOPEN-2019]]
[[Категория:Верификация]]
{{stats|disqus_comments=0|refresh_time=2020-017-28T12:06:5605T22:44:51.387919819938|vimeo_plays=12|youtube_comments=0|youtube_plays=0}}25}}

Версия 19:44, 5 июля 2020

Speaker
Nikolaj Bjørner.jpg
Nikolaj Bjørner

Modern theorem provers have in the past decade demonstrated immense capabilities and found numerous practical applications. Building a theorem prover takes extensive empirical research, supported by careful thought, clever insight, and a deep theoretical understanding of logical formalisms and reasoning. In this talk I describe an underlying insight that has found its way into Z3's core in different guises over the years: model-based search and saturation. Z3 is a state-of-art theorem prover available from Microsoft Research. Inspiration isn't born in vacuum. A set of north stars taken from driving scenarios, such verifying compilers, symbolic execution, quantum compilation, and network verification to name a few, have shaped directions of research and systems building in Z3.

Video

on youtube

Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.

Slides

From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf
From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019)!.jpg

Links

Plays:27   Comments:0

Источник — «https://0x1.tv/index.php?title=From_North_Stars_to_Clever_Insights_—_On_using_grand_challenges_to_drive_new_techniques_in_automated_theorem_proving_(Nikolaj_Bjørner,_ISPRASOPEN-2019)&oldid=156020»