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

{{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|}}{{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]]