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
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) (Batch edit: replace PCRE (\n\n)+(\n) with \2) |
||
(не показано 10 промежуточных версий этого же участника) | |||
{{eng}} ;{{SpeakerInfo}}: {{Speaker|Nikolaj Bjørner}} <blockquote> 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. </blockquote> {{VideoSection}} {{vimeoembed|378874905|800|450}} {{youtubelink|}}|ri6_nAEAnDA}} {{letscomment}} {{SlidesSection}} [[File:From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019).pdf|left|page=-|300px]] {{----}} [[File:{{#setmainimage:From North Stars to Clever Insights — On using grand challenges to drive new techniques in automated theorem proving (Nikolaj Bjørner, ISPRASOPEN-2019)!.jpg}}|center|640px]] {{LinksSection}} <!-- * [ Talks page on site] --> <!-- <blockquote>[©]</blockquote> --> {{vklink|1524}} <references/> <!-- topub --> [[Категория:ISPRASOPEN-2019]] [[Категория:Верификация]] {{stats|disqus_comments=0|refresh_time=2020-01-09T16:01:042021-08-31T16:21:27.465840500934|vimeo_plays=13|youtube_comments=0|youtube_plays=0}}43}} |
Текущая версия на 12:19, 4 сентября 2021
- Speaker
- 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
Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.
Slides
Links
Plays:46 Comments:0